超越求解器判定：用于自动形式化的生成式奖励模型
神经符号系统依赖数学求解器来验证推理，但求解器无法判断形式翻译是否与指定的参考形式化保持严格等价。该研究将一种失效模式定义为“保留判定的不忠实性”（VPU）：错误编码仍能成功执行，并产生预期判定。理论分析表明，仅依赖结构和判定结果的验证方法，检测这类案例的能力最多接近随机水平。研究人员提出 Generative Verification（GenV），将离线的 Z3 等价性预言器蒸馏为连续且无需参考内容的分数，并利用语言模型的词汇空间。在实验中，结合困难负例的 GenV 验证器取得 0.961 的 AUROC，能够零样本泛化到未见过的翻译器和形式风格，并使智能体在推理时进行计算资源分配的下游准确率提升 11.3 个百分点。
本文来源：Hugging Face，仅供学习参考，版权归原作者所有。