編輯：編輯部
【新智元導讀】 就在剛剛，谷歌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的訓練數據中。
其實，早在今年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。
先來看定理聲明是，定義了「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/
