IMO 2025 刚刚结束。今年许多 AI 模型参与了这个挑战。以下是我对结果的看法。
大挑战
自从 IMO 大挑战 在 2020 年提出以来，获得 IMO 金奖被视为一个重要的 AI 里程碑，人们对这一目标何时能够实现充满了猜测与争议。我记得在 Neurips 2022 举行的一个大型晚宴上，与会的 AI 研究人员普遍认为，我们距离目标还很远，几位专家甚至表示在 2030 年之前不可能实现。当时 Secret AlphaProof 团队中的某个人打赌将会在 2024 年实现这一目标，结果引来了众人的嘲笑。那时前沿 LLM 还无法处理 更简单的数学难题，未来的方向并不明确。
这也是 Eliezer Yudkowsky 和 Paul Christiano 打赌 的热门话题，其中 EY 的乐观预测是“到 2025 年底有超过 16% 的机会”。此类问题的预测市场也出现了，尤其是 这个关于 manifold 的。
今年 IMO 大挑战落下帷幕。Google DeepMind 和 OpenAI 宣布他们的模型达到了金奖标准。
我与这个问题的联系
我在 Google DeepMind 花了将近两年时间研究这个问题，最终我们在 IMO 2024 后宣布了 AlphaProof。加上 AlphaGeometry，它获得了银奖表现，离金奖只差一分。这对于 AI 和数学界都是一个巨大的震惊。
这次未能击败 IMO 大挑战有几个原因：
- 系统未能获得金奖。
- 某些题目的解决时间过长，最长的花费了将近 3 天，而人类只给 4.5 小时。
- 题目最初是由人类将其从英语翻译为 Lean 的。
不过我们感觉真的非常接近。
关于 (1)，我们离金奖只差一分。今年共有 6 道题，每题 7 分——系统得到了 28 分，而当年的金奖最低分是 29。尽管这次题目的分布相对于系统的强项有些不幸运。系统在组合数学方面表现最弱，而 AlphaProof 未能解决的两个问题（P3 和 P5）都是组合数学问题。历史上，组合数学问题的数量不到一半的时间里都会出现。
关于 (2)，这方面可以通过一些努力来解决。而 (3) 对于 AlphaProof 已解的题目，系统本身也可以成功实现自动形式化（尽管这在竞赛环境中未被使用）。
这促使 AlphaProof 团队从 IMO 转向更加困难的数学问题，也让我部分原因转向 Anthropic 从事行动编码工作。因此，看着多个 AI 公司竞争，争夺今年的金奖，令我感到十分有趣——「我虽不关心，但并非无动于衷」（视频）。
今年的结果
如果让我预测 AI 模型在今年 IMO 的表现，我会对至少某些 AI 系统获得金奖持乐观态度。考虑到去年的结果，某个基于 Lean 的系统获奖几乎是必然的。
但考虑到大实验室对一般 LLM 推理的关注，再次使用 Lean 可能会分散注意力。Google DeepMind 和 OpenAI 在 2024 年测试过一般 LLM，但当时这些系统的能力不足以实现此目标。从那以后，进展的速度令人惊叹，但我仍然只会给出一个 50% 的机会认为一个一般 LLM 会获得金奖。
题目情况
今年的题目 分为 2 道组合问题，2 道数论问题，1 道几何问题和 1 道函数不等式（尽管有几道题目属于多个分类）。和去年一样，我发现 Dedekind cuts 的 YouTube 频道非常有助于理解这些问题和解决方案。为了遵循比赛地点的主题，今年的题目中包含了一些与澳大利亚相关的参考，包括“inekoalaty”这一术语。
参赛者普遍认为今年的题目比去年容易，金奖的最低分为 35/42。今年有很多学生的得分为 35，因此共颁发了 72 个金奖（与去年的 58 个相比）。这实际上降低了金奖的最低分，加上最低分刚好与题目边界相重合（即 5/6 恰好落在分界线上），使得 AI 尝试的成功率上升。
OpenAI
OpenAI 是 第一个宣布 成绩的，他们在周五晚上完成。过程完全在自然语言中进行，没有使用工具，并且在 4.5 小时内完成。
他们的证明可以在 这里找到。这些证明 相当奇怪。例如，模型非常简洁，尽可能使用缩写，没有完整句子甚至正确语法的书写。它还会不时插入一些自我鼓励的词语，比如“很好”或者“完美”。
“全了。正好。完成。”
—— OpenAI 的 IMO 模型，在完成 P5 时说。
他们在 这篇访谈中 谈到了一些他们的方法。他们表示，他们找到了在难以验证的任务上进行 RL 的新方法。看起来这只是一支非常小的团队在这个项目上工作。
Google DeepMind
Google DeepMind 在 OpenAI 宣布之后 随后在周一宣布他们的结果。同样是在自然语言中，并且在 4.5 小时内完成。他们还让 IMO 对他们的证明进行审查并确认其金奖表现。
他们的证明可以在 这里找到。这些证明看起来比 OpenAI 的更加精炼，几乎与优秀的人类证明无法区分。
从致谢中可以看出，有很多人参与了这个项目，包括许多来自 2024 年尝试的团队。看起来他们采用了几种技术的结合，包括并行测试时的计算、RL、翻译的形式化证明、基于之前的解决方案的 RAG 以及提示/支撑。他们还发布了一个 轻量版 系统，在非数学推理任务上也有不错的表现。
形式系统
还有几个形式系统也宣称获得了金奖。
字节跳动宣布了 Seed-Prover，该系统解决了 P1-P5，但耗时 4 天。 这些证明 数量惊人，例如 P1 的证明超过 4000 行。他们的技术同时依赖形式和自然语言数据，测试时的扩展使用了库学习和测试时的猜想生成。
Harmonic，一家以 Lean 为重点的初创公司，也 声称获得金奖。 他们的证明 可读性更高，但仍然非常冗长，例如 P1 超过 1400 行。我曾认为去年 AlphaProof 的 P6 解决方案 已经很长了，而那只有 300 行。他们没有分享太多关于他们协议的细节——听起来他们的过程可能比字节跳动运行的时间更长，目前还不清楚使用了什么模型来生成答案，以及是否训练了自己的基础模型。
我对结果的看法
OpenAI 和 Google DeepMind 的结果令人印象深刻。尤其是，如果 OpenAI 关于这种针对难以验证任务的 RL 方法的说法足够广泛，可以扩展到其他困难任务，那看起来非常有希望。从证明中可以看出，模型经过了积极的 RL 调整。我的猜测是，它是一个评卷模型，经过训练利用某种形式的参考解决方案，结合一些 RL 技巧以防止奖励黑客，但我可能会错。
关于 AI IMO 解决方案的可信打分 作为 Google DeepMind 2024 IMO 项目的负责人之一，我亲身经历了评估 AI 解决方案的过程，发现其中的细节比想象的要复杂得多。
理想情况下，会有一个单一的系统，并在比赛前冻结。题目输入，该系统进行思考，并在某一时刻输出答案。答案将由 IMO 评审进行评分，并根据情况给予相应的分数。
但在实践中，这种严格的标准是非常难以实现的，我怀疑今年的任何系统都达到了这一标准。团队可能进行的一些看似合理的操作可能会违反这一协议：
- 手动运行和重启命令，修复出现的错误。
- 切换计算、运行时间和其他参数，可能是根据题目的分布调整。
- 事先不明确所使用的协议，使得许多决定取决于模型的实际表现。例如，如果某个团队未能在 4.5 小时内获得 IMO 金奖，那么他们很可能会在 4.5 小时内继续运行，重新评估并报告结果。
- 评估多个系统，仅报告表现最佳的结果。
Terry Tao 在 一篇好文章中 讨论了这一点。理想情况下，这应在正式的比赛环境中进行。若无法做到，通过外部评分者和监考人员（正如我们在 2024 年所做的）将增加很多价值。从这个角度来看，Google DeepMind 的声明是最可信的，因为 (a) 它得到了外部的验证，且 (b) 这是第二次在相同问题上由大型团队进行的尝试，有机会完善协议。
在某种意义上，这些都是小问题——拥有一个 AI 系统，使这些问题变得触手可及才是真正的成就，其余则是无关紧要的细节。
关于基于 Lean 的证明者，查看字节跳动发布的基准数据，证明的实力与去年 AlphaProof 相似。但现在我们拥有现成的基础模型，可以 显然进行支撑 ，在通用语言中引导出金奖级的解决方案，因此再通过数天的计算使用 Lean 来解决相同问题就更难以合理化了。
关于 AI 研究的本质
IMO 的故事突显了当前 AI 研究中的几个方面，我想对此做一些深入探讨。
能量与势头
目前 AI 的势头十分强劲，似乎只要足够多人投入精力，我们就能解决几乎所有问题。几乎没有什么东西是不受推动的。
大多数研究突破都不特别
OpenAI 和 Google DeepMind 使用截然不同的技术达到了完全相同的结果。字节跳动在 Lean 证明方面达到了与去年 AlphaProof 相似的水平，但其采用的方法非常不同。
很多 AI 的进展都是如此。许多好的想法应该都能奏效，但没有实验室有资源尝试所有想法。此外，有效的技术可能是路径依赖的——它们最适合特定实验室的设置/基础设施/人员。而随着规模的增加，能力正在以高涨的潮流不断上升，改变可能有效的方法的格局。
确实存在一些被称为“瓶颈”的突破，大家需要统一在同一个见解上以做出进展（一个显而易见的例子就是 transformers）。但是许多其他的“突破”并不特殊。
未来
我预计明年将继续对 AI 在 IMO 中的尝试产生一定兴趣。前沿 LLM 可能能够毫不费力地获得金奖，无需任何专业化。
与数学家交谈时，我有种感觉，解决一些非平凡（但并不是特别激动人心）的开放问题在当前能力下“并不难”。我预计这将在接下来的 6 个月内发生。
Lean 在数学 AI 中仍然发挥着重要作用。在某些方面，随着我们逐渐转向越来越困难的问题，Lean 的优势愈发明显，在这些领域，很难判断证明的正确性。目前的定理证明研究范式是“Lean 专用基础模型，大量测试时计算”。当大型基础模型在自然语言数学证明上效果不佳时，这听起来是合理的；额外的计算更适合用于生成更加可信的证明候选，利用较小的专门模型，因为 Lean 可以告诉你你是否找到了答案。我认为现在恰好翻转这一点，将这两种技能结合到同一个模型中是合理的。
在过去 3 年中，我亲自评估了多次 LLM 在 IMO 问题上的表现，他们的进展令我震惊。我还记得在 2023 年中，我手动审查了 Gemini 和 GPT-4 的每个最近数值解的 IMO 问题，发现只有一个问题值得部分分数（其余均为零）。而仅仅两年后，获得 5/6 的金奖代表了令人难以置信的进展速度。如果你一直专注于如何改善模型在某个不擅长的领域，可能会忽略更大的图景。
我在“智能体编码”领域中也切身感受到 AGI 的存在。当前这一批模型在各方面都领先于以往的任何模型，并且我可以开始勾勒出我们明年及其后怎样的前景。这将在许多其他领域发生，如果你尚未在自己的领域中感受到这一点，那么这只是时间问题。
原文链接：https://rishimehta.xyz/2025/08/09/imo-2025-results.html