人工智能在数学推理的赛道上再次迎来里程碑式突破。字节跳动Seed AI团队最新推出的数学大模型Seed Prover1.5，在国际数学奥林匹克（IMO）模拟测试中一举夺金，以35分的高分成绩成功跻身金牌行列，成为继谷歌Gemini之后第二个达到该成就的AI系统，标志着AI向复杂抽象思维领域迈出了坚实一步。
据悉，Seed Prover1.5在处理IMO2025全部六道题目时，仅用16.5小时便完成了前五题的严格形式化证明，唯一失分题目的解答也接近完整。相较之下，字节此前版本的模型需耗时近三天才解出四题，最终止步银牌。此次效率与准确率的双重飞跃，不仅体现了技术迭代的速度，更重新定义了AI解决高阶数学问题的能力边界。
这一跃迁背后，是强化学习策略的大规模应用。团队通过构建密集的训练环境，使模型在定理证明任务中的成功率从初始阶段的约50%稳步提升至接近90%。不仅如此，该模型还在极具挑战性的美国Putnam数学竞赛中创下新纪录，进一步验证了其在多样化数学场景下的泛化能力与稳定性。
技术层面，Seed Prover1.5引入了两项关键架构创新：Agentic Prover与Sketch Model。前者基于Lean等可验证的形式化语言体系，实现逻辑链条的机器自检，确保每一步推导均可追溯、可验证。为增强推理灵活性，系统被赋予调用外部工具的能力，例如实时检索Mathlib数学库或运行Python脚本辅助数值计算，极大拓展了解题路径的广度。
而Sketch Model则借鉴人类数学家的思维习惯，允许模型先以非正式方式“打草稿”——即构建直觉性论证框架，提出中间引理并规划证明路线图，再逐步转化为严谨的形式证明。这种“先构思后精修”的双阶段机制，结合混合奖励信号的强化学习框架，显著提升了模型对长程逻辑依赖的掌控力，有效缓解了传统端到端模型易出现的推理断裂问题。
分析人士指出，Seed Prover1.5不仅是算法工程上的胜利，更预示着AI或将深度参与未来数学发现与教学变革。当机器开始理解并创造数学证明，其影响将远超技术圈层，触及科研范式与知识生产方式的根本转变。
论文地址：https://arxiv.org/pdf/2512.17260
