字节跳动Seed Prover 1.5发布：刷新数学推理纪录，IMO金牌水平证明生成

字节跳动Seed团队于12月24日正式发布形式化数学推理专用模型Seed Prover 1.5，该模型在多项国际数学竞赛评测中刷新性能纪录。据技术报告显示，该模型在16.5小时内针对2025年国际数学奥林匹克（IMO）前5道题目生成了完整可编译验证的Lean证明代码，换算成绩为35/42分，达到IMO金牌分数线标准。此外，Seed Prover 1.5在普特南数学竞赛中成功解决11道题目，并在MiniF2F数据集实现100%正确率，其泛化能力显著超越主流基准模型。

新一代模型采用Agentic Prover架构，结合自然语言推理与形式化证明优势，可灵活调用Mathlib数学库及Python代码辅助验证。相比前代模型，其推理效率提升约4倍，尤其在复杂定理证明场景展现出突破性进展，包括解决78.1%的历年IMO难题，以及在MiniCTX-2数据集上取得81.8%的正确率。

字节跳动表示，Seed Prover 1.5的技术报告已通过开源平台发布，并将于近期开放API接口，供数学及AI研究社区进行实验验证。该模型的推出标志着形式化数学推理领域的重要进展，其应用潜力涵盖自动定理证明、数学教育辅助及科研工具开发等场景。团队特别强调，开放API旨在促进学术合作，推动数学与人工智能的交叉研究发展。