每經(jīng)編輯：杜宇
高級數(shù)學(xué)推理是現(xiàn)代人工智能的關(guān)鍵能力，谷歌DeepMind再一次展示了它在這一領(lǐng)域的卓越實力。
圖片來源：每經(jīng)記者 鄭雨航 攝
近日，谷歌宣布其混合人工智能系統(tǒng)在2024年的國際數(shù)學(xué)奧林匹克競賽（IMO）中表現(xiàn)優(yōu)異，獲得了相當(dāng)于銀牌的成績，且僅僅差1分就能摘得金牌。這一突破被認為是AI研究領(lǐng)域的又一個里程碑，被許多人稱為“數(shù)學(xué)界的AlphaGo時刻”。
在IMO中，AlphaGeometry 2在接收到形式化的第4題后，僅用19秒就解決了這個問題。
具體來說google展示了第一個以銀牌級別解決國際數(shù)學(xué)奧林匹克問題的人工智能。
它結(jié)合了 AlphaProof（一種新的突破性形式推理模型）和 AlphaGeometry 2（之前系統(tǒng)的改進版本）。
國際數(shù)學(xué)奧林匹克競賽是全球最悠久、規(guī)模最大、最具聲望的青年數(shù)學(xué)家比賽，自1959年起每年舉辦一次。參賽者需要解決六道涉及代數(shù)、組合學(xué)、幾何和數(shù)論的極其困難的問題。許多菲爾茲獎得主曾在青年時期代表國家參加過IMO。近年來，IMO也成為了機器學(xué)習(xí)領(lǐng)域的一個重要挑戰(zhàn)，被視為衡量人工智能系統(tǒng)高級數(shù)學(xué)推理能力的標桿
在今年的比賽中，DeepMind的AI系統(tǒng)獲得了28分（滿分42分），相當(dāng)于銀牌獲得者的水平。這一成績僅差1分就能達到金牌標準，而在今年的609名參賽者中，只有58人獲得了金牌。
AlphaProof：形式化數(shù)學(xué)推理的突破
AlphaProof系統(tǒng)采用強化學(xué)習(xí)方法，將預(yù)訓(xùn)練的語言模型與AlphaZero算法相結(jié)合。這種方法的優(yōu)勢在于可以正式驗證涉及數(shù)學(xué)推理的證明的正確性。為了克服形式化語言訓(xùn)練數(shù)據(jù)不足的問題，研究團隊通過微調(diào)Gemini模型，創(chuàng)建了一個包含各種難度的形式化問題庫
AlphaProof是一個自學(xué)習(xí)系統(tǒng)，專門用于在形式化數(shù)學(xué)語言Lean中證明數(shù)學(xué)陳述。它的核心創(chuàng)新在于結(jié)合了預(yù)訓(xùn)練語言模型和AlphaZero強化學(xué)習(xí)算法
工作流程如下：
問題轉(zhuǎn)化：首先，使用經(jīng)過微調(diào)的Gemini模型將自然語言的數(shù)學(xué)問題自動轉(zhuǎn)換為Lean的形式化語言。這一步驟創(chuàng)建了一個大型的形式化問題庫，涵蓋不同難度級別。
解決方案生成：面對一個新問題時，AlphaProof會生成可能的解決方案
證明搜索：系統(tǒng)在Lean中搜索可能的證明步驟，試圖證明或反駁這些解決方案
強化學(xué)習(xí)：每找到并驗證一個證明，就用它來強化AlphaProof的語言模型，提高系統(tǒng)解決后續(xù)更具挑戰(zhàn)性問題的能力
持續(xù)訓(xùn)練：在準備IMO比賽期間，AlphaProof在數(shù)周內(nèi)證明或反駁了數(shù)百萬個問題，覆蓋各種難度和數(shù)學(xué)主題。在比賽過程中，它還繼續(xù)應(yīng)用這個訓(xùn)練循環(huán)，通過證明自己生成的比賽問題變體來增強能力，直到找到完整解決方案
AlphaGeometry 2
AlphaGeometry 2是AlphaGeometry的改進版本，它的語言模型基于Gemini，并在比前代多一個數(shù)量級的合成數(shù)據(jù)上進行了訓(xùn)練。
AlphaGeometry 2是一個神經(jīng)符號混合系統(tǒng)。主要改進包括：
增強的語言模型：基于Gemini，從頭開始訓(xùn)練，使用了比前代多一個數(shù)量級的合成數(shù)據(jù)。這大大提高了模型處理復(fù)雜幾何問題的能力，包括物體運動、角度方程、比例或距離等問題。
更快的符號引擎：新版本的符號處理引擎速度提高了兩個數(shù)量級，大大加快了問題解決速度。
知識共享機制：引入了新的知識共享機制，能夠高級組合不同的搜索樹，以解決更復(fù)雜的問題。
性能提升：在接受今年IMO比賽前，AlphaGeometry 2能夠解決過去25年IMO幾何問題的83%，遠超前代系統(tǒng)53%的解決率
實時表現(xiàn)：在今年的IMO中，AlphaGeometry 2在接收到形式化的第4題后，僅用19秒就解決了這個問題。
DeepMind的研究團隊還在探索基于自然語言推理的系統(tǒng)，這種系統(tǒng)不需要將問題轉(zhuǎn)換為形式化語言，可能與其他AI系統(tǒng)結(jié)合使用。這種方法在今年的IMO問題上也顯示出了巨大的潛力。
采用神經(jīng)符號方法
AlphaGeometry是一套神經(jīng)符號系統(tǒng)，由神經(jīng)語言模型加符號推導(dǎo)引擎組成，希望兩相結(jié)合以尋求對復(fù)雜幾何定理的證明。這類似于“快、慢思考相結(jié)合”的理念，一個系統(tǒng)提供快速、“直觀”的想法，另一系統(tǒng)則做出更加深思熟慮的理性決策。
由于語言模型更擅長發(fā)現(xiàn)數(shù)據(jù)中的一般模式和關(guān)系，所以能夠快速預(yù)測可能有用的潛在構(gòu)造，但卻往往缺乏嚴格推理并解釋其決策的能力。另一方面，符號推導(dǎo)引擎則基于形式邏輯，依靠明確的規(guī)則來得出結(jié)論。后者更理性、可解釋性更強，但往往比較“緩慢”且不夠靈活這一點在單獨處理大型復(fù)雜問題時體現(xiàn)得尤其明顯。
AlphaGeometry的語言模型會引導(dǎo)其符號推導(dǎo)引擎為幾何問題尋求可能的解。
奧數(shù)幾何問題的題干大多基于圖表，需要添加新的幾何構(gòu)造才能解決，例如點、線或圓。AlphaGeometry的語言模型可以從無數(shù)種可能性中預(yù)測添加哪些新構(gòu)造更有助于解題。這些線索能夠填補空白，引導(dǎo)符號引擎對圖表做進一步推論并逐步趨近正確答案。
AlphaGeometry解決的一個簡單問題：給定問題圖及其定理前提（左），AlphaGeometry（中）首先使用符號引擎來推導(dǎo)關(guān)于圖的新表述，直到找出正確解或用盡新表述。
如果找不到可行的解，AlphaGeometry語言模型會添加一種可能有用的構(gòu)造（藍色部分，即輔助線）為符號引擎開辟新的推導(dǎo)路徑。整個循環(huán)不斷重復(fù)，直到找到正確解為止（右）。在此示例中，只需要一種新構(gòu)造（一條輔助線）。
AlphaGeometry提出的每一道奧數(shù)題解法，都經(jīng)過計算機檢查和驗證。DeepMind還將結(jié)果與之前的AI方法以及人類選手在奧賽中的表現(xiàn)做出比較。此外，數(shù)學(xué)教練、前奧數(shù)競賽金牌得主Evan Chen也幫助對AlphaGeometry的解題思路進行評估。
每日經(jīng)濟新聞綜合公開資料
