字节跳动 Seed Prover 取得 IMO 2025 银牌分数

字节跳动 Seed 团队受 IMO（国际数学奥林匹克竞赛）官方邀请参加了 IMO 2025 比赛，我们的形式化数学推理专用模型 Seed Prover 通过 3 天的尝试，完整解决了 6 道题目中的 4 道以及一道题的部分证明，IMO 官方认证 Seed Prover 的成绩为 30 分，达到了银牌的分数（六道题得分为 2/7/7/7/7/0）。团队在赛后进行了额外的尝试，完整证明了前 5 道题目。

Seed Prover 基于 Lean 验证器构建，通过多阶段强化学习训练完成。其通过自然语言思考和形式化代码的交互进行数学题目证明，从而保证证明过程 100% 可靠。借助长链思维推理，并通过多智能体进行测试时算力拓展，Seed Prover 能针对一道数学题进行持续数天、深度且广泛的思考。

除了在 IMO 中的亮眼表现，Seed Prover 还在多个基准测试中刷新了形式化数学推理的最高水平。

IMO 2025 题目解决情况 

Seed Prover 解决 4 道 IMO 2025 赛题共耗时三天。答题前，题目形式化的部分由人进行翻译以保证题目的准确性。最终，Seed Prover 在 IMO 第一天的竞赛题中解决了第 2 题（几何）和第 3 题（数论），在第二天的竞赛题中解决了第 4 题（数论）和第 5 题（组合/代数）。Seed Prover在赛后继续搜索，证明出了第 1 题（组合题）。

具体解题情况如下：

• 第 1 题（组合）：Seed Prover 在比赛中只正确进行了构造，在赛后通过 4 天的搜索完成了 4000 行的证明。

• 第 2 题（几何）：由 Seed Geometry 子系统在 2 秒内自动生成推理并验证了证明。

• 第 3 题（数论）：由 Seed Prover 通过 3 天推理完成证明，包含 2000 行形式化代码。

• 第 4 题（数论）：同样耗时 3 天完成证明，包含 4000 行形式化代码。

• 第 5 题（组合/代数）：耗时 1 天完成证明，与公开的人类解法存在差异。

上述问题的完整形式化证明以及对应的自然语言翻译如下：

第 1 题证明：https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/imo2025/p1.lean

第 2 题证明：https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/imo2025/p2_proof.pdf

第 3 题证明：https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/imo2025/p3.lean

第 4 题证明：https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/imo2025/p4.lean

第 5 题证明：https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/imo2025/p5.lean

Seed Prover 测试时算力扩展设置 

Seed Prover 的成功源于多阶段强化学习训练，这提升了其针对复杂数学问题的长链思维推理能力，并实现了与 Lean 验证器的多样化交互。另一个重要因素在于 Seed Prover 如何扩展测试时推理，为此团队设计了多层次的测试时扩展策略：

轻量级

先前的研究通过 Pass@K 来评估配备长链思维推理的大语言模型在自动定理证明上的表现。团队发现，利用 Lean 编译器信息结合模型总结能力来迭代改进证明，能够突破单次推理的 token 预算限制，并显著提升证明能力。

Seed Prover 的轻量级测试时扩展设置为每个证明最多迭代 8 次，并在 Pass@8 标准下进行评估，此过程可在 1 小时内完成。在轻量级设置下，Seed Prover 能够证明如 IMO 2022 P2（MOHS 难度=15）难度的题目，而如果不允许使用 Lean 编译器信息进行证明迭代，IMO 2022 P2 则需要在 Pass@8192 的标准下才能被证明。

中量级

要证明一道高难度竞赛题，其证明过程可能冗长且复杂。Seed Prover 的中等量级测试时扩展设置包含内层优化过程和外层优化过程。外层优化过程与轻量级设置相同，即对原始问题的证明进行优化。内层优化过程则尝试证明外层优化过程中未能解决的困难引理，这为证明的每一个引理都提供了足够的 token 预算。

在该设置下，Seed Prover 能够解决难度更高的题目，如 IMO 2003 P6（MOHS 难度=35 ）和 IMO 2025 P5，最终的证明代码可超过 1000 行。此设置的运行时间从数小时到数天不等。

重量级

中等量级设置让 Seed Prover 能够深入思考证明中的每个细节，但不能广泛地探索围绕给定问题的新猜想。在重量级推理设置下，系统创建了一个包含给定问题的猜想池和一个空的引理池。

在推理过程中，Seed Prover 会尝试证明或反驳猜想池中的每个问题。它能够利用引理池和 Lean 编译结果来优化证明。一旦某个猜想被证明，就会被移入引理池。如果某些问题难以证明，Seed Prover 会创建可能有助于证明这些难题的新猜想并加入猜想池。经过数天的思考，引理池可能会包含数千条有趣的数学事实。系统会根据引理的证明难度和相关性对引理池进行评估，选取数百条最有价值的引理来帮助系统完成给定问题的证明。IMO 2025 P3 以及 IMO 2025 P4 就是在重量级设置下被证明的。

Seed Prover 多基准测试结果

为了将 Seed Prover 与此前最先进的技术进行对比，团队在多个形式化推理数据集上对 Seed Prover 进行了评估。

Seed Prover 成功证明了 79% 的此前已形式化的 IMO 题目，解决了 MiniF2F 基准测试中绝大部分问题，同时解决了北美大学级别数学竞赛 Putnam 历史赛题中超过一半的问题。Seed Prover 还在多个基准测试中展现出优势，包括 CombiBench 和 MiniCTX-v2。这表明 Seed Prover 并非仅擅长高中竞赛题，而是能应对广泛的数学概念。

数据结果截至 7 月 22 日

总结与展望 

我们感谢 IMO 组委会邀约字节跳动 Seed 团队参与答题，并帮助阅卷和组织评分。本次披露的 Seed Prover 在 IMO 2025 中取得的最终分数，在发布前与IMO 组委会进行了确认。

Seed Prover 在数学竞赛题中的表现，展现了将大语言模型与形式化验证相结合的潜力。团队采取的推理时间扩展策略通过深度且广泛的思考，显著提升了系统性能。不过，竞赛数学并不能代表所有的数学领域，团队未来的目标是在更广泛的数学课题上进行探索。