字节跳动 seed 团队推出新一代形式化数学推理专用模型 seed prover 1.5，通过大规模的 agentic rl 训练，其推理能力和推理效率取得显著进步。相比上一代模型，seed prover 1.5 在 16.5 小时内，针对 imo 2025 的前 5 道题目生成了完整可编译验证的 lean 证明代码，换算成绩为 35/42，达到此前 imo 评分标准的金牌分数线。
更系统的评估中，Seed Prover 1.5 在完整的 Putnam 历史评估集上解决了 88% 的问题，在代表硕士数学难度的 Fate-H 和代表博士生数学难度的 Fate-X 评估集上，分别解决了 80% 和 33% 的问题，刷新了形式化数学推理模型在这几个评测集上的 SOTA 表现。
Seed Prover 1.5 针对 FATE-H 问题调用工具示例：
技术报告：https://arxiv.org/abs/2512.17260Lean
证明代码：https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver-1.5/Putnam2025.zip
源码地址：点击下载
