字节跳动旗下 Seed 团队近日正式推出了新一代面向形式化数学推理的专业模型 Seed Prover 1.5。该模型基于大规模Agentic RL训练框架，在推理能力和求解效率上都实现了显著突破。

与前代版本相比，Seed Prover 1.5 在国际数学奥林匹克竞赛IMO 2025的前五道题目中，仅用时16.5小时就生成了完整且能通过编译验证的Lean证明代码，对应得分为35分（满分42分），达到了过往IMO金牌获奖的分数线标准。

在北美本科数学竞赛Putnam 2025的测试中，该模型耗时9小时，成功为12道赛题中的11道生成了可编译运行的Lean代码。在更全面的系统性评估中，Seed Prover 1.5 在完整的Putnam历史试题集上解决了88%的问题；在代表硕士阶段数学难度的Fate-H测评分集中，解题覆盖率达到80%；在代表博士级别数学挑战的Fate-X测评分集中，也成功解决了33%的问题，三项成绩均刷新了当前形式化数学推理模型在相应基准上的最优表现。

目前，Seed Prover 1.5 的技术报告已对外发布，可供公众查阅。相关团队表示，后续将开放模型API接口以支持更广泛的研究与应用。技术报告详见：https://arxiv.org/abs/2512.17260。部分生成的Lean证明代码已收录于开源仓库，链接为：https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver-1.5/Putnam2025.zip。