“年輕的”IMO選手：掃蕩“圍棋”后，開始掃蕩“數(shù)學(xué)” 原創(chuàng)
谷歌稱著名數(shù)學(xué)家蒂莫西·高爾斯爵士（Sir Timothy Gowers）和約瑟夫·邁爾斯（Joseph Myers）博士使用國際海事組織（IMO）的官方規(guī)則對人工智能模型的解決方案進行了評分。該公司報告稱，其組合系統(tǒng)獲得了42分中的28分，略低于29分的金牌門檻。
AlphaProof解決了兩個代數(shù)問題和一個數(shù)論問題，而AlphaGeometry 2解決了幾何問題。這包括在比賽中最難的問題上獲得滿分，谷歌聲稱今年只有五名人類參賽者解決了這個問題。
圖表顯示了AlphaProof+AlphaGeometry 2在IMO 2024上相對于人類競爭對手的性能。AI獲得28分（滿分42分），達到了與比賽中銀牌得主相同的水平。
1.AlphaProof
形式語言的優(yōu)勢在于能夠驗證數(shù)學(xué)證明的正確性，但由于數(shù)據(jù)稀缺，在機器學(xué)習(xí)的過程成為瓶頸。自然語言方法可以擁有更多的數(shù)據(jù)，但會產(chǎn)生不正確的推理步驟。AlphaProof通過微調(diào)語言模型將自然語言問題陳述轉(zhuǎn)化為正式陳述來彌合這一差距，從而創(chuàng)建一個具有不同難度級別的大型正式問題庫。
AlphaProof使用Gemini模型的微調(diào)版本，將自然語言的數(shù)學(xué)問題轉(zhuǎn)換為一種稱為 Lean 的正式斷言，同時將預(yù)訓(xùn)練的語言模型與AlphaZero強化學(xué)習(xí)算法相結(jié)合。
當給定一個問題時，它會生成候選解決方案，并通過在正式斷言語言Lean中搜索證明步驟來證明或反駁它們。每個經(jīng)過驗證的證明都用于加強AlphaProof的語言模型，從而提高其解決更具挑戰(zhàn)性問題的能力。
該系統(tǒng)針對涵蓋各種困難和數(shù)學(xué)主題的數(shù)百萬個問題進行了訓(xùn)練，這些問題涉及到廣泛的數(shù)據(jù)領(lǐng)域，且都是相當困難的問題。哪怕它在參加國際數(shù)學(xué)奧林匹克競賽 （IMO） 競賽期間也進行了循環(huán)訓(xùn)練。
“事實上，程序可以提出像這樣不明顯的結(jié)構(gòu)，這非常令人印象深刻，遠遠超出了我的認知。” — Timothy Gowers 爵士教授，IMO 金牌得主和菲爾茲獎獲得者。
在今年的比賽之前，AlphaGeometry 2可以解決過去25年中所有歷史IMO幾何問題的83%，而第一代只能解決53%。
對于IMO 2024，AlphaGeometry 2在收到其形式化后的19秒內(nèi)解決了問題4。
問題4要求證明∠KIL和∠XPY之和等于 180°。AlphaGeometry 2建議構(gòu)造 E，即直線BI上的一個點，使∠AEB = 90°。點E有助于確定AB的中點L，從而創(chuàng)建許多相似三角形對，例如證明結(jié)論所需的 ABE ~ YBI和ALE ~ IPC。
2.正式的推理方法
AlphaProof訓(xùn)練自己用形式語言Lean來證明數(shù)學(xué)斷言。它將預(yù)訓(xùn)練的語言模型與AlphaZero強化學(xué)習(xí)算法相結(jié)合，該算法以前自學(xué)如何掌握國際象棋、將棋和圍棋的游戲。
上圖為AlphaProof的強化學(xué)習(xí)訓(xùn)練循環(huán)的過程信息圖。大約有100萬個非正式數(shù)學(xué)問題被形式化網(wǎng)絡(luò)翻譯成正式的數(shù)學(xué)語言。然后，求解器網(wǎng)絡(luò)搜索問題的證明或反駁，通過AlphaZero算法逐步訓(xùn)練自身以解決更具挑戰(zhàn)性的問題。
這項研究的意義在于通過以更扎實的方式應(yīng)用邏輯和推理來解決大型語言模型的最壞趨勢的前景。大型語言模型往往難以掌握基本的數(shù)學(xué)知識，也無法從邏輯上推理問題。
未來神經(jīng)符號方法可以為人工智能系統(tǒng)提供一種方法，將問題或任務(wù)轉(zhuǎn)化為一種形式，可以以一種產(chǎn)生可靠結(jié)果的方式進行推理。例如OpenAI正在研發(fā)代號為“草莓”的系統(tǒng)。
研究人員指出谷歌DeepMind不會讓人類數(shù)學(xué)家失業(yè)。“我們的目標是提供一個可以證明任何事情的系統(tǒng)，但這并不是數(shù)學(xué)家工作的終點，”，“數(shù)學(xué)的很大一部分是提出問題，并找到要問的有趣問題。你可能會把它看作是另一種工具，類似于滑尺、計算器或計算工具。”
本文轉(zhuǎn)載自 ??魯班模錘??，作者： 龐德公
