谷歌AI一分之差痛失IMO金牌，19秒做一题碾压人类选手，几何AI超进化震撼评委

AI，已经斩获了IMO奥数银牌！

就在刚刚，谷歌DeepMind宣布：今年国际数学奥林匹克竞赛的真题，被自家的AI系统做出来了。

其中，AI不仅成功完成了6道题中的4道，而且每道题都获得了满分，相当于是银牌的最高分——28分。

这个成绩，距离金牌只有1分之遥！

609名参赛选手中，拿到金牌的只有58人

在正式比赛中，人类选手会分两次提交答案，每次限时4.5小时。

有趣的是，AI只用了几分钟便答出了其中一道，但剩下的问题却花了整整三天时间，可以说是严重超时了。

这次立下大功的，是两款AI系统——AlphaProof和AlphaGeometry 2。

划重点：2024 IMO并不在这两个AI的训练数据中。

其实，早在今年1月份，谷歌DeepMind的第一代AlphaGeometry就登上了Nature。当时，它做出了IMO 30个几何题中的25道。

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。

AI IMO