AI研究領域又一個里程碑！19秒解奧數幾何題，僅差1分即可摘金牌

每經編輯 杜宇

高級數學推理是現代人工智能的關鍵能力，谷歌DeepMind再一次展示了它在這一領域的卓越實力。

圖片來源：每經記者 鄭雨航 攝

近日，谷歌宣布其混合人工智能系統在2024年的國際數學奧林匹克競賽（IMO）中表現優異，獲得了相當于銀牌的成績，且僅僅差1分就能摘得金牌。這一突破被認為是AI研究領域的又一個里程碑，被許多人稱為“數學界的AlphaGo時刻”。

在IMO中，AlphaGeometry 2在接收到形式化的第4題后，僅用19秒就解決了這個問題。

具體來說google展示了第一個以銀牌級別解決國際數學奧林匹克問題的人工智能。

它結合了 AlphaProof（一種新的突破性形式推理模型）和 AlphaGeometry 2（之前系統的改進版本）。

國際數學奧林匹克競賽是全球最悠久、規模最大、最具聲望的青年數學家比賽，自1959年起每年舉辦一次。參賽者需要解決六道涉及代數、組合學、幾何和數論的極其困難的問題。許多菲爾茲獎得主曾在青年時期代表國家參加過IMO。近年來，IMO也成為了機器學習領域的一個重要挑戰，被視為衡量人工智能系統高級數學推理能力的標桿‍

在今年的比賽中，DeepMind的AI系統獲得了28分（滿分42分），相當于銀牌獲得者的水平。這一成績僅差1分就能達到金牌標準，而在今年的609名參賽者中，只有58人獲得了金牌。

AlphaProof：形式化數學推理的突破

AlphaProof系統采用強化學習方法，將預訓練的語言模型與AlphaZero算法相結合。這種方法的優勢在于可以正式驗證涉及數學推理的證明的正確性。為了克服形式化語言訓練數據不足的問題，研究團隊通過微調Gemini模型，創建了一個包含各種難度的形式化問題庫

AlphaProof是一個自學習系統，專門用于在形式化數學語言Lean中證明數學陳述。它的核心創新在于結合了預訓練語言模型和AlphaZero強化學習算法‍

工作流程如下：

問題轉化：首先，使用經過微調的Gemini模型將自然語言的數學問題自動轉換為Lean的形式化語言。這一步驟創建了一個大型的形式化問題庫，涵蓋不同難度級別。

解決方案生成：面對一個新問題時，AlphaProof會生成可能的解決方案

證明搜索：系統在Lean中搜索可能的證明步驟，試圖證明或反駁這些解決方案

強化學習：每找到并驗證一個證明，就用它來強化AlphaProof的語言模型，提高系統解決后續更具挑戰性問題的能力

持續訓練：在準備IMO比賽期間，AlphaProof在數周內證明或反駁了數百萬個問題，覆蓋各種難度和數學主題。在比賽過程中，它還繼續應用這個訓練循環，通過證明自己生成的比賽問題變體來增強能力，直到找到完整解決方案

AlphaGeometry 2

AlphaGeometry 2是AlphaGeometry的改進版本，它的語言模型基于Gemini，并在比前代多一個數量級的合成數據上進行了訓練‍。

AlphaGeometry 2是一個神經符號混合系統。主要改進包括：

增強的語言模型：基于Gemini，從頭開始訓練，使用了比前代多一個數量級的合成數據。這大大提高了模型處理復雜幾何問題的能力，包括物體運動、角度方程、比例或距離等問題。

更快的符號引擎：新版本的符號處理引擎速度提高了兩個數量級，大大加快了問題解決速度。

知識共享機制：引入了新的知識共享機制，能夠高級組合不同的搜索樹，以解決更復雜的問題。

性能提升：在接受今年IMO比賽前，AlphaGeometry 2能夠解決過去25年IMO幾何問題的83%，遠超前代系統53%的解決率

實時表現：在今年的IMO中，AlphaGeometry 2在接收到形式化的第4題后，僅用19秒就解決了這個問題。

DeepMind的研究團隊還在探索基于自然語言推理的系統，這種系統不需要將問題轉換為形式化語言，可能與其他AI系統結合使用。這種方法在今年的IMO問題上也顯示出了巨大的潛力。

采用神經符號方法

AlphaGeometry是一套神經符號系統，由神經語言模型加符號推導引擎組成，希望兩相結合以尋求對復雜幾何定理的證明。這類似于“快、慢思考相結合”的理念，一個系統提供快速、“直觀”的想法，另一系統則做出更加深思熟慮的理性決策。

由于語言模型更擅長發現數據中的一般模式和關系，所以能夠快速預測可能有用的潛在構造，但卻往往缺乏嚴格推理并解釋其決策的能力。另一方面，符號推導引擎則基于形式邏輯，依靠明確的規則來得出結論。后者更理性、可解釋性更強，但往往比較“緩慢”且不夠靈活——這一點在單獨處理大型復雜問題時體現得尤其明顯。

AlphaGeometry的語言模型會引導其符號推導引擎為幾何問題尋求可能的解。

奧數幾何問題的題干大多基于圖表，需要添加新的幾何構造才能解決，例如點、線或圓。AlphaGeometry的語言模型可以從無數種可能性中預測添加哪些新構造更有助于解題。這些線索能夠填補空白，引導符號引擎對圖表做進一步推論并逐步趨近正確答案。

AlphaGeometry解決的一個簡單問題：給定問題圖及其定理前提（左），AlphaGeometry（中）首先使用符號引擎來推導關于圖的新表述，直到找出正確解或用盡新表述。

如果找不到可行的解，AlphaGeometry語言模型會添加一種可能有用的構造（藍色部分，即輔助線）為符號引擎開辟新的推導路徑。整個循環不斷重復，直到找到正確解為止（右）。在此示例中，只需要一種新構造（一條輔助線）。

AlphaGeometry提出的每一道奧數題解法，都經過計算機檢查和驗證。DeepMind還將結果與之前的AI方法以及人類選手在奧賽中的表現做出比較。此外，數學教練、前奧數競賽金牌得主Evan Chen也幫助對AlphaGeometry的解題思路進行評估。

每日經濟新聞綜合公開資料

免責聲明：本文內容與數據僅供參考，不構成投資建議，使用前請核實。據此操作，風險自擔。

封面圖片來源：每經記者 鄭雨航 攝