TY  - UNPB
TI  - Beyond Solver Verdicts: Generative Reward Models for Autoformalization
UR  - https://arxiv.org/abs/2609.11085
DO  - 10.48550/arXiv.2609.11085
DA  - 2026-09-10
KW  - Juju Radar
KW  - 待阅读
KW  - 补看
KW  - Agent
KW  - 自动形式化
N1  - Juju Radar · 2026-09-14  让大模型把文字要求翻译成逻辑表达式，再交给数学求解器检查，是一种常见的可靠性思路。但求解器检查的是它收到的表达式。模型如果在翻译时改错了一个条件，表达式仍可能合法，求解结果也可能碰巧相同。这个“通过”并没有检查原来的意思是否保留下来。  Beyond Solver Verdicts 把这种情况单独做成了验证任务。作者先用 Z3 求解器判断候选表达式与标准答案是否逻辑等价，再把这套离线判断教给一个名为 GenV 的模型，让它在运行时给候选翻译打分。关键在于额外检查翻译本身，补上仅看最终判定发现不了的错误。  实验有个容易被摘要掩盖的细节：系统准确率从 65.5% 提高到 76.8%，但大部分增益来自多次采样。验证器帮助决定何时多算、选哪个结果；把全部 11.3 个百分点都算成验证器的贡献，会高估它的作用。  另一条边界同样重要：它学的是“与指定参考表达式等价”，还不能保证符合所有人对原文的理解。论文披露部分测试题与训练集文字重合，去除重合题后，区分正确与错误翻译的 AUROC 为 0.955；这也不是 95.5% 的准确率。做 Agent 验收时，可以借鉴它对错误类型的拆分，暂不宜把分数当成通用保险。论文 9 月 10 日提交、11 日公告，本期补看。  入选理由：把求解器输出正确与自然语言到形式化表达的翻译正确分开，直接关系到Agent验证器的可信范围。正文揭示采样预算和参考语义的限制。 重要度：8.5/10。 论文：https://arxiv.org/abs/2609.11085 本期资料：https://www.asteronline.cn/juju-radar/2026-09-14/ AI 辅助整理；原始 PDF 以链接附件保存，未独立复现。
ER  -