时令 发自 凹非寺
量子位 | 公众号 QbitAI
不仅能达IMO银牌水准，更能解决普特南数学竞赛难题，甚至超越顶尖模型o4-mini！
字节发布全新复杂数学解决模型——Seed-Prover。
该模型全面超越了谷歌的AlphaGeometry2，并在MiniF2F数据集上实现了惊人的100%正确率。
不仅如此，Seed-Prover还展现了其卓越的泛化能力：
-
成功解决了78.1%的历年IMO难题； -
在普特南数学竞赛中的成绩达到其他主流模型的4倍； -
在MiniCTX-2数据集上，以81.8%的高正确率远超基准模型o4-mini。
对此，前谷歌成员Deedy Das惊叹道：字节真不愧是唯一一家专为IMO发表完整论文的AI实验室！
Seed-Prover模型框架
Seed-Prover是一个专注于使用Lean 4进行形式化推理的大型语言模型。
Lean 4允许用户精确定义数学对象和定理，并通过机器自动验证推理步骤的严谨性与正确性。
相较于先前的研究，Seed-Prover最显著的区别在于采用了引理式证明作为证明范式，从而将引理置于推理过程的核心。
简单来说，就是在进行推理时，先要求模型生成一些有用的引理，每个引理由 “lemma” 关键字引入 ，然后再使用 “theorem” 通过应用生成的引理来生成主要证明。
这种方法具有几个关键优势：
1、它可以清晰地识别已成功证明的引理和需要进一步完善的引理。
2、由于引理是模块化的，它们可以独立编译、独立存储和自由组合。
3、证明引理的过程可能为模型提供灵感，以证明其他未证引理或解决主要问题。
为了实现Seed-Prover的工作流程，研究人员为每个难题建立了一个引理池，存储来自所有推理运行的综合数据，包括引理陈述、引理名称、完整证明、证明难度和依赖关系。
根据可用的推理资源和问题难度，字节还开发了三个级别的策略：轻量推理、中等推理和重量级推理。
由于Lean在几何支持方面存在不足，Seed-Prover集成了一个专用的几何推理引擎Seed-Geometry。
它采用了前向链推理的引擎架构：即系统通过检查适用的规则来推导所有已知事实，直到得出结论。
此外，Seed-Geometry还具有反向追踪事实依赖关系的能力，能够识别一个几何问题中最小的依赖关系结构，从而将问题本身的上下文与解决该问题所需的辅助构造有效区分开来。
基于上述工作，Seed-Geometry建立了一个包含2.3亿个需要辅助构造的独特几何问题的库。
这是通过利用过去20多年数学奥林匹克竞赛的统计数据，并在其专用领域特定语言定义的几何空间中进行广泛搜索实现的。
基于这一专属几何数据训练得到的Seed模型，成为了一个高效的神经-符号混合几何证明器。
它可以补全缺失的辅助构造元素，并借助几何推理引擎，按步骤进行前向推理，最终完成整个几何问题的形式化证明。
达IMO银牌水准
研究团队使用Seed-Prover与Seed-Geometry参加了IMO 2025，完整解决了6道题中的4道以及一道题的部分证明，在比赛规定时间内达到了IMO银牌水准。
根据IMO-AG-50的统计方法，在2000年至2024年IMO几何问题中，Seed-Geometry (SG) 解决了43道题，比AlphaGeometry 2 (AG2) 多解决1道。
对于2000年至2022年难度大的多的IMO候选题中的几何题，AlphaGeometry 2解决了19道，而Seed-Geometry解决了22道。
此外，值得注意的是，Seed-Geometry还在2秒内解出了IMO 2025第2题。
除此之外，对于MiniF2F测试集，Seed-Prover达到了几乎百分百的正确率。
（文：量子位）