Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience

📄 arXiv: 2512.17260v1 📥 PDF

作者: Jiangjie Chen, Wenxiang Chen, Jiacheng Du, Jinyi Hu, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Wenlei Shi, Zhihong Wang, Mingxuan Wang, Chenrui Wei, Shufa Wei, Huajian Xin, Fan Yang, Weihao Gao, Zheng Yuan, Tianyang Zhan, Zeyu Zheng, Tianxi Zhou, Thomas Hanwen Zhu

分类: cs.CL

发布日期: 2025-12-19

备注: 21 pages

💡 一句话要点

Seed-Prover 1.5：通过经验学习掌握本科水平定理证明

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 定理证明 强化学习 形式语言 Lean Agent 经验学习 测试时缩放 数学推理

📋 核心要点

  1. 现有方法在形式语言定理证明中面临挑战，尤其是在本科及以上难度的问题上，计算成本高昂。
  2. Seed-Prover 1.5通过大规模Agent强化学习训练，并结合测试时缩放（TTS）工作流程，提升证明能力。
  3. 实验结果表明，Seed-Prover 1.5在多个难度级别的基准测试中均优于现有方法，计算成本更低。

📝 摘要（中文）

大型语言模型在生成严谨的数学证明方面取得了显著进展。然而，将LLM用于形式语言（如Lean）中的定理证明仍然具有挑战性且计算成本高昂，尤其是在解决本科及以上水平的问题时。本文提出了Seed-Prover 1.5，一个通过大规模Agent强化学习训练的形式定理证明模型，以及高效的测试时缩放（TTS）工作流程。通过与Lean和其他工具的广泛交互，该模型在RL过程中不断积累经验，从而显著提高了形式定理证明的能力和效率。此外，利用自然语言证明的最新进展，我们的TTS工作流程有效地弥合了自然语言和形式语言之间的差距。与最先进的方法相比，Seed-Prover 1.5以更小的计算预算实现了卓越的性能。它解决了88%的PutnamBench（本科水平），80%的Fate-H（研究生水平）和33%的Fate-X（博士水平）问题。值得注意的是，使用我们的系统，我们在9小时内解决了Putnam 2025的12个问题中的11个。我们的研究结果表明，由高质量的形式反馈驱动的经验学习扩展，为形式数学推理的未来提供了巨大的潜力。

🔬 方法详解

问题定义：论文旨在解决形式语言（如Lean）中定理证明的问题，特别是本科及以上难度的问题。现有方法，如直接使用大型语言模型，面临计算成本高昂、难以有效利用形式化反馈等痛点。这些痛点限制了模型在复杂定理证明任务上的应用。

核心思路：论文的核心思路是通过大规模Agent强化学习，使模型能够从与形式化环境的交互中学习，积累经验。这种经验学习的方式能够使模型更好地理解形式语言的规则和约束，从而提高定理证明的效率和准确性。此外，论文还引入了测试时缩放（TTS）工作流程，以弥合自然语言和形式语言之间的差距。

技术框架：Seed-Prover 1.5的技术框架主要包括以下几个部分：1) 基于大型语言模型的Agent，负责生成证明步骤；2) 形式化环境（如Lean），用于验证证明步骤的正确性并提供反馈；3) 强化学习算法，用于优化Agent的策略；4) 测试时缩放（TTS）模块，用于将自然语言问题转换为形式语言问题。整个流程是一个迭代的过程，Agent不断与环境交互，根据反馈调整策略，最终达到解决问题的目标。

关键创新：论文最重要的技术创新点在于将大规模Agent强化学习应用于形式定理证明，并结合了测试时缩放（TTS）技术。与现有方法相比，Seed-Prover 1.5能够更有效地利用形式化反馈，从而提高学习效率和证明能力。此外，TTS技术使得模型能够处理自然语言描述的问题，降低了使用门槛。

关键设计：论文的关键设计包括：1) 强化学习算法的选择，可能采用了某种策略梯度或Q学习算法；2) 奖励函数的设计，需要能够准确反映证明步骤的正确性和效率；3) Agent的网络结构，可能采用了Transformer或其他适合序列生成的模型；4) TTS模块的具体实现，可能涉及到自然语言处理和形式语言转换的技术。具体的参数设置、损失函数和网络结构等细节可能在论文中有更详细的描述。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

Seed-Prover 1.5在PutnamBench（本科水平）上达到了88%的解决率，在Fate-H（研究生水平）上达到了80%，在Fate-X（博士水平）上达到了33%。更值得注意的是，该系统在9小时内解决了Putnam 2025的12个问题中的11个，展示了其强大的定理证明能力。与现有方法相比，Seed-Prover 1.5在性能上取得了显著提升，同时降低了计算成本。

🎯 应用场景

该研究成果可应用于自动化定理证明、形式化验证、软件工程等领域。通过提高定理证明的效率和准确性，可以加速数学研究的进展，并提高软件系统的可靠性。未来，该技术有望应用于更广泛的逻辑推理和知识发现任务。

📄 摘要（原文）

Large language models have recently made significant progress to generate rigorous mathematical proofs. In contrast, utilizing LLMs for theorem proving in formal languages (such as Lean) remains challenging and computationally expensive, particularly when addressing problems at the undergraduate level and beyond. In this work, we present \textbf{Seed-Prover 1.5}, a formal theorem-proving model trained via large-scale agentic reinforcement learning, alongside an efficient test-time scaling (TTS) workflow. Through extensive interactions with Lean and other tools, the model continuously accumulates experience during the RL process, substantially enhancing the capability and efficiency of formal theorem proving. Furthermore, leveraging recent advancements in natural language proving, our TTS workflow efficiently bridges the gap between natural and formal languages. Compared to state-of-the-art methods, Seed-Prover 1.5 achieves superior performance with a smaller compute budget. It solves \textbf{88\% of PutnamBench} (undergraduate-level), \textbf{80\% of Fate-H} (graduate-level), and \textbf{33\% of Fate-X} (PhD-level) problems. Notably, using our system, we solved \textbf{11 out of 12 problems} from Putnam 2025 within 9 hours. Our findings suggest that scaling learning from experience, driven by high-quality formal feedback, holds immense potential for the future of formal mathematical reasoning.