谷歌DeepMind團(tuán)隊推出了基于強(qiáng)化學(xué)習(xí)的新型形式數(shù)學(xué)推理系統(tǒng)AlphaProof以及幾何求解系統(tǒng)的改進(jìn)版本AlphaGeometry 2。這兩個系統(tǒng)解決了今年國際數(shù)學(xué)奧林匹克競賽（IMO）六道題目中的四道，首次在競賽中取得與銀牌得主同等的成績。

近年來，一年一度的國際數(shù)學(xué)奧林匹克競賽也被廣泛認(rèn)為是機(jī)器學(xué)習(xí)領(lǐng)域的一大挑戰(zhàn)，也是衡量人工智能系統(tǒng)高級數(shù)學(xué)推理能力的理想基準(zhǔn)。

今年，谷歌人工智能系統(tǒng)成功挑戰(zhàn)了IMO主辦方提供的競賽賽題。谷歌解決方案由著名數(shù)學(xué)家、IMO金牌得主和菲爾茲獎得主蒂莫西·高爾斯教授和兩屆IMO金牌得主、IMO 2024問題遴選委員會主席約瑟夫·邁爾斯博士根據(jù)IMO評分規(guī)則進(jìn)行評分。

首先，賽題被手動翻譯成正式的數(shù)學(xué)語言，以便人工智能系統(tǒng)理解。在正式比賽中，學(xué)生分兩節(jié)提交答案，每節(jié)4.5小時。

AlphaProof通過確定答案并證明其正確性，解決了兩道代數(shù)題和一道數(shù)論題。其中包括比賽中最難的一道題，今年IMO比賽中只有五名選手解決了這道題；AlphaGeometry 2則解決了幾何題目，而兩道組合題目仍未解決。

六道題目每道可得7分，總分最高為42分。谷歌人工智能系統(tǒng)最終得分為28分，每道題目都獲得滿分——相當(dāng)于銀牌類別的最高分。今年，金牌門檻為29分，在正式比賽中，609名參賽者中有58人達(dá)到了金牌門檻。

AlphaProof是一個自我訓(xùn)練的系統(tǒng)，以形式語言Lean來證明數(shù)學(xué)陳述。它將預(yù)先訓(xùn)練好的語言模型與AlphaZero強(qiáng)化學(xué)習(xí)算法結(jié)合，后者之前曾自學(xué)過如何掌握國際象棋、將棋和圍棋游戲。

形式語言的關(guān)鍵優(yōu)勢在于，涉及數(shù)學(xué)推理的證明可以得到形式化驗證，以確保其正確性。相比之下，基于自然語言的方法盡管能夠訪問數(shù)量級更多的數(shù)據(jù)，卻可能產(chǎn)生看似合理但實際上不正確的中間推理步驟和解決方案。谷歌通過微調(diào)Gemini模型來自動將自然語言問題陳述轉(zhuǎn)換為形式陳述，從而在這兩個互補(bǔ)領(lǐng)域之間建立了一座橋梁，創(chuàng)建了一個包含各種難度的形式化問題大型庫。

當(dāng)遇到問題時，AlphaProof會生成解決方案候選，然后通過搜索Lean中可能的證明步驟來證明或反駁這些候選。每個找到并驗證的證明都會用于強(qiáng)化AlphaProof語言模型，從而提高其解決后續(xù)更具挑戰(zhàn)性題目的能力。

AlphaGeometry 2則是AlphaGeometry的顯著改進(jìn)版本。它是一個神經(jīng)符號混合系統(tǒng)，其中的語言模型基于Gemini，并使用比其前身多一個數(shù)量級的合成數(shù)據(jù)從頭開始訓(xùn)練。這有助于該模型解決更具挑戰(zhàn)性的幾何題目，包括有關(guān)物體運(yùn)動和角度、比率或距離方程的問題。

AlphaGeometry 2 采用的符號引擎比其前代產(chǎn)品快兩個數(shù)量級。當(dāng)遇到新問題時，會使用一種新穎的知識共享機(jī)制來實現(xiàn)不同搜索樹的高級組合，以解決更復(fù)雜的問題。