白交西风发自凹非寺
量子位公众号 QbitAI
刚刚，大模型再次攻下一城！
谷歌 DeepMind 宣布，他们数学 AI“摘得”IMO（国际数学奥林匹克竞赛）银牌，并且距离金牌仅一分之差！
是的，没有听错！就是难到绝大多数人类的奥数题。要知道今年 IMO 全部 609 名参赛者，也仅有 58 位达到了金牌水平。
此次，谷歌 AI 解决了 2024 IMO 竞赛 6 道题目中的 4 道，而且一做一个满分，总共获得 28 分。（满分 42 分，金牌分数线 29 分）
其中第四题几何题，AI 仅仅用时 19 秒？！
而号称本届最难的第六题，今年仅有五名参赛者拿下，它也完全答对。
此次的成绩还得到了 IMO 组委的专业认证——由 IMO 金牌得主、菲尔兹奖获得者 Timothy Gowers 教授和两届 IMO 金牌得主、2024 IMO 问题选择委员会主席 Joseph Myers 博士进行评分。
Timothy Gowers 教授直接惊叹：远远超过我认知的最先进水平。
来康康是如何做到的？
谷歌拿下 IMO 银牌，Alpha 家族新成员问世
此次拿下 IMO 银牌的是谷歌两位 Alpha 家族成员，他们各自数业有专攻。
- AlphaProof，Alpha 家族新成员，基于强化学习的形式数学推理系统。
- AlphaGeometry 2，此前 AlphaGeometry 改进版，专门用于解决几何问题。
先来认识一下新成员——AlphaProof。
它是一个自训练系统，能用形式语言 Lean 来证明数学陈述。它能将预先训练好的语言模型与 AlphaZero 强化学习算法结合在一起。
团队通过微调 Gemini，能自动将自然语言陈述转换为形式语言 Lean 陈述，由此创建了一个大型数学题库。
当遇到问题时，AlphaProof 会生成解决方案候选，然后通过搜索 Lean 中可能的证明步骤来证明或反驳这些候选。
每个找到并验证的证明都会用于强化 AlphaProof 的语言模型，从而提高其解决后续更具挑战性的问题的能力。
在比赛的前几周内，它就这么循环往复地用数百万个 IMO 级别题目进行了训练。
比赛期间也应用了训练循环，不断强化自身证明，直到找到完整的解决方案。
再来了解一下进化之后的AlphaGeometry 2。它是一个神经-符号混合系统，其中语言模型基于 Gemini。
它的前身 1.0 今年还登上了 Nature：无需人类演示达到 IMO 金牌选手的几何水平。
跟上一个版本比，它使用了更大一数量级的合成数据进行从头训练。而它采用的符号引擎比其前代快两个数量级。当遇到新问题时，会使用一种新的知识共享机制来实现不同搜索树的高级组合，以解决更复杂的问题。
在正式比赛之前，它就已经可以解决过去 25 年所有 IMO 几何问题中的 83%，而其前身的解决率仅为 53%。
今年 IMO 赛事中，它仅用了 19 秒就完成了第四个问题。
接着就来看看，此次 IMO 这两位是如何配合发挥的。
首先，问题被手动翻译成正式的数学语言，以便系统理解。
我们知道人类比赛时，分两次提交答案，每次有 4.5 个小时。
而谷歌这两个系统先是在几分钟内解决了一个问题，其他问题则是花了三天时间。
最终，AlphaProof 通过确定答案并证明其正确性，解决了两道代数题和一道数论题。
其中包括比赛中最难的一道题，也就是，今年的 IMO 比赛中仅有五名选手解出的第六题。
AlphaGeometry 2 解决了几何问题，而两道组合问题仍未解决。
除此之外，谷歌团队还试验了一种基于 Gemini 的自然语言推理系统。换言之，无需将问题翻译成形式语言，并且可以跟其他 AI 系统结合使用。
团队表示，他们接下来还会探索更多用于推进数学推理的 AI 方法。
而关于 AlphaProof 的更多技术细节，也计划很快发布。
网友：不懂数学但大受震撼
看到这两个系统的表现，网友们纷纷表示“不懂数学但大受震撼”。
AI 程序员 Devin 团队 Cognition AI 联合创始人 Scott Wu 表示：
这样的结果真是令人惊叹。小时候，奥林匹克竞赛就是我的全部。从未想过它们会在 10 年后被人工智能解决。
OpenAI 科学家 Noam Brown 也开麦祝贺：
不过，也有网友表示，如果按照标准比赛时间（竞赛分两天进行，每天四个半小时，每天解决三个题），这两个 AI 系统实际上只能解决 6 个问题中的一个。
这一说法立刻得到了部分网友反驳：
在此情境中，速度不是主要关注点。如果浮点操作次数（flops）保持不变，增加计算资源会缩短解决问题所需的时间。
针对这一点，也有网友疑问道：
两个 AI 系统没能解答出组合题，是训练的问题还是计算资源不够，时间上不行？或者还存在其他限制吗？
Timothy Gowers 教授发推文给出了他的看法：
如果允许人类参赛者在每个问题上花费更多时间，他们的得分无疑会更高。然而，对于 AI 系统来说，这已经远超以往自动定理证明器的能力；其次，随着效率的提高，所需时间有望进一步缩短。
不过前两天大模型还困于“9.11 和 9.9 哪个数字更大？”这么一个小学题，怎么这一边大模型又能解决奥数级别的难题了？！
失了智，然后现在怎么又灵光乍现，恢复了智？
英伟达科学家 Jim Fan 给出解释：是训练数据分布的问题。
谷歌的这个系统是在形式证明和领域特定符号引擎上进行训练的。某种程度上说，它们在解决奥林匹克竞赛方面高度专业化，即使它们建立在通用大模型基础上。
而像 GPT-4o 的训练集中混有大量 GitHub 代码数据，可能远远超过数学数据。在软件版本中，“v9.11>v9.9”，这可能会严重扭曲分布。所以说，这个错误还算说得过去。
对于这一奇怪现象，他将其形容为
我们发现了一个非常奇特的区域，就像一颗看起来像地球却遍布奇异山谷的系外行星。
还有热心的网友 cue 了下 OpenAI，也许你们也可以尝试……
对此，奥特曼的回复是：
参考链接：
[1]https://x.com/googledeepmind/status/1816498082860667086?s=46
[2]https://x.com/jeffdean/status/1816498336171753948?s=46
[3]https://x.com/quocleix/status/1816501362328494500?s=46
[4]https://x.com/drjimfan/status/1816521330298356181?s=46
[5]https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
