刚刚！字节跳动 Seed Prover 1.5 发布

AIPress.com.cn报道

12月24日消息，字节跳动 Seed 团队发布了新一代形式化数学推理模型 Seed Prover 1.5。该模型基于全新的 Agentic 架构 与大规模强化学习训练，在多项高难度数学评测中实现突破，刷新了形式化数学推理模型的性能纪录。

今年 7 月，Seed 团队受邀参与 IMO 2025（国际数学奥林匹克）。当时，Seed Prover 在 3 天内完成了 6 道试题中的 4 道完整证明及 1 道部分证明，获得官方认证的 银牌成绩。

而在最新一代模型中，Seed Prover 1.5 进一步将成绩推向新高度：在 16.5 小时 内，对 IMO 2025 前 5 道题生成了 完整、可编译验证的 Lean 证明代码，换算得分为 35/42，达到以往评分体系下IMO的金牌分数线。

在北美本科数学竞赛 Putnam 中，Seed Prover 1.5 同样表现突出。模型用时约 9 小时，对 12 道赛题中的 11 道生成了可验证的 Lean 代码。更系统的评估显示，该模型在 Putnam 历史评估集上的解题率达到 88%；在代表硕士与博士数学难度的 Fate-H 与 Fate-X 评测集中，分别解决了 80% 和 33% 的问题，刷新了多个评测集上的 SOTA 纪录。

此次能力跃升，核心来自 Seed 团队提出的 Agentic Prover 架构。不同于传统形式化证明中“逐步生成”或“一次成型”的两种极端方式，Seed Prover 1.5 将 Lean 语言视作一种可调用工具，允许模型在证明过程中灵活使用 Mathlib 定理检索、Python 计算验证、增量式引理保存与复用 等多种能力。这种设计使模型能够在复杂推理中不断修正路径，显著提升成功率与效率。

在训练方法上，Seed Prover 1.5 采用了 大规模 Agentic 强化学习（RL）。官方表示，Lean 编译器提供了绝对客观的“对/错”反馈，为强化学习提供了高质量的奖励信号。随着RL训练步数增加，模型在训练集上的证明通过率从 50% 提升至近 90%，同时在高难度任务中以更低算力消耗，超越上一代模型。

为进一步缩小自然语言与形式语言之间的鸿沟，Seed 团队还训练了 Sketch Model。该模型模拟人类数学家的工作方式，先生成高层证明框架，再将复杂命题拆解为多个可并行求解的引理。

在此基础上，Seed Prover 1.5 构建了一套多智能体协作流程：由自然语言模型提供数学直觉，Sketch Model 生成证明结构，Agentic Prover 并行完成形式化验证，从而显著提升复杂定理的求解成功率。

Seed 团队表示，当前 AI 已能在规则清晰、背景封闭的竞赛型数学问题中取得突破，但距离参与真正的前沿数学研究仍有差距。未来，团队将继续探索 数学文献发现、基于文献的推理能力，以及大规模形式化方法，推动 AI 从“解题工具”向“数学研究助手”演进。

目前，Seed Prover 1.5 的技术报告已在 arXiv 公开，相关 Lean 证明代码也已上线 GitHub，后续将逐步开放 API，面向数学与 AI 研究者提供体验。