风险控制的精炼式自然语言数学推理评判
人工智能
2026-05-28 v1 计算与语言
计算机科学中的逻辑
摘要
Lean 正在日益被用于评判自然语言数学答案，但其信号是部分的：许多答案从未形式化，且可能的错误证明反映的是格式错误的陈述或缺失的库事实，而非错误的答案。在 MATH-500 数据集上，我们展示该信号（i）在覆盖率依赖性上具有明显特征，即在高证明覆盖率下，证明获胜的答案正确率为 96%，而在低覆盖率下仅为 20%；（ii）稀疏且常常不可靠：7B 自动形式化器对仅 28% 的问题进行形式化，人工审计发现其中仅约 43% 的证明是可靠的。我们提出了 COVCAL，这是一种针对 Lean 诊断信息的选择器，可在接受答案或放弃的情况下，对接受答案施加有限样本选择性风险界限，在两种体系下运行（保守的 Bonferroni 边界和更紧密的 dev-then-cal 规则）。可行性取决于自动形式化覆盖率：在 7B 形式化器下，该信号过于稀疏，Bonferroni 在所有 20 个自助分区中都放弃；而专用证明器的形式化器达到 79% 的覆盖率，将其转化为在 17 个自助分区中可行，接受约 48% 的问题，准确率为 0.98。由于自我一致性本身已达到 91% 的准确率，因此我们的贡献是对何时、以及使用哪种形式化器时，部分形式化信号可在风险控制下被可靠使用的精确阐述。
引用
@article{arxiv.2605.28365,
title = {Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning},
author = {Pauline Bourigault and Xiaotong Ji and Matthieu Zimmer and Rasul Tutunov and Haitham Bou Ammar},
journal= {arXiv preprint arXiv:2605.28365},
year = {2026}
}