Beyond Solver Verdicts: Generative Reward Models for Autoformalization
超越求解器裁决：用于自动形式化的生成式奖励模型
🧭 Autoformalization · 生成式验证
Case Western Reserve University · Amazon Web Services
将离线 Z3 等价 oracle 蒸馏为生成式连续等价评分，检测 VPU，AUROC 0.961，并带来 11.3 点下游提升
📌 工作参考价值（4 点）
- 把验证器从结构化硬判定升级为连续、参考无关的 reward model：在 query 改写、商品属性约束生成、Agent 工具调用结果校验等场景，训练一个生成式等价性打分器，能捕捉“执行成功但语义偏移”的失败样本，弥补规则/校验器只查语法和返回码的盲区。
- 用离线 oracle 蒸馏低成本验证器：电商/推荐里可用大模型、人工标注或仿真环境构造等价/非等价对，蒸馏到轻量 LM 作为 reward model，再用于线上样本过滤、beam search 重排或 RLHF-style 优化。
- 将连续验证分数用于 agentic test-time compute allocation：对候选生成结果按参考等价性评分动态分配采样/回溯预算，比固定采样或仅按 solver 成功分配更稳；可直接借鉴到多步商品推荐解释、购物 Agent 路径选择。
- 机制分析 trick：通过 decision-projected logit lens / sparse autoencoders 定位 LM 生成中的错误坐标，可用于诊断商品属性约束生成中“哪个 token 维度导致不可满足或不一致”，帮助后续提示或微调。