GoogleAI一分之差痛失IMO金牌，19秒做一題碾壓人類選手，幾何AI超進化震撼評委

AI，已經斬獲了IMO奧數銀牌！

就在剛剛，GoogleDeepMind宣佈：今年國際數學奧林匹克競賽的真題，被自家的AI系統做出來了。

其中，AI不僅成功完成了6道題中的4道，而且每道題都獲得了滿分，相當於是銀牌的最高分——28分。

這個成績，距離金牌只有1分之遙！

在正式比賽中，人類選手會分兩次提交答案，每次限時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強化學習算法，後者曾自學掌握了國際象棋、將棋和圍棋。

形式化語言的一個關鍵優勢，就是可以對涉及數學推理的證明進行形式化驗證。然而，由於人類編寫的相關數據量非常有限，它們在機器學習中的應用一直受到限制。

相比之下，基於自然語言的方法儘管可以訪問大量數據，但卻可能產生似是而非、但不正確的中間推理步驟和解決方案。

為了克服這一點，GoogleDeepMind研究者通過微調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」，可能嚴重扭曲了數據分佈。因此，這個錯誤在某種程度上是可以理解的。

Google開發者負責人表示，能夠解決困難的數學、物理問題的模型，是通向AGI的關鍵路徑，而今天我們在這條道路上又邁出了一步。

另有網民表示，這一週信息量太大了。

參考資料：

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

https://x.com/DrJimFan/status/1816521330298356181

本文來自微信公眾號「新智元」，作者：新智元，36氪經授權發佈。