14 hours ago
Seed-Prover：自动化定理证明中的深度与广度推理
Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang, Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang, Yue Zhang, Ge Zhang, Tianyun Zhao, Jianqiu Zhao, Yichi Zhou, Thomas Hanwen Zhu
摘要
大语言模型（LLMs）通过结合长链式思维（long chain-of-thought）与强化学习，已展现出强大的数学推理能力，但在定理证明方面仍面临挑战，主要原因在于仅依赖自然语言时缺乏清晰的监督信号。专用领域特定语言（如 Lean）通过形式化证明验证提供明确的监督信号，从而支持基于强化学习的有效训练。在本工作中，我们提出 Seed-Prover——一种基于引理风格的完整证明推理模型。Seed-Prover 能够根据 Lean 的反馈、已证明的引理以及自我总结，迭代优化其证明过程。为解决国际数学奥林匹克（IMO）级别的竞赛题，我们设计了三种测试时推理策略，实现深度与广度兼具的推理能力。实验结果表明，Seed-Prover 成功证明了 78.1% 的形式化历史 IMO 问题，完全解决 MiniF2F 基准，且在 PutnamBench 上取得超过 50% 的成绩，显著超越此前的最先进方法。针对 Lean 在几何推理方面支持不足的问题，我们进一步提出几何推理引擎 Seed-Geometry，其性能优于以往的形式化几何推理系统。我们利用上述两个系统参与 2025 年国际数学奥林匹克竞赛，并成功完整证明了其中 5 道题目。本工作标志着自动化数学推理领域的重要进展，充分验证了结合形式化验证与长链式思维推理的有效性。