今年 7 月，字节跳动 Seed 团队受邀参加了 IMO 2025。我们的形式化数学推理模型 Seed Prover 通过 3 天的尝试，完整解决了 6 道题目中的 4 道以及一道题的部分证明，达到官方认证的银牌成绩。
近日，我们推出新一代形式化数学推理专用模型 Seed Prover 1.5 ，通过大规模的 Agentic RL 训练，其推理能力和推理效率取得显著进步。相比上一代模型，Seed Prover 1.5 在 16.5 小时内，针对 IMO 2025 的前 5 道题目生成了完整可编译验证的 Lean 证明代码，换算成绩为 35/42，达到此前 IMO 评分标准的金牌分数线。
针对北美本科级别数学竞赛 Putnam，Seed Prover 1.5 用时 9 小时，对 12 道 Putnam 2025 赛题中的 11 道生成了可编译验证的 Lean 代码。更系统的评估中，Seed Prover 1.5 表现出色：它在完整的 Putnam 历史评估集上解决了 88% 的问题，在代表硕士数学难度的 Fate-H 和代表博士生数学难度的 Fate-X 评估集上，分别解决了 80% 和 33% 的问题，刷新了形式化数学推理模型在这几个评测集上的 SOTA 表现。
Seed Prover 1.5 在多个评估集上与此前其他 SOTA 方法的比较（柱列上数字代表解决评估集中问题的数量）
Seed Prover 1.5 的技术报告已对外公开。我们后续将开放 API，邀请感兴趣的数学和 AI 研究者体验该模型。
技术报告：
https://arxiv.org/abs/2512.17260
Lean 证明代码：
https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver-1.5/Putnam2025.zip
1. Agentic Prover：一种新的形式化数学推理范式
大语言模型已能用自然语言流畅解答不少数学问题，不过，面对复杂度极高的前沿数学研究，自然语言证明常出现逻辑跳跃或定义模糊的问题，导致难以完全获得数学家的信任。形式化数学推理则要求模型使用 Lean 等形式语言，构建可在公理系统中机械验证的证明，这意味着其在确保正确性上有着自然语言证明无法比及的优势。
但也正因如此，形式化证明比自然语言证明更加困难。根据“De Bruijn factor”经验法则，一行普通的数学推导，通常需要扩展成 4 到 10 行复杂的代码。这需要模型不仅懂数学，还要精通编程和类型论，而这一高门槛导致形式化证明在效率和成功率上一直远落后于自然语言推理。
以往的研究中，形式化证明器通常分为两类：一类是“步步为营”的 Step-prover，效率很低；一类是“一气呵成”的 Whole-prover，尝试一次性生成完整证明，一旦中间出错则前功尽弃。
Seed Prover 1.5 提出了一种全新的 Agentic Prover 架构来弥合与自然语言推理的差距，其平衡了两种形式化证明方式的优缺点：模型将 Lean 语言视为一种工具，且在证明过程中可以自主地调用其他多种工具。
Mathlib 搜索工具：类似于程序员查阅技术文档，模型可以主动检索 Lean 庞大的数学库 Mathlib，寻找可用的定理和定义，而非依赖不可靠的隐式记忆。
Python 代码执行：遇到需要计算的部分，模型可以编写并运行 Python 脚本来辅助验证直觉。
增量式引理验证：模型不再被迫一次性生成整个证明，而是将复杂问题拆解为若干引理。每证明出一个引理，系统就会将其保留并复用，作为后续推理的基石。
这种设计让模型能够灵活调整策略：既可以像人类一样先使用“草稿纸”（自然语言）进行推理，又可以随时调用工具验证猜想，最后将经过验证的模块拼装成完整的形式化证明。
Seed Prover 1.5 针对 FATE-H 问题调用工具示例
Seed Prover 1.5 的强大能力来自大规模的 Agentic RL。我们在构建的环境中让模型进行了海量的自我探索和训练。由于 Lean 编译器提供了绝对客观的“对/错”反馈，这为强化学习提供了最优质的奖励信号。实验表明，随着 RL 训练步数的增加，模型在训练集上的证明通过率从初始的 50% 升至接近 90%。
Agentic RL 还带来了大幅的效率提升。在对比测试中，Seed Prover 1.5 仅需少量的计算资源，就能在 Putnam 和 Fate 等高难度数据集上，击败消耗大量算力的上一代 Seed Prover 模型。这表明 Seed Prover 1.5 在推理能力与效率上迈上了新台阶，让形式化证明进一步走向实用化。
Seed Prover 1.5 在效率和效果上都明显领先 Seed Prover 1.0 (pass@8*8 约等于 0.4 GPU days/problem 算力)
2. Sketch Model：打通自然语言与形式语言的界限
虽有 Agentic Prover 加持，但模型面对动辄需要上万行代码的复杂定理证明，直接生成完整的形式化代码仍是一个巨大的挑战。为解决这一难题，我们训练了一个 Sketch Model，模拟人类数学家解决问题的方式：先构建高层的证明框架，再补充细节。
这一模型可将自然语言证明拆解为若干个独立的、难度更低的引理，并暂时跳过具体证明，仅保留整体的逻辑骨架。其好处显而易见：将原本不可解的复杂命题，转化成了难度显著降低的子目标。
为训练出优秀的“证明架构师”，我们采用了一种混合奖励信号的强化学习策略：
信号一：Lean 编译器验证生成的草图是否完全正确。
信号二：自然语言 Prover 会逐一检查引理，一旦发现任一引理在数学上不成立，整个草图即被否决。
信号三：引入基于长思维链的 Rubric 评分模型，从语义层面评估草图的质量——考量引理是否与自然语言证明对齐、拆解的粒度是否合适、是否真正降低了原题的难度。
最终，当草图在形式验证、数学正确性和整体评分上均满足要求时，才会获得正向奖励。
基于 Sketch Model，我们还构建了一套高效的测试工作流，形成一个分层级的多智能体协作系统：
Natural Language Prover 负责提供高层的数学直觉和自然语言证明。
Sketch Model 将自然语言转化为形式化的引理结构。
Agentic Prover 并行地攻克每一个被拆解出的引理。
如果某个引理太难证明，系统会递归地调用 Sketch Model 再次进行拆解。这种“分而治之”的策略，不仅规避了长文本生成的错误累积问题，更提升了推理的并行度和成功率。
3. 未来展望：AI 解决开放数学问题
现有 AI 系统虽已能较好解决“规则清晰、背景封闭”的数学题目，如 IMO 或 Putnam 等竞赛题，但其距离做出媲美人类专家的数学贡献仍有很大距离。这种局限性源于前沿数学研究中的“依赖性问题”——与解决“无需特定先验知识即可求解”的竞赛题不同，推动前沿数学的发展往往需要综合大量相关论文中的洞见。
为了让 AI 从“做题家”进化为真正的“研究者”，我们还需要解决三个相互关联的核心挑战：
文献发现：让模型能从大量数学文献中识别出最具影响力和相关性的论文。
基于文献的推理：让模型能立足于已有的论文，进行下一步的数学推理。
规模形式化：开发可扩展的方法，将模型从既有论文中推导出的新结果转化为形式化代码。
我们后续将对这几大难题进行探索研究。期待在不远的将来，AI 能够协助人类数学家，共同向开放性数学猜想发起冲击。
