时令 发自 凹非寺

量子位 | 公众号 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” 通过应用生成的引理来生成主要证明。

这种方法具有几个关键优势：

2、由于引理是模块化的，它们可以独立编译、独立存储和自由组合。

3、证明引理的过程可能为模型提供灵感，以证明其他未证引理或解决主要问题。

为了实现Seed-Prover的工作流程，研究人员为每个难题建立了一个

引理池

，存储来自所有推理运行的综合数据，包括引理陈述、引理名称、完整证明、证明难度和依赖关系。

根据可用的推理资源和问题难度，字节还开发了三个级别的策略：轻量推理、中等推理和重量级推理。

由于Lean在几何支持方面存在不足，Seed-Prover集成了一个专用的几何推理引擎

Seed-Geometry

。

它采用了前向链推理的引擎架构：即系统通过检查适用的规则来推导所有已知事实，直到得出结论。

基于上述工作，Seed-Geometry建立了一个包含2.3亿个需要辅助构造的独特几何问题的库。

这是通过利用过去20多年数学奥林匹克竞赛的统计数据，并在其专用领域特定语言定义的几何空间中进行广泛搜索实现的。

基于这一专属几何数据训练得到的Seed模型，成为了一个高效的

神经-符号混合几何证明器

。

它可以补全缺失的辅助构造元素，并借助几何推理引擎，按步骤进行前向推理，最终完成整个几何问题的形式化证明。

达IMO金牌水准

研究团队使用Seed-Prover与Seed-Geometry参加了IMO 2025，成功证明了6道题中的5道，达到了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题——IMO中表现最差的两道题中的一道。

除此之外，对于MiniF2F测试集，Seed-Prover达到了几乎百分百的正确率。

参考链接：

[2]https://www.alphaxiv.org/pdf/2507.23726

一键三连