arXiv cs.CL· Lei Xu, Xin Quan, Andr\'e Freitas·· 2 天前AI 评分22
无需标准答案的推理：自动形式化的代理评判理论
Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization
AI 导读
研究提出一种无参考的代理评判框架，将自动形式化的正确性拆分为接地、陈述忠实性、覆盖度和推理四项，并给出代理评判误判率如何影响迭代改进的理论边界。作者用八个代理在 Lean 4 的 ProofNet、miniF2F 和 Isabelle/HOL 的 e-SNLI、ProntoQA 上验证，单代理移除下所有预先写出的预测均未被推翻。
正文 · AI 翻译
摘要：自动形式化（AF）既需要证明器接受，又需要忠实于非形式化来源，但仅凭证明器接受无法确立忠实性，而经专家验证的参考形式化又难以获取。我们引入了一个无参考的代理评判框架，将正确性分解为接地、陈述忠实性、覆盖率和推理，并提出了关于不完美检查如何影响迭代精化的理论。我们确立了三个结果。第一，对于固定的候选序列，新增代理的假阳性和假阴性率限定了其对通过但错误率的影响。第二，对正确形式化的损害需要一次假拒绝，使其暴露于进一步精化，而有害的修订随后通过无防护的更改、遗漏的更改或覆盖评判警告的证明器进展而被保留。第三，对最终通过率的分解区分了持续精化、新候选的生成及其通过检查的成功。我们用八个代理实例化了该框架，并在 Lean~4 中的 ProofNet 和 miniF2F 以及 Isabelle/HOL 中的 e-SNLI 和 ProntoQA 上测试了这些预测。在单代理移除下，运行前写下的预测无一被推翻，所有追踪到的断裂都遵循已识别的失败路径。这些结果将代理可靠性与精化的收益、风险和局限联系起来，且无需参考形式化。
| 主题： | 计算与语言（cs.CL） |
| 引用为： | arXiv:2606.09449 [cs.CL] |
| （或 arXiv:2606.09449v2 [cs.CL] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2606.09449 arXiv 颁发的 DOI 通过 DataCite |
提交历史
来自：Lei Xu [查看电子邮件]
[v1]
2026年6月8日星期一 12:57:09 UTC（241 KB）
[v2]
2026年10月14日星期三 16:45:14 UTC（370 KB）
来源：arXiv cs.CL · arxiv.org