联合证明框架以约六分之一 token 成本达到逐候选证明成功率。
资讯摘要
论文提出一种联合证明框架，将候选答案选择、答案补充与形式化证明生成整合为统一推理过程。其核心是训练过的证明器，单次调用即可选择或提出新答案并为至少一个答案生成证明，还能复用已生成证明检测形式化陈述的忠实性错误。作者报告在 MATH-500、AMC 2023 与 AIME 2024/2025/2026 上，以约六分之一 token 成本达到逐候选证明的成功率，并识别出至少 6.1% 的不忠实形式化陈述。
要点速读
- 框架将候选答案选择、答案补充和 Lean 形式化证明生成合并为一次推理调用。
- 作者报告在 MATH-500、AMC 2023、AIME 2024/2025/2026 上以约六分之一 token 成本达到与逐候选证明相同的成功率。
- 无需额外评判器即可识别至少 6.1% 的不忠实形式化陈述；模型与代码已公开。
中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/28 08:00:17（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。