數(shù)學(xué)界的AlphaGo時刻：谷歌DeepMind AI 19秒解 IMO幾何題，僅差1分即可摘金牌

激石Pepperstone(http://wargoo.com/)報道：

高級數(shù)學(xué)推理是現(xiàn)代人工智能的關(guān)鍵能力。今天，Google宣布了一項長期重大挑戰(zhàn)中的一個重要里程碑：Google混合人工智能系統(tǒng)在今年的國際數(shù)學(xué)奧林匹克競賽（IMO）中獲得了相當(dāng)于銀牌的成績

具體來說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é)推理能力的標(biāo)桿

在今年的比賽中，DeepMind的AI系統(tǒng)獲得了28分（滿分42分），相當(dāng)于銀牌獲得者的水平。這一成績僅差1分就能達到金牌標(biāo)準(zhǔn)，而在今年的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í)算法

工作流程如下：

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

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

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

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

5.持續(xù)訓(xùn)練：在準(zhǔ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)。主要改進包括：

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

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

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

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

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

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