字节跳动旗下Seed团队近日正式发布新一代形式化数学推理专用模型——Seed Prover 1.5。该模型通过大规模Agentic强化学习（RL）训练，在数学推理能力与效率方面实现突破性提升，成为形式化数学推理领域的重要进展。
在针对国际数学奥林匹克竞赛（IMO）的测试中，Seed Prover 1.5展现出强劲实力。仅用16.5小时，该模型便为IMO 2025前5道题目生成完整可编译验证的Lean证明代码，按竞赛评分标准换算后取得35分的成绩，达到金牌分数线（满分42分）。这一表现较前代模型有显著提升，标志着自动化数学推理向人类顶尖水平迈进一步。
面向北美本科数学竞赛Putnam的测试同样验证了模型的泛化能力。在9小时内，Seed Prover 1.5成功为Putnam 2025的12道赛题中的11道生成可验证的Lean代码，解题效率与准确性均达到竞赛级标准。更全面的评估显示，该模型在完整的Putnam历史题库中解决了88%的问题，在代表硕士数学难度的Fate-H评估集和博士生数学难度的Fate-X评估集中，分别攻克了80%和33%的题目，刷新了形式化数学推理模型在多项权威评测中的最优表现（SOTA）。
技术层面，Seed Prover 1.5通过创新的Agentic RL训练框架，实现了推理路径的自主规划与优化。其核心突破在于将形式化证明过程分解为可动态调整的子任务链，使模型能够根据问题特征灵活选择策略，显著提升了复杂数学问题的求解效率。团队公开的技术报告详细披露了模型架构与训练方法，为学术界与工业界提供了可复现的研究范式。
目前，Seed Prover 1.5的技术报告已对外发布，相关代码库与演示接口即将陆续开放。开发者可通过官方渠道获取Lean证明代码示例，体验模型在自动化数学推理领域的实际应用能力。这一进展不仅为数学研究提供新型辅助工具，也为人工智能在科学推理领域的拓展奠定了技术基础。
