新智元报道
编辑：编辑部
就在刚刚，谷歌 DeepMind 最新的数学模型捧得了 IMO 奥数银牌！它不仅以满分成绩做出了 6 道题中的 4 道，距离金牌只有 1 分之差，而且在第 4 题上只用了 19 秒，解题质量和速度惊呆了评分的人类评委。
AI，已经斩获了 IMO 奥数银牌！
就在刚刚，谷歌 DeepMind 宣布：今年国际数学奥林匹克竞赛的真题，被自家的 AI 系统做出来了。
其中，AI 不仅成功完成了 6 道题中的 4 道，而且每道题都获得了满分，相当于是银牌的最高分——28 分。
这个成绩，距离金牌只有 1 分之遥！
609 名参赛选手中，拿到金牌的只有 58 人
在正式比赛中，人类选手会分两次提交答案，每次限时 4.5 小时。
有趣的是，AI 只用了几分钟便答出了其中一道，但剩下的问题却花了整整三天时间，可以说是严重超时了。
这次立下大功的，是两款 AI 系统——AlphaProof 和 AlphaGeometry 2。
划重点：2024 IMO 并不在这两个 AI 的训练数据中。
AI 工程师 Devin 背后创始人之一 Scott Wu（IOI 三枚金牌得主）感慨道，「当我还是个孩子的时候，奥林匹克竞赛就是我的全部。从来没有想过，仅仅 10 年后，它们就被 AI 解决了」。
今年的 IMO 竞赛上，共有六道赛题，涉及代数、组合学、几何和数论。六道做出四道，让我们感受一下 AI 的水平——
AI 的数学推理能力，震惊评分教授
我们都知道，以前的 AI 在解决数学问题上一直捉襟见肘，原因在于推理能力和训练数据的限制。
而今天携手登场的两位 AI 选手，则打破了这种限制。它们分别是——
- AlphaProof，基于强化学习的形式数学推理新系统
- AlphaGeometry 2，第二代几何解题系统
两位 AI 给出的答案，由著名数学家 Timothy Gowers 教授（IMO 金牌得主和菲尔兹奖得主）和 Joseph Myers 博士（两次 IMO 金牌得主、IMO 2024 问题选择委员会主席），根据规则进行评分。
最终，AlphaProof 正确做出两个代数题和一个数论题，其中一个最难的问题，在今年 IMO 中只有 5 名人类参赛者做了出来；AlphaGeometry 2 则做出了一道几何题。
没有被攻克的，只有两道组合数学题。
Timothy Gowers 教授在评分的过程中，也被深深地震撼了——
程序能够提出这样一个非显而易见的解法，实在令人印象深刻，远超出我对当前技术水平的预期。
AlphaProof
AlphaProof 是一个能够在形式化语言 Lean 中证明数学命题的系统。
它结合了预训练的大语言模型和 AlphaZero 强化学习算法，后者曾自学掌握了国际象棋、将棋和围棋。
形式化语言的一个关键优势，就是可以对涉及数学推理的证明进行形式化验证。然而，由于人类编写的相关数据量非常有限，它们在机器学习中的应用一直受到限制。
相比之下，基于自然语言的方法尽管可以访问大量数据，但却可能产生似是而非、但不正确的中间推理步骤和解决方案。
为了克服这一点，谷歌 DeepMind 研究者通过微调 Gemini 模型，将自然语言问题陈述自动翻译成形式化陈述，建立了一个包含不同难度的形式化问题的大型库，从而在两个互补领域之间架起桥梁。
解题时，AlphaProof 会生成候选的解决方案，并通过在 Lean 中搜索可能的证明步骤，来证明或反驳它们。
每个被找到并验证的证明，都被用于强化 AlphaProof 的语言模型，让它可以在后续解决更难的问题。
为了训练 AlphaProof，研究者证明或反驳了几百万个问题，涵盖了从比赛前几周到比赛期间广泛的难度和数学主题领域。
在比赛期间，他们还应用了训练循环，通过强化自生成的比赛问题变体的证明，直到找到完整的解决方案。
AlphaProof 强化学习训练循环的流程信息图：大约一百万个非正式数学问题由形式化网络翻译成形式化数学语言；接着，求解网络通过搜索这些问题的证明或反驳，并利用 AlphaZero 算法逐步训练自己，以解决更具挑战性的问题
AlphaGeometry 2
AlphaGeometry 的升级版 AlphaGeometry 2，是一个神经符号混合系统，基于 Gemini 的语言模型从头开始训练。
基于比上一代多了一个数量级的合成数据，它能够做出难度更高的几何问题，包括涉及物体运动、角度、比例和距离方程等等。
此外，它还采用了比前一代快两个数量级的符号引擎。当遇到新问题时，它会用一种新颖的知识共享机制，使不同搜索树的高级组合能够解决更复杂的问题。
在今年参赛 IMO 之前，AlphaGeometry 2 已经战绩累累：它能做出过去 25 年 IMO 几何赛题中的 83%，而第一代只能做出 53%。
在这届 IMO 中，AlphaGeometry 2 的神勇速度更是震惊了众人——在接收到形式化问题的 19 秒内，它就把问题 4 做出来了！
问题 4 要求证明∠KIL 和∠XPY 之和等于 180°。AlphaGeometry 2 建议在 BI 线上构造一个点E，使得∠AEB=90°。点E有助于确定 AB 的中点L，形成了许多类似的三角形对，如 ABE ~ YBI 和 ALE ~ IPC，从而证明结论
AI 的解题过程
值得一提的是，这些问题首先会被人工翻译成正式的数学语言，然后才会投给 AI。
P1
一般来说，每届 IMO 试题中第一题（P1）相对来说，是比较容易的。
网友表示，「P1 仅需要高中数学知识就够了，人类选手通常会在 60 分钟内完成」。
IMO 2024 第一题主要考察了实数α的性质，并要求找出满足特定条件的实数α。
AI 给出了正确答案——α是偶整数。那么，它具体是如何解答的呢？
解题第一步，AI 先给出了一个定理，左右两边集合相等。
左边集合表示，所有满足条件的实数α，对于任何正整数n，n能整除从 1 到n的⌊i*α⌋；右边集合表示，存在一个整数k，k是偶数，实数α等于k。
接下来的证明中，分为两个方向。
首先证明右边集合，是左边集合的子集（简单方向）。
然后，再证明左边集合，是右边集合的子集（困难方向）。
直到代码结束时，AI 提出了一个关键等式⌊(n+1)*α⌋ = ⌊α⌋+2n (l-⌊α⌋)，使用等式来证明α必须是偶数。
最后，DeepMind 总结了 AI 在解题过程中，依赖的三个公理：propext、Classical.choice，以及 Quot.sound。
以下是 P1 的完整解题过程：https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html
P2
第二题考察的是，正整数对(a,b)的关系，涉及到最大公约数的性质。
AI 求解的答案是：
定理是对于满足特定条件的正整数对(a,b)，其集合只能包含(1,1)。
AI 在如下的解题过程中，采取的证明策略是，首先证明(1,1) 满足给定条件，然后再证明这是唯一的解。
证明(1,1) 是最终解，使用g=2，N=3。
证明如果(a,b)是解，那么 ab+1 必须整除g。
在这一过程中，AI 使用了欧拉定理，以及模运算的性质进行推理。
最后，去证明a=b=1 是唯一可能的解。
如下是 P2 的完整解题过程：https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html
P4
P4 是一道几何证明题，要求去证明一个特定的几何角度关系。
如上所述，这是由 AlphaGeometry 2 在 19 秒内完成答题，创新纪录。
根据所给的解决方案，与一代 AlphaGeometry 一样，所有解决方案中的辅助点都是由语言模型自动生成的。
证明中，所有的角度追踪都使用了高斯消元法（Gaussian elimination），d(AB)−d(CD)等于从 AB 到 CD 的有向角度（以π为模）。
解题过程中，AI 会手动标注相似三角形和全等三角形对（以红色标注）。
接下来，就是 AlphaGeometry 的解题步骤了，采用了「反证法」去完成。
先用 Lean 完成需要证明命题的形式化，以及可视化几何构造。
证明中的关键步骤，如下所示。
完整解题过程参见下图：https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html
P6
IMO 第六题便是「终极 boss」，探讨了函数的性质，要求证明关于有理数的特定结论。
AI 求解，c=2。
先来看定理声明是，定义了「Aquaesulian 函数」的性质，并声明对于所有这样的函数，f(r) +f(-r)的取值集合最多有 2 个元素。
证明策略是，首先证明对于任何 Aquaesulian 函数，f(r) +f(-r)的取值集合最多有 2 个元素。然后构造一个具体的 Aquaesulian 函数，使得f(r) +f(-r)恰好有 2 个不同的值。
证明当f(0)=0 时，f(x) +f(-x)最多取两个不同的值，并证明不可能存在f(0)≠0 的 Aquaesulian 函数。
构造函数f(x)=-x+2⌈x⌉，并证明它是 Aquaesulian 函数。
最后，再去证明对于这个函数，f(-1) +f(1) =0 和f(1/2) +f(-1/2)=2 是两个不同的值。
以下是完整解题过程：https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html
能做奥数题，但能分清 9.11 和 9.9 谁大吗？
斯坦福大学和红杉的研究员 Andrew Gao 肯定了这次 AI 突破的意义——
关键的是，最新 IMO 试题不包含训练集中。这一点很重要，说明 AI 能够处理全新的、未见过的问题。
而且，被 AI 成功解出的几何问题，由于涉及空间性质（需要直观思维和空间想象力），历来都被认为是极具挑战性的。
英伟达高级科学家 Jim Fan 则发长文表示，大模型是神秘的存在——
它们既能在数学奥林匹克竞赛中获得银牌，又会在「9.11 和 9.9 哪个数字更大」这样的问题上频频出错。
不仅是 Gemini，就连 GPT-4o、Claude-3.5、Llama-3 都无法 100% 正确回答。
通过训练 AI 模型，我们正在探索超越自身智能的广阔领域。在这个过程中，我们发现了一个非常奇特的区域——一个看起来像地球，却充满诡异山谷的系外行星
这看起来很不合理，但我们可以用训练数据分布来解释：
AlphaProof 和 AlphaGeometry 2，是在形式化证明和特定领域的符号引擎上完成训练。在某种程度上，它们在解决专业的奥林匹克竞赛问题更出色，即使它们基于通用 LLM 构建的。 而 GPT-4o 的训练集中，混杂了大量的 GitHub 代码数据，可能远远超过数学数据。在软件版本中，「v9.11 > v9.9」，可能严重扭曲了数据分布。因此，这个错误在某种程度上是可以理解的。
谷歌开发者负责人表示，能够解决困难的数学、物理问题的模型，是通向 AGI 的关键路径，而今天我们在这条道路上又迈出了一步。
另有网友表示，这一周信息量太大了。
参考资料：
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
