AIPress.com.cn报道

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

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

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

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

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

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

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

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

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

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