Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
Seed-Prover 1.5以Agentic RL和测试时扩展，在PutnamBench达88%。
核心发现
方法论
系统由自然语言证明器、Sketch Model和Agentic Lean Prover组成。Agentic Prover在Lean、Mathlib语义检索和Python工具间循环，并以Lean编译成功为奖励。训练采用VAPO与工具交互式RL、SFT及自总结；推理阶段通过lemma式草图递归拆分目标，再并行或逐项验证子定理。
关键结果
- 在Lean v4.22.0上，系统解决PutnamBench 87.9%（约580/660）、Fate-H 80/100、Fate-X 33/100；Agentic Prover单独以Pass@8×8达到Putnam 359/660、Fate-H 57/100、Fate-X 10/100。
- 相较Seed-Prover 1.0的331/660、35/100和9/100，1.5在更低预算下明显提升；RL后训练准确率由约50%升至近90%，平均工具调用约15降至10，序列长度约28K降至17K。
- 测试时扩展呈近似对数线性收益；系统在9小时内解决Putnam 2025的12题中11题，显示自然语言分解与形式验证结合具有较高效率。
研究意义
论文说明形式化证明不只是昂贵的最终验证器，也可以成为大规模强化学习的精确环境反馈。Lean消除自然语言证明中的幻觉和逻辑漏洞，使模型能够试错、缓存已证引理并学习工具策略。结果缩小了自然语言推理与形式证明之间的能力差距，为可信数学软件、自动化教育和机器辅助研究提供了更稳固的技术路线。
技术贡献
核心贡献是把中粒度lemma交互引入Agentic Prover：既避免逐tactic交互过密，也避免整段证明一次生成过稀。LooKeng提供结构化Lean反馈，Mathlib v4.22.0语义搜索和Python执行扩展工具能力；已验证引理被缓存。Sketch Model使用VAPO、Lean结构奖励和Rubric LLM语义奖励，形成自然语言证明到Lean子目标的层级桥接。
新颖性
新颖性不在单一模型规模，而在“经验学习—正式反馈—测试时分解”的闭环。相较AlphaProof等步级方法及整段生成器，系统允许动态调整交互粒度，并把自然语言证明转化为可递归验证的lemma树；这是将高质量形式反馈用于大规模agentic RL和高效TTS的系统化实现。
局限性
- Fate-X仅解决33%，说明博士级问题仍受证明复杂度、长上下文推理和Mathlib覆盖限制。
- CombiBench存在显著形式化问题，部分Erdős问题也因形式化错误被剔除，因此跨基准比较需谨慎。
- 32K–64K长响应仍出现负分；测试时搜索可延伸至53小时，计算成本仍高。
未来方向
后续可继续迭代利用RL模型自动收集经验，改善长上下文规划、错误剪枝和搜索调度；同时扩展Mathlib、修复基准形式化质量，并研究更强的自然语言验证器、并行子目标求解和自适应预算分配，以推进PhD级及前沿猜想证明。
AI 总览摘要
形式化数学证明要求模型输出可被Lean编译器逐字检查的程序，而不是看似合理的自然语言。现有步级方法调用过密，整段生成又难以调试；AlphaProof在完整Putnam基准上约为56%，且曾报告每题约500 TPU-days的高成本。Seed-Prover 1.5试图解决能力、效率与可信度之间的矛盾。
系统包含自然语言证明器、Sketch Model和Agentic Lean Prover。前者生成严格的lemma式证明，Sketch Model将其转为含有辅助引理的Lean草图，后者通过LooKeng、Mathlib语义搜索和Python逐项验证。训练采用SFT及基于VAPO的工具交互式RL，成功编译奖励+1，否则−1；验证通过的引理会缓存，减少重复生成。测试时，失败或被反驳的子目标可递归拆分，形成层级搜索树。
在Lean v4.22.0上，系统解决PutnamBench 87.9%、Fate-H 80%和Fate-X 33%，并在9小时内解决Putnam 2025的12题中11题。RL使训练准确率约从50%升至90%，平均调用从15降至10，序列长度从约28K降至17K。论文的核心意义是展示：形式验证不仅能检查答案，也能成为模型学习工具使用和积累经验的高质量反馈源。不过，博士级问题、超长上下文、Mathlib缺口和高测试时算力仍是主要瓶颈。
深度分析
研究背景
Lean提供机器可检查的数学证明，能抑制自然语言推理中的幻觉。近年来DeepSeek-Math-V2在Putnam 2024表现近乎完美，但AlphaProof在较简单的Putnam完整基准仅解决56%，显示形式化仍有巨大性能税。既有系统主要采用逐步tactic交互或整段代码生成，前者频繁调用Lean，后者难以修复长证明。
核心问题
目标是在本科至博士级数学问题上生成可编译Lean证明，同时控制上下文、工具调用和推理成本。难点包括寻找Mathlib引理、处理数千行潜在代码、长期规划以及自然语言论证与形式语法之间的鸿沟。单一交互粒度无法兼顾局部反馈、全局结构和效率。
核心创新
- �� Agentic Prover以lemma为交互单位，动态调用Lean、Mathlib搜索和Python。
- �� RL使用Lean编译结果作为精确奖励，训练工具策略与错误恢复。
- �� Sketch Model把自然语言证明转换为lemma树，并用VAPO、Lean结构分数和Rubric语义分数训练。
- �� 测试时采用递归分解、缓存与Pass@3×3搜索，连接自然语言推理和形式验证。
方法详解
- �� 输入：Lean形式命题及可选自然语言证明。
- �� 冷启动：基于Seed-Prover 1.0的模型进行SFT，学习工具调用格式。
- �� RL：使用VAPO式截断策略目标，轨迹含工具调用；Lean成功奖励+1，失败−1。
- �� 工具：LooKeng编译验证、固定Mathlib v4.22.0的嵌入检索、Python执行。
- �� 草图：自然语言证明器生成论证，Sketch Model生成至少3个辅助引理；若引理无效则拒绝或重写。
- �� 搜索：Agentic Prover逐个证明叶节点，成功引理缓存；失败时递归重分解，直到全证或达到深度上限。
实验设计
基准包括660题的PutnamBench、各100题的Fate-H与Fate-X、CombiBench、IMO及Putnam 2025和部分Erdős问题。模型运行于Lean v4.22.0，Agentic Prover最大序列64K、最多28次工具调用；训练动态使用Putnam-200。比较对象包括Seed-Prover 1.0、AlphaProof、Hilbert Prover、Aleph Prover和Goedel-Prover-V2-32B，并考察RL步数、搜索深度和计算预算。
结果分析
Seed-Prover 1.5达到Putnam 87.9%、Fate-H 80%、Fate-X 33%；单独Agentic Prover分别为359/660、57/100、10/100。相比Seed-Prover 1.0的331/660、35/100、9/100，性能和效率均提升。RL后训练准确率近90%，平均调用由约15降至10。测试时扩大宽度和深度带来近似对数线性收益，但困难题可持续到53小时。
应用场景
系统可用于Lean数学库自动补全、教材和竞赛题形式化、证明助手中的候选引理生成，以及研究人员对猜想进行可验证探索。实际部署需要稳定的Lean环境、可靠的Mathlib版本、足够GPU/TPU预算和人工审查；教育场景还可把自然语言证明与形式证明并列展示。
局限与展望
当前方法仍明显受Mathlib覆盖和形式化质量影响，Fate-X仅33%，不能代表一般博士级数学能力。长达32K–64K的轨迹仍可能失败，递归搜索和最高53小时测试时间带来成本。论文也未提供完整消融来分离自然语言证明器、Sketch Model、缓存和各工具的独立贡献；未来需加强长程规划、并行化、自动错误剪枝和基准规范化。
通俗解读 非专业人士也能看懂
把证明想成建造一座桥。传统方法要么每放一块砖就请工程师检查，检查太频繁；要么先画完整座桥再一次验收，出错时几乎无法返工。Seed-Prover 1.5先让一个“讲解员”用普通语言说明建桥方案，再由“设计师”把方案拆成桥墩、钢梁和路面等小任务。每完成一件，Lean这个极其严格的验收员就检查它是否真的合格。
如果某个零件不合格，系统不会盲目重造整座桥，而是继续把它拆成更小的部分；合格零件会放进仓库，之后直接复用。模型还可以查数学资料库、运行小实验，并从过去的失败中总结经验。训练时，验收通过就是奖励，失败就是惩罚，所以模型逐渐学会少做无用尝试。
结果是：它在660道本科数学题中解决约88%，在研究生级Fate-H中解决80%，在博士级Fate-X中解决33%，还在9小时内做出Putnam 2025的12题中11题。它仍然昂贵且会被非常复杂的零件难住，但说明可靠检查本身可以教会AI如何更聪明地工作。
简单解释 像给14岁少年讲一样
想象你在玩一个超级难的解谜游戏，目标不是说“我觉得答案是这样”，而是要让游戏里的裁判逐步检查每一步，任何小错误都会被拒绝。Lean就是这个严格裁判，数学证明就是你要提交的通关代码。
Seed-Prover 1.5像一个会合作的游戏小队：自然语言队员先讲攻略，草图队员把攻略拆成很多小任务，Lean队员负责逐个验证。如果某任务太难，就继续拆；如果已经完成，就存进背包，下次不用再做。它还能搜索数学资料，甚至用Python做计算实验。
训练时，成功通关得1分，失败得−1分。玩得越多，它越知道什么时候查资料、什么时候试代码、什么时候总结失败。论文显示，训练后成功率从约50%升到近90%，还学会用更少的操作完成证明。
成绩很惊人：本科Putnam题解决约88%，研究生级Fate-H解决80%，博士级Fate-X解决33%；Putnam 2025中12题做对11题。不过它不是魔法：超长证明、资料库里没有的定理和博士级难题仍会卡住。你可以把它看成一个正在快速升级、但还需要更大地图和更聪明策略的数学游戏AI！
术语表
Agentic Reinforcement Learning（智能体强化学习）
模型通过多轮行动、工具反馈和奖励学习策略，而非只生成一次答案。这里的奖励由Lean是否成功编译证明决定。
用于训练Agentic Lean Prover。
Lean
一种可执行形式化逻辑系统和证明助手。证明只有通过其内核检查才被接受。
负责验证每个引理和最终定理。
VAPO
一种策略优化算法，用优势估计和概率比裁剪更新模型。论文据此处理含工具调用的多轮轨迹。
用于Agentic Prover和Sketch Model的RL训练。
Lemma-style Lean sketch（引理式Lean草图）
把大命题拆成多个辅助引理及主证明结构的中间表示。草图可先保留未证明部分，再逐项填充。
由Sketch Model生成并供递归搜索。
Test-time scaling（测试时扩展）
在推理阶段增加搜索宽度、深度或计算量来提升解题率。论文观察到其收益近似对数线性增长。
驱动Seed-Prover 1.5工作流。
Mathlib semantic search（Mathlib语义检索）
根据自然语言或数学意图检索相关定理、定义和引理。它比仅按名称查找更适合发现未知库接口。
Agentic Prover的核心辅助工具。
开放问题 这项研究留下的未解疑问
- 1 如何让模型在32K–64K甚至更长轨迹中保持稳定规划，目前负分仍然存在；需要更好的记忆压缩、证明状态抽象和长程信用分配。
- 2 Fate-X和前沿猜想的低成功率究竟来自数学推理、Lean形式化还是Mathlib缺口，尚未被严格分解，需要更细粒度的失败诊断和标准化基准。
- 3 如何在不牺牲可靠性的情况下显著降低最高53小时的搜索成本，仍是部署到研究工作流的关键问题。
应用场景
近期应用
Lean教材与题库自动形式化
教师或数学库维护者可输入自然语言证明和Lean命题，让系统生成引理草图并自动验证。前提是题目已正确形式化、使用固定Mathlib版本；输出可作为课程例题和库代码候选。
研究人员的证明助手
研究者可让自然语言证明器提出分解，再由Agentic Prover搜索Mathlib引理、运行Python检查并验证细节。它适合缩短机械化证明时间，但关键数学结论仍需专家审阅。
远期愿景
可信的AI数学研究伙伴
随着Mathlib覆盖扩大和搜索成本下降，系统可能从竞赛题扩展到研究定理、猜想验证和数学知识库构建。主要障碍是博士级创造性、基准质量和可解释的长期规划。
原文摘要
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.