验证通过了，题意却可能已经翻译错了

补看 · Agent / 自动形式化 · 8.5/10 · 建议深挖

让大模型把文字要求翻译成逻辑表达式，再交给数学求解器检查，是一种常见的可靠性思路。但求解器检查的是它收到的表达式。模型如果在翻译时改错了一个条件，表达式仍可能合法，求解结果也可能碰巧相同。这个“通过”并没有检查原来的意思是否保留下来。

Beyond Solver Verdicts 把这种情况单独做成了验证任务。作者先用 Z3 求解器判断候选表达式与标准答案是否逻辑等价，再把这套离线判断教给一个名为 GenV 的模型，让它在运行时给候选翻译打分。关键在于额外检查翻译本身，补上仅看最终判定发现不了的错误。

实验有个容易被摘要掩盖的细节：系统准确率从 65.5% 提高到 76.8%，但大部分增益来自多次采样。验证器帮助决定何时多算、选哪个结果；把全部 11.3 个百分点都算成验证器的贡献，会高估它的作用。

另一条边界同样重要：它学的是“与指定参考表达式等价”，还不能保证符合所有人对原文的理解。论文披露部分测试题与训练集文字重合，去除重合题后，区分正确与错误翻译的 AUROC 为 0.955；这也不是 95.5% 的准确率。做 Agent 验收时，可以借鉴它对错误类型的拆分，暂不宜把分数当成通用保险。论文 9 月 10 日提交、11 日公告，本期补看。