字节跳动旗下Seed团队近日宣布，其研发的新一代形式化数学推理模型Seed Prover 1.5正式发布。该模型通过引入创新的Agentic架构与大规模强化学习训练方法，在多项高难度数学评测中取得突破性进展，刷新了形式化数学推理领域的性能纪录。
在备受瞩目的国际数学奥林匹克（IMO 2025）模拟测试中，Seed Prover 1.5展现出强大实力。模型仅用16.5小时便完成前5道赛题的完整形式化证明，生成可编译验证的Lean代码，最终获得35/42的评分，达到该赛事历史评分体系下的金牌标准。今年7月，其前代版本Seed Prover曾以3天完成4道完整证明和1道部分证明的成绩，获得IMO官方认证银牌。
北美本科数学竞赛Putnam的测试结果同样令人瞩目。Seed Prover 1.5在约9小时内为12道赛题中的11道生成可验证的Lean代码，系统评估显示其解题率达88%。在更高难度的Fate-H与Fate-X评测集（分别对应硕士与博士水平数学难题）中，模型分别解决了80%和33%的问题，多项指标刷新现有最优纪录。
技术突破的核心在于团队提出的Agentic Prover架构。该架构突破传统形式化证明的线性生成模式，将Lean语言转化为可调用的工具集。模型在证明过程中可动态调用Mathlib定理库检索、Python计算验证、引理增量保存与复用等功能，通过实时修正推理路径显著提升复杂问题的解决效率。这种设计使模型在保持高成功率的同时，算力消耗较前代降低30%。
训练方法方面，研究团队采用大规模Agentic强化学习框架。Lean编译器的绝对客观反馈为模型提供了精准的奖惩信号，经过数百万步训练后，模型在训练集上的证明通过率从50%跃升至近90%。这种训练方式使模型在高难度任务中展现出更强的泛化能力，部分测试场景下性能超越人类专家水平。
为弥合自然语言与形式语言之间的差异，团队同步开发了Sketch Model。该模型模拟人类数学家的思维模式，先构建高层证明框架，再将复杂命题拆解为多个可并行求解的子问题。通过与自然语言模型和Agentic Prover的协同工作，形成"直觉生成-结构规划-形式验证"的三阶段流程，使复杂定理的求解成功率提升40%。
技术文档显示，Seed Prover 1.5的研发团队已将完整技术报告上传至arXiv预印本平台，所有Lean证明代码在GitHub开源。目前模型正进行API接口测试，未来将面向数学与人工智能领域研究者开放使用。研究团队特别强调，当前模型虽在竞赛级数学问题中表现优异，但距离辅助前沿数学研究仍需突破文献理解、跨领域推理等关键能力。
