Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
作者: 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
分类: cs.AI, cs.CL
发布日期: 2025-07-31 (更新: 2025-08-01)
💡 一句话要点
提出Seed-Prover：用于自动定理证明的深度和广度推理模型
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱五：交互与反应 (Interaction & Reaction) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 自动定理证明 形式化验证 强化学习 长链推理 大型语言模型 数学推理 几何推理
📋 核心要点
- 现有大型语言模型在定理证明中缺乏明确的监督信号，导致性能受限。
- Seed-Prover通过迭代改进证明、利用Lean反馈和引理，实现深度和广度推理。
- Seed-Prover在IMO、MiniF2F和PutnamBench等基准测试中显著超越现有技术水平。
📝 摘要（中文）
大型语言模型（LLMs）通过强化学习和长链思维展现了强大的数学推理能力，但由于仅使用自然语言时缺乏明确的监督信号，它们在定理证明方面仍然面临挑战。像Lean这样的专用领域特定语言通过形式化验证证明提供了清晰的监督，从而可以通过强化学习进行有效的训练。本文提出了Seed-Prover，一种引理式整体证明推理模型。Seed-Prover可以基于Lean反馈、已证明的引理和自我总结迭代地改进其证明。为了解决IMO级别的竞赛问题，我们设计了三种测试时推理策略，以实现深度和广度推理。Seed-Prover证明了78.1%的已形式化的IMO历史问题，饱和了MiniF2F，并在PutnamBench上实现了超过50%的准确率，大大优于之前的最先进水平。为了解决Lean中缺乏几何支持的问题，我们引入了一个几何推理引擎Seed-Geometry，它优于之前的形式几何引擎。我们使用这两个系统参加了IMO 2025，并完全证明了6个问题中的5个。这项工作代表了自动数学推理的重大进步，证明了形式化验证与长链思维推理的有效性。
🔬 方法详解
问题定义：现有的基于自然语言的大型语言模型在定理证明方面表现不佳，主要原因是缺乏清晰的监督信号。虽然大型语言模型可以通过强化学习进行训练，但定理证明的正确性验证需要形式化的证明过程，而自然语言无法提供这种精确的反馈。因此，如何利用形式化验证的优势，提升大型语言模型在定理证明方面的能力，是一个亟待解决的问题。
核心思路：Seed-Prover的核心思路是结合大型语言模型的推理能力和形式化验证的精确性。它通过迭代地生成和验证证明步骤，利用Lean等形式化语言提供的反馈来指导模型的学习和改进。此外，Seed-Prover还引入了引理式推理和自我总结机制，以增强模型的推理深度和广度。
技术框架：Seed-Prover的整体框架包括以下几个主要模块：1) 证明生成器：基于大型语言模型生成定理的证明步骤。2) 形式化验证器：使用Lean等形式化语言验证证明步骤的正确性，并提供反馈。3) 引理管理器：存储和检索已证明的引理，以供后续证明使用。4) 自我总结器：对已完成的证明进行总结，提取关键信息，用于指导未来的证明过程。5) 推理策略：在测试时，采用深度和广度相结合的推理策略，以提高证明的成功率。
关键创新：Seed-Prover的关键创新在于其引理式整体证明推理模型，以及结合形式化验证和自我总结的迭代改进机制。与传统的基于自然语言的定理证明方法相比，Seed-Prover能够利用形式化验证提供的精确反馈，从而更有效地学习和改进证明策略。此外，Seed-Prover的引理式推理和自我总结机制也增强了模型的推理能力和知识积累。
关键设计：Seed-Prover的关键设计包括：1) 使用强化学习训练证明生成器，以最大化证明的成功率。2) 设计合适的奖励函数，以鼓励模型生成正确且简洁的证明步骤。3) 采用深度和广度相结合的推理策略，例如，通过调整搜索树的宽度和深度，以平衡探索和利用。4) 为了解决Lean中缺乏几何支持的问题，专门设计了一个几何推理引擎Seed-Geometry。
🖼️ 关键图片
📊 实验亮点
Seed-Prover在多个基准测试中取得了显著的成果。在IMO问题上，Seed-Prover证明了78.1%的已形式化问题，显著优于之前的最佳水平。在MiniF2F上，Seed-Prover达到了饱和状态。在PutnamBench上，Seed-Prover的准确率超过50%。此外，Seed-Geometry在形式几何推理方面也超越了之前的引擎。在IMO 2025中，Seed-Prover成功证明了6个问题中的5个。
🎯 应用场景
Seed-Prover在自动定理证明领域具有广泛的应用前景，可以用于数学、计算机科学等领域的定理验证和发现。该技术可以辅助数学家和科学家进行研究，提高科研效率。此外，Seed-Prover还可以应用于教育领域，帮助学生学习和理解数学概念和证明方法。未来，该技术有望应用于更复杂的推理任务，例如程序验证、知识图谱推理等。
📄 摘要（原文）
LLMs have demonstrated strong mathematical reasoning abilities by leveraging reinforcement learning with long chain-of-thought, yet they continue to struggle with theorem proving due to the lack of clear supervision signals when solely using natural language. Dedicated domain-specific languages like Lean provide clear supervision via formal verification of proofs, enabling effective training through reinforcement learning. In this work, we propose \textbf{Seed-Prover}, a lemma-style whole-proof reasoning model. Seed-Prover can iteratively refine its proof based on Lean feedback, proved lemmas, and self-summarization. To solve IMO-level contest problems, we design three test-time inference strategies that enable both deep and broad reasoning. Seed-Prover proves $78.1\%$ of formalized past IMO problems, saturates MiniF2F, and achieves over 50\% on PutnamBench, outperforming the previous state-of-the-art by a large margin. To address the lack of geometry support in Lean, we introduce a geometry reasoning engine \textbf{Seed-Geometry}, which outperforms previous formal geometry engines. We use these two systems to participate in IMO 2025 and fully prove 5 out of 6 problems. This work represents a significant advancement in automated mathematical reasoning, demonstrating the effectiveness of formal verification with long chain-of-thought reasoning.