谷歌DeepMind的AI系统在最新的国际数学奥林匹克竞赛(IMO)上取得了惊人的成绩。

就在刚刚,谷歌DeepMind最新的数学模型捧得了IMO奥数银牌!它不仅以满分成绩做出了6道题中的4道,距离金牌只有1分之差,而且在第4题上只用了19秒,解题质量和速度惊呆了评分的人类评委。

AI,已经斩获了IMO奥数银牌!
就在刚刚,谷歌DeepMind宣布:今年国际数学奥林匹克竞赛的真题,被自家的AI系统做出来了。
其中,AI不仅成功完成了6道题中的4道,而且每道题都获得了满分,相当于是银牌的最高分——28分。
这个成绩,距离金牌只有1分之遥!
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
609名参赛选手中,拿到金牌的只有58人
在正式比赛中,人类选手会分两次提交答案,每次限时4.5小时。
有趣的是,AI只用了几分钟便答出了其中一道,但剩下的问题却花了整整三天时间,可以说是严重超时了。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
这次立下大功的,是两款AI系统——AlphaProof和AlphaGeometry 2。
划重点:2024 IMO并不在这两个AI的训练数据中。
其实,早在今年1月份,谷歌DeepMind的第一代AlphaGeometry就登上了Nature。当时,它做出了IMO 30个几何题中的25道。
AI工程师devin背后创始人之一Scott Wu(IOI三枚金牌得主)感慨道,「当我还是个孩子的时候,奥林匹克竞赛就是我的全部。从来没有想过,仅仅10年后,它们就被AI解决了」。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
今年的IMO竞赛上,共有六道赛题,涉及代数、组合学、几何和数论。六道做出四道,让我们感受一下AI的水平——
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
AI的数学推理能力,震惊评分教授
我们都知道,以前的AI在解决数学问题上一直捉襟见肘,原因在于推理能力和训练数据的限制。
而今天携手登场的两位AI选手,则打破了这种限制。它们分别是——
– AlphaProof,基于强化学习的形式数学推理新系统
– AlphaGeometry 2,第二代几何解题系统
两位AI给出的答案,由著名数学家Timothy Gowers教授(IMO金牌得主和菲尔兹奖得主)和Joseph Myers博士(两次IMO金牌得主、IMO 2024问题选择委员会主席),根据规则进行评分。
最终,AlphaProof正确做出两个代数题和一个数论题,其中一个最难的问题,在今年IMO中只有5名人类参赛者做了出来;AlphaGeometry 2则做出了一道几何题。
没有被攻克的,只有两道组合数学题。
Timothy Gowers教授在评分的过程中,也被深深地震撼了——
程序能够提出这样一个非显而易见的解法,实在令人印象深刻,远超出我对当前技术水平的预期。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
AlphaProof
AlphaProof是一个能够在形式化语言Lean中证明数学命题的系统。
它结合了预训练的大语言模型和AlphaZero强化学习算法,后者曾自学掌握了国际象棋、将棋和围棋。
形式化语言的一个关键优势,就是可以对涉及数学推理的证明进行形式化验证。然而,由于人类编写的相关数据量非常有限,它们在机器学习中的应用一直受到限制。
相比之下,基于自然语言的方法尽管可以访问大量数据,但却可能产生似是而非、但不正确的中间推理步骤和解决方案。
为了克服这一点,谷歌DeepMind研究者通过微调Gemini模型,将自然语言问题陈述自动翻译成形式化陈述,建立了一个包含不同难度的形式化问题的大型库,从而在两个互补领域之间架起桥梁。
解题时,AlphaProof会生成候选的解决方案,并通过在Lean中搜索可能的证明步骤,来证明或反驳它们。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
每个被找到并验证的证明,都被用于强化AlphaProof的语言模型,让它可以在后续解决更难的问题。
为了训练AlphaProof,研究者证明或反驳了几百万个问题,涵盖了从比赛前几周到比赛期间广泛的难度和数学主题领域。
在比赛期间,他们还应用了训练循环,通过强化自生成的比赛问题变体的证明,直到找到完整的解决方案。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
AlphaProof强化学习训练循环的流程信息图:大约一百万个非正式数学问题由形式化网络翻译成形式化数学语言;接着,求解网络通过索这些问题的证明或反驳,并利用AlphaZero算法逐步训练自己,以解决更具挑战性的问题
AlphaGeometry 2
AlphaGeometry的升级版AlphaGeometry 2,是一个神经符号混合系统,基于Gemini的语言模型从头开始训练。
基于比上一代多了一个数量级的合成数据,它能够做出难度更高的几何问题,包括涉及物体运动、角度、比例和距离方程等等。
此外,它还采用了比前一代快两个数量级的符号引擎。当遇到新问题时,它会用一种新颖的知识共享机制,使不同索树的高级组合能够解决更复杂的问题。
在今年参赛IMO之前,AlphaGeometry 2已经战绩累累:它能做出过去25年IMO几何赛题中的83%,而第一代只能做出53%。
在这届IMO中,AlphaGeometry 2的神勇速度更是震惊了众人——在接收到形式化问题的19秒内,它就把问题4做出来了!
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
问题4要求证明∠KIL和∠XPY之和等于180°。AlphaGeometry 2建议在BI线上构造一个点E,使得∠AEB=90°。点E有助于确定AB的中点L,形成了许多类似的三角形对,如ABE ~ YBI和ALE ~ IPC,从而证明结论
AI的解题过程

值得一提的是,这些问题首先会被人工翻译成正式的数学语言,然后才会投给AI。

