Seed Prover 1.5：Agentic Prover架构革新，数学定理自动证明达IMO金牌水平

图1：Seed Prover 1.5 概念示意图，寓意模型在形式化数学土壤中成长

近日，字节跳动Seed团队正式发布了新一代面向高难度数学定理证明任务的形式化推理专用模型——Seed Prover 1.5。该模型采用了全新的 Agentic Prover（智能体证明）架构，在多项国际权威数学评测中刷新了当前最优成绩，标志着自动形式化推理能力迈上了新的台阶。

什么是形式化数学推理？

形式化数学推理（Formal Theorem Proving）指的是将数学问题和证明过程，转化为可由计算机严格校验的形式化语言（如 Lean），并在逻辑系统中逐步构造、验证完整的证明链。

与使用自然语言解题不同，形式化推理要求极为严格：

• 每一步推理都必须逻辑完备；
• 最终的证明结果必须可编译、可验证；
• 不允许任何基于直觉的“跳步”。

因此，这类任务长期被认为是人工智能领域中难度最高的推理挑战之一。

核心创新一：Agentic Prover 架构

Seed Prover 1.5 最核心的升级在于引入了 Agentic Prover 架构。在这一架构下，模型不再仅仅是一个被动的文本生成器，而是化身为一个能够主动决策、调用工具的“智能体”，来组织整个证明流程。

图2：Agentic Prover 架构下的交互流程，展示了模型与工具环境的动态互动

具体而言，模型可以：

• 自主调用数学库（如 Lean 的 Mathlib）进行定理和引理的检索；
• 执行代码与计算工具，辅助完成复杂的代数或数值验证；
• 在推理过程中动态调整策略，逐步推进证明。

这种“工具增强 + 主动决策”的模式，让模型的解题方式更接近人类数学家的问题求解过程。

核心创新二：大规模 Agentic 强化学习

在训练方法上，Seed Prover 1.5 采用了大规模 Agentic 强化学习（RL）。模型与形式化证明环境进行持续交互，每一步证明尝试能否通过验证都会形成一个明确的反馈信号。通过算法层面的强化学习，模型不断优化其证明策略与搜索路径。

相比仅依赖于监督数据的方法，这种基于环境反馈的训练机制显著提升了模型在长链推理、复杂定理构造任务上的稳定性与成功率。

核心创新三：Sketch Model 证明分解机制

为了有效应对复杂且冗长的数学证明，Seed Prover 1.5 引入了 Sketch Model（证明草图模型）机制。该机制的工作流程如下：

• 首先，生成高层次的证明结构框架（Proof Sketch）；
• 接着，将原始问题拆解为多个独立的子引理；
• 然后，对各个子引理进行并行证明与验证；
• 最后，将所有子证明合并为完整的形式化证明。

这一机制有效降低了长证明中错误累积的风险，同时提升了整体的搜索效率，是模型能在高难度题目上取得突破的关键技术之一。

评测表现：多项国际竞赛刷新 SOTA

IMO 2025（国际数学奥林匹克）

在 IMO 2025 的形式化测试中，Seed Prover 1.5 展现出了强大实力：

• 在 16.5 小时内完成了前 5 道题目的 Lean 形式化证明；
• 按官方评分标准折算得分为 35 / 42；
• 达到了 IMO 金牌分数线水平。

这是当前已公开的系统中，在 IMO 级别难度下取得的最高形式化推理成绩之一。

Putnam 数学竞赛评测

在 Putnam 数学竞赛的相关测试中，Seed Prover 1.5 的表现同样突出：

• 在 Putnam 2025 赛题中，12 道题目成功解决了 11 道；
• 在 Putnam 历史题集上，整体解决率高达 88%；
• 在更高难度的评测集上：
  • Fate-H（硕士难度）：80%
  • Fate-X（博士难度）：33%

这些结果充分表明，模型已具备稳定处理从本科到研究生阶段的高难度数学问题的能力。

图3：Seed Prover 1.5 与多个前沿证明器在多项评测中的性能对比

技术开放情况

为了推动领域发展，Seed 团队已同步公开了相关的技术资料与代码资源：

• 技术论文已发布在 arXiv 上；
• Putnam 2025 的完整 Lean 证明代码已开放下载；
• 部分实验设置与评测流程可供复现。

这些资源为学术界和工业界进一步研究形式化推理提供了重要的参考。对前沿AI技术动态感兴趣的开发者，可以持续关注 云栈社区 以获得更多深度解读和技术分享。