每經(jīng)編輯 杜宇

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

圖片來源：每經(jīng)記者 鄭雨航 攝

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

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

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

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

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

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

AlphaProof：形式化數(shù)學推理的突破

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

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

工作流程如下：

問題轉(zhuǎn)化：首先，使用經(jīng)過微調(diào)的Gemini模型將自然語言的數(shù)學問題自動轉(zhuǎn)換為Lean的形式化語言。這一步驟創(chuàng)建了一個大型的形式化問題庫，涵蓋不同難度級別。

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

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

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

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

AlphaGeometry 2

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

AlphaGeometry 2是一個神經(jīng)符號混合系統(tǒng)。主要改進包括：

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

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

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

性能提升：在接受今年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)語言模型加符號推導引擎組成，希望兩相結(jié)合以尋求對復雜幾何定理的證明。這類似于“快、慢思考相結(jié)合”的理念，一個系統(tǒng)提供快速、“直觀”的想法，另一系統(tǒng)則做出更加深思熟慮的理性決策。

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

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

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

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

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

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

每日經(jīng)濟新聞綜合公開資料

免責聲明：本文內(nèi)容與數(shù)據(jù)僅供參考，不構(gòu)成投資建議，使用前請核實。據(jù)此操作，風險自擔。

封面圖片來源：每經(jīng)記者 鄭雨航 攝