P1

一般来说,每届IMO试题中第一题(P1)相对来说,是比较容易的。
网友表示,「P1仅需要高中数学知识就够了,人类选手通常会在60分钟内完成」。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
IMO 2024第一题主要考察了实数α的性质,并要求找出满足特定条件的实数α。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
AI给出了正确答案——α是偶整数。那么,它具体是如何解答的呢?
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
解题第一步,AI先给出了一个定理,左右两边集合相等。
左边集合表示,所有满足条件的实数α,对于任何正整数n,n能整除从1到n的⌊i*α⌋;右边集合表示,存在一个整数k,k是偶数,实数α等于k。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
接下来的证明中,分为两个方向。
首先证明右边集合,是左边集合的子集(简单方向)。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
然后,再证明左边集合,是右边集合的子集(困难方向)。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
直到代码结束时,AI提出了一个关键等式⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋),使用等式来证明α必须是偶数。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
最后,DeepMind总结了AI在解题过程中,依赖的三个公理:propext、Classical.choice,以及Quot.sound。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
以下是P1的完整解题过程:https://storage.Googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手

上下滑动查看

P2

第二题考察的是,正整数对(a,b)的关系,涉及到最大公约数的性质。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
AI求解的答案是:
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
定理是对于满足特定条件的正整数对(a,b),其集合只能包含(1,1)。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
AI在如下的解题过程中,采取的证明策略是,首先证明(1,1)满足给定条件,然后再证明这是唯一的解。
证明(1,1)是最终解,使用g=2,N=3。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
证明如果(a,b)是解,那么ab+1必须整除g。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
在这一过程中,AI使用了欧拉定理,以及模运算的性质进行推理。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
最后,去证明a=b=1是唯一可能的解。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
如下是P2的完整解题过程:https://storage.Googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手

上下滑动查看

P4

P4是一道几何证明题,要求去证明一个特定的几何角度关系。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
如上所述,这是由AlphaGeometry 2在19秒内完成答题,创新纪录。
根据所给的解决方案,与一代AlphaGeometry一样,所有解决方案中的辅助点都是由语言模型自动生成的。
证明中,所有的角度追踪都使用了高斯消元法(Gaussian elimination),d(AB)−d(CD)等于从AB到CD的有向角度(以π为模)。
解题过程中,AI会手动标注相似三角形和全等三角形对(以红色标注)。
接下来,就是AlphaGeometry的解题步骤了,采用了「反证法」去完成。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
先用Lean完成需要证明命题的形式化,以及可视化几何构造。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
证明中的关键步骤,如下所示。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
完整解题过程参见下图:https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手

上下滑动查看

P6

IMO第六题便是「终极boss」,探讨了函数的性质,要求证明关于有理数的特定结论。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
AI求解,c=2。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
先来看定理声明是,定义了「Aquaesulian函数」的性质,并声明对于所有这样的函数,f(r)+f(-r)的取值集合最多有2个元素。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
证明策略是,首先证明对于任何Aquaesulian函数,f(r)+f(-r)的取值集合最多有2个元素。然后构造一个具体的Aquaesulian函数,使得f(r)+f(-r)恰好有2个不同的值。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
证明当f(0)=0时,f(x)+f(-x)最多取两个不同的值,并证明不可能存在f(0)≠0的Aquaesulian函数。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
构造函数f(x)=-x+2⌈x⌉,并证明它是Aquaesulian函数。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
最后,再去证明对于这个函数,f(-1)+f(1) =0和f(1/2)+f(-1/2)=2是两个不同的值。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
以下是完整解题过程:https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手

上下滑动查看
能做奥数题,但能分清9.11和9.9谁大吗?
斯坦福大学和红杉的研究员Andrew Gao肯定了这次AI突破的意义——
关键的是,最新IMO试题不包含训练集中。这一点很重要,说明AI能够处理全新的、未见过的问题。
而且,被AI成功解出的几何问题,由于涉及空间性质(需要直观思维和空间想象力),历来都被认为是极具挑战性的。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
英伟达高级科学家Jim Fan则发长文表示,大模型是神秘的存在——
它们既能在数学奥林匹克竞赛中获得银牌,又会在「9.11和9.9哪个数字更大」这样的问题上频频出错。
不仅是Gemini,就连GPT-4o、Claude-3.5、Llama-3都无法100%正确回答。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
通过训练AI模型,我们正在探索超越自身智能的广阔领域。在这个过程中,我们发现了一个非常奇特的区域——一个看起来像地球,却充满诡异山谷的系外行星
这看起来很不合理,但我们可以用训练数据分布来解释:
AlphaProof和AlphaGeometry 2,是在形式化证明和特定领域的符号引擎上完成训练。在某种程度上,它们在解决专业的奥林匹克竞赛问题更出色,即使它们基于通用LLM构建的。
GPT-4o的训练集中,混杂了大量的GitHub代码数据,可能远远超过数学数据。在软件版本中,「v9.11 > v9.9」,可能严重扭曲了数据分布。因此,这个错误在某种程度上是可以理解的。
谷歌开发者负责人表示,能够解决困难的数学、物理问题的模型,是通向AGI的关键路径,而今天我们在这条道路上又迈出了一步。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手
另有网友表示,这一周信息量太大了。
谷歌AI一分之差痛失IMO金牌!19秒做一题碾压人类选手

这一次的竞赛不仅展示了AI在数学推理领域的巨大潜力,还引发了人们对人工智能在未来挑战和机遇的广泛讨论。