字节跳动Seed团队今日宣布推出新一代形式化数学推理专用模型SeedProver1.5，该模型通过大规模的AgenticRL训练，在推理能力和效率上取得显著进步。与上一代模型相比，SeedProver1.5在16.5小时内针对IMO2025的前5道题目生成了完整可编译验证的Lean证明代码，成绩达到35/42，符合金牌分数线。此外，该模型在Putnam数学竞赛中表现突出，用时9小时对12道赛题中的11道生成了可编译验证的Lean代码。

SeedProver1.5在更系统的评估中表现优异，解决了88%的Putnam历史评估集问题，在硕士数学难度的Fate-H评估集上解决了80%的问题，在博士生数学难度的Fate-X评估集上解决了33%的问题，刷新了形式化数学推理模型在这些评测集上的SOTA表现。技术报告已对外公开，官方计划后续开放API，以供更广泛的研究和应用。