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

9小时攻克11道Putnam难题！Seed-Prover 1.5重塑AI形式化证明

在AI数学推理领域，我们正处于一个有趣的十字路口。一方面，DeepSeek-Math、GPT-4o等模型在自然语言解题上高歌猛进；另一方面，使用Lean等形式化语言进行严格定理证明（Formal Theorem Proving）却依然步履维艰——它不仅门槛高，而且计算成本极其昂贵。

ArXiv URL：http://arxiv.org/abs/2512.17260v1

这就引出了一个灵魂拷问：如果大模型已经能用自然语言给出高准确率的答案，我们还有必要死磕昂贵的形式化证明吗？

答案是肯定的，因为只有形式化环境（如Lean）才能提供100%可信的验证，彻底消除“幻觉”。今天我们要介绍的 Seed-Prover 1.5，正是为了打破“形式化证明太贵、太难”这一刻板印象而生。它不仅在本科生级别的数学竞赛中大杀四方，更重要的是，它证明了通过从经验中学习（Learning from Experience），AI可以在形式化证明的效率和能力上实现质的飞跃。

形式化证明的“破局者”

Seed-Prover 1.5 的核心理念非常直观：与其让模型像无头苍蝇一样在茫茫代码海中撞大运，不如把它训练成一个懂得使用工具、懂得从失败中总结经验的智能体（Agent）。

这就好比培养一个数学系学生，你不能只让他背答案，得让他去图书馆查资料（使用工具）、去草稿纸上推演（中间步骤）、并从老师的批改中学习（环境反馈）。

从上图可以看出，Seed-Prover 1.5 在各项基准测试中均取得了SOTA（State-of-the-Art）的成绩，尤其是在计算预算较小的情况下，效率惊人。

核心技术：Agentic RL 与 经验学习

Seed-Prover 1.5 的成功主要归功于两个关键技术支柱：基于工具的强化学习和自然语言到形式化语言的桥接。

1. 会用工具的 Agentic Prover

传统的证明模型要么是“步进式”（每一步都和Lean交互，太慢），要么是“生成式”（一次性生成整个证明，太难）。Seed-Prover 1.5 选择了一条中间路线：它是一个基于智能体的证明器（Agentic Prover）。

这个智能体被赋予了三种强大的武器：

• Lean验证器：实时检查代码是否正确。

• Mathlib搜索：通过语义检索，在庞大的数学库中找到相关的定理和引理（类似于程序员查文档）。

• Python执行器：用于数值计算和辅助验证。

通过大规模的强化学习（Reinforcement Learning, RL），模型学会了何时该查资料、何时该写代码、何时该回溯。训练数据显示，随着RL步数的增加，模型调用工具的次数反而下降了（从平均15次降到10次），这说明它变得更“聪明”了——不再盲目试错，而是精准打击。

2. Sketch Model：自然语言作为桥梁

我们知道，大模型在自然语言推理上已经很强了。Seed-Prover 1.5 巧妙地利用了这一点。

它引入了一个Sketch Model（草图模型）。这个模型的作用是充当“翻译官”和“架构师”。它首先将问题用自然语言解一遍，然后将其转化为Lean语言的“草图”（Sketch）。这个草图包含了一系列引理（Lemmas），将一个大难题拆解成了$N$个独立的小目标。

这种分层处理极大地降低了搜索空间。如果某个引理证不出来，系统会自动回退，重新生成草图。这种测试时扩展（Test-Time Scaling, TTS）策略，让模型能够攻克那些单次生成根本无法解决的长难证明。

惊人的实战战绩

Seed-Prover 1.5 的实战表现可以用“碾压”来形容，特别是在本科生和研究生级别的数学问题上。

• Putnam 2025 挑战：这是最令人印象深刻的战绩。在2025年的Putnam竞赛题目中，Seed-Prover 1.5 在短短 9小时 内成功解决了 12道题中的11道！相比之下，前代版本需要消耗巨大的算力才能勉强解决一半。

• 基准测试屠榜：

  • PutnamBench (本科级)：解决了 88% 的问题。

  • Fate-H (研究生级)：解决了 80% 的问题。

  • Fate-X (博士级)：解决了 33% 的问题。

值得注意的是，Seed-Prover 1.5 在达到这些成绩时，消耗的计算资源远少于 Google DeepMind 的 AlphaProof。AlphaProof 每个问题大约消耗 500 TPU-days，而 Seed-Prover 1.5 的效率实现了数量级的提升。

为什么这很重要？

Seed-Prover 1.5 的出现不仅仅是刷榜，它向我们展示了AI数学推理的未来方向：

1. 形式化与非形式化的融合：通过 Sketch Model，自然语言的灵活性和形式化语言的严谨性被完美结合。

2. 经验学习的威力：模型通过与环境交互积累“经验”，这种能力比单纯堆砌参数更具扩展性。

3. 效率即正义：在有限算力下解决复杂问题，是AI从实验室走向实际应用的关键。

虽然在博士级（PhD-level）难题上，AI 距离人类顶级数学家还有差距（主要受限于Mathlib库的覆盖范围和极度复杂的推理深度），但 Seed-Prover 1.5 已经证明：通过高质量的形式化反馈驱动的经验学习，AI 正在以前所未有的速度掌握数学真理的钥匙。

未来的数学研究，或许真的会变成 AI 负责证明，人类负责定义的协作模式。