字节跳动发布新一代形式化数学推理模型 Seed Prover 1.5：Seed Prover1.5登顶数学AI
2025-12-25 10:40
87
字节跳动Seed团队发布形式化数学推理模型Seed Prover1.5，在推理能力和效率上取得显著提升。该模型采用全新的Agentic Prover架构，结合自然语言推理与形式化证明，并能在证明过程中灵活调用数学库和Python代码等工具。在2025年国际数学奥林匹克（IMO）和普特南数学竞赛中表现出色，分别达到金牌分数线和在9小时内完成12题中的11题，刷新了多个评测集的最佳表现。
什么是形式化数学推理？
形式化数学推理（Formal Theorem Proving）指的是将数学问题和证明过程，转化为可由计算机严格校验的形式化语言（如Lean），并在逻辑系统中逐步构造、验证完整证明。
与自然语言解题不同，形式化推理要求：
每一步推理必须逻辑完备
证明结果必须可编译、可验证
不允许任何“直觉跳步”
这类任务长期被认为是人工智能中难度最高的推理问题之一。
核心创新一：Agentic Prover架构
Seed Prover 1.5的核心升级是引入Agentic Prover架构，即以“智能体”为中心组织整个证明流程。
在该架构下，模型不再只是被动生成证明文本，而是可以：
自主调用数学库（如Lean的Mathlib）进行定理和引理检索
执行代码与计算工具，辅助复杂代数或数值验证
在推理过程中动态调整策略，逐步推进证明
这种“工具增强+主动决策”的方式，使模型具备更接近人类数学家的问题求解模式，而非单一的语言生成器。
核心创新二：大规模Agentic强化学习
在训练层面，Seed Prover 1.5采用了大规模Agentic强化学习（RL）：
模型与形式化证明环境持续交互
每一步证明是否通过验证都会形成明确反馈
通过强化学习不断优化证明策略与搜索路径
相比仅依赖监督数据的方法，强化学习显著提升了模型在长链推理、复杂定理构造上的稳定性与成功率。
核心创新三：Sketch Model证明分解机制
为应对复杂、冗长的数学证明，Seed Prover 1.5引入了Sketch Model（证明草图模型）：
先生成高层次证明结构（Proof Sketch）
将原问题拆解为多个子引理
对子引理进行并行证明与验证
最终合并为完整形式化证明
该机制有效降低了长证明中错误累积的风险，也提升了整体搜索效率，是模型在高难度题目中取得突破的重要原因之一。
评测表现：多项国际竞赛刷新SOTA
IMO 2025（国际数学奥林匹克）
在IMO 2025形式化测试中：
Seed Prover 1.5在16.5小时内完成前5道题的Lean形式化证明
按官方评分标准折算得分35/42
达到IMO金牌分数线水平
这是当前已公开系统中，在IMO难度下取得的最高形式化推理成绩之一。
Putnam数学竞赛评测
在Putnam竞赛相关测试中，Seed Prover 1.5表现同样突出：
Putnam 2025赛题中，12题成功解决11题
在Putnam历史题集上，整体解决率达到88%
在更高难度评测集：
Fate-H（硕士难度）：80%
Fate-X（博士难度）：33%
这些结果显示模型已具备稳定处理本科到研究生阶段高难数学问题的能力。
0
好文章，需要你的鼓励