面对国际数学奥林匹克竞赛前五道题目，这个AI模型在16.5小时内生成完整证明代码，换算成绩达到金牌分数线。

字节跳动Seed团队于12月24日宣布推出新一代形式化数学推理专用模型Seed Prover 1.5。该模型基于大规模Agentic RL训练框架，在多项数学推理基准测试中刷新纪录。

在北美本科数学竞赛Putnam 2025的12道赛题中，Seed Prover 1.5仅用9小时就成功为其中11道生成了可编译验证的Lean证明代码。

01 竞赛表现

Seed Prover 1.5在多项国际数学竞赛中展现出接近人类顶尖水平的推理能力。

最引人注目的是，面对国际数学奥林匹克竞赛IMO 2025的前五道题目，该模型在16.5小时内生成了完整且可通过编译验证的Lean证明代码。

换算成比赛成绩，这一表现相当于获得35分（满分42分），达到了过往IMO金牌获奖的分数线标准。

在更具系统性的评估中，Seed Prover 1.5在完整的Putnam历史试题集上解决了88%的问题。这一数据集涵盖了北美本科数学竞赛多年来的题目，是对模型广度和稳定性的全面检验。

02 技术突破

Seed Prover 1.5的核心创新在于其独特的技术架构和训练方法。

该模型采用Agentic Prover架构，结合了自然语言推理与形式化证明的双重优势。与传统的“逐步交互”或“全证明生成”模式不同，这种架构允许模型在推理过程中动态调整与证明环境的交互粒度。

训练过程中，模型通过大规模Agentic强化学习，在Lean证明环境中持续积累经验。研究人员还引入了Sketch Model，专门模拟人类数学家的思路，将自然语言证明转化为结构化证明框架。

这种方法有效弥合了自然语言推理与形式化数学证明之间的鸿沟，使模型能够调用多种工具，通过增量式引理验证拆解复杂问题。

03 多层级评估

Seed Prover 1.5在不同难度层级的数学问题集上进行了全面测试，结果均刷新了当前形式化数学推理模型的最优表现。

在代表硕士阶段数学难度的Fate-H测评集中，解题覆盖率达到80%；在代表博士级别数学挑战的Fate-X测评集上，也成功解决了33%的问题。

这些成绩表明，Seed Prover 1.5不仅在本科级别数学问题上表现优异，还能够应对更高阶的数学推理挑战。

特别值得注意的是，模型在保持高性能的同时，计算资源消耗相对合理。这与早期形式化证明系统需要海量计算资源形成鲜明对比，显示出效率上的显著提升。

04 行业影响与开源

形式化数学推理被认为是检验人工智能深层推理能力的重要试金石。Seed Prover 1.5的突破性表现，为AI在严谨数学证明领域的应用开辟了新路径。

目前，该模型的技术报告已在arXiv平台对外发布，供学术界和工业界研究参考。部分生成的Lean证明代码也已收录于开源仓库。

字节跳动Seed团队表示，后续将开放模型API接口，支持更广泛的研究与应用。这一举措将邀请全球数学和AI研究者共同探索形式化推理的前沿。

技术报告详细披露了模型的架构设计、训练数据构建与验证流程。这种开放性有助于推动整个领域的技术进步和学术交流。

普特南数学竞赛办公室的走廊里，历年获奖者的照片整齐排列。今年的获奖名单尚未公布，但Seed Prover 1.5已经用9小时11道题的成绩，在数学推理的赛道上刻下了新的里程碑。

当字节跳动Seed团队宣布将开放模型API时，全球数学与人工智能研究社区正密切关注这一工具的后续进展。Lean证明代码开源仓库的链接已经活跃着第一批研究者的身影。