超越求解器判定：面向自动形式化的生成式奖励模型
Beyond Solver Verdicts: Generative Reward Models for Autoformalization
AI 导读
研究提出 Verdict-Preserving-Unfaithfulness（VPU）失效模式：错误的形式化翻译仍能通过求解器并得到预期判定，并证明仅依据判定的结构性验证启发式检测能力在数学上被限制在随机水平。为此提出 Generative Verification（GenV），将离线 Z3 等价性 oracle 蒸馏为无参考的连续参考等价性评分，机制分析显示其可原生提取精确的空间错误坐标。oracle 挖掘的验证器 GenV+HN 在参考等价性验证上达到 0.961 AUROC，零样本泛化到未见翻译器与不同形式风格，并在智能体测试时算力分配上带来 11.3 个百分点的下游准确率提升。