谷歌稱著名數(shù)學(xué)家蒂莫西·高爾斯爵士（Sir Timothy Gowers）和約瑟夫·邁爾斯（Joseph Myers）博士使用國際海事組織（IMO）的官方規(guī)則對人工智能模型的解決方案進(jìn)行了評分。該公司報(bào)告稱，其組合系統(tǒng)獲得了42分中的28分，略低于29分的金牌門檻。

AlphaProof解決了兩個代數(shù)問題和一個數(shù)論問題，而AlphaGeometry 2解決了幾何問題。這包括在比賽中最難的問題上獲得滿分，谷歌聲稱今年只有五名人類參賽者解決了這個問題。

圖表顯示了AlphaProof+AlphaGeometry 2在IMO 2024上相對于人類競爭對手的性能。AI獲得28分（滿分42分），達(dá)到了與比賽中銀牌得主相同的水平。

1.AlphaProof

形式語言的優(yōu)勢在于能夠驗(yàn)證數(shù)學(xué)證明的正確性，但由于數(shù)據(jù)稀缺，在機(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強(qiáng)化學(xué)習(xí)算法相結(jié)合。

當(dāng)給定一個問題時，它會生成候選解決方案，并通過在正式斷言語言Lean中搜索證明步驟來證明或反駁它們。每個經(jīng)過驗(yàn)證的證明都用于加強(qiáng)AlphaProof的語言模型，從而提高其解決更具挑戰(zhàn)性問題的能力。

該系統(tǒng)針對涵蓋各種困難和數(shù)學(xué)主題的數(shù)百萬個問題進(jìn)行了訓(xùn)練，這些問題涉及到廣泛的數(shù)據(jù)領(lǐng)域，且都是相當(dāng)困難的問題。哪怕它在參加國際數(shù)學(xué)奧林匹克競賽 （IMO） 競賽期間也進(jìn)行了循環(huán)訓(xùn)練。

“事實(shí)上，程序可以提出像這樣不明顯的結(jié)構(gòu)，這非常令人印象深刻，遠(yuǎn)遠(yuǎn)超出了我的認(rèn)知?！?— 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上的一個點(diǎn)，使∠AEB = 90°。點(diǎn)E有助于確定AB的中點(diǎn)L，從而創(chuàng)建許多相似三角形對，例如證明結(jié)論所需的 ABE ~ YBI和ALE ~ IPC。

2.正式的推理方法

AlphaProof訓(xùn)練自己用形式語言Lean來證明數(shù)學(xué)斷言。它將預(yù)訓(xùn)練的語言模型與AlphaZero強(qiáng)化學(xué)習(xí)算法相結(jié)合，該算法以前自學(xué)如何掌握國際象棋、將棋和圍棋的游戲。

上圖為AlphaProof的強(qiáng)化學(xué)習(xí)訓(xùn)練循環(huán)的過程信息圖。大約有100萬個非正式數(shù)學(xué)問題被形式化網(wǎng)絡(luò)翻譯成正式的數(shù)學(xué)語言。然后，求解器網(wǎng)絡(luò)搜索問題的證明或反駁，通過AlphaZero算法逐步訓(xùn)練自身以解決更具挑戰(zhàn)性的問題。

這項(xiàng)研究的意義在于通過以更扎實(shí)的方式應(yīng)用邏輯和推理來解決大型語言模型的最壞趨勢的前景。大型語言模型往往難以掌握基本的數(shù)學(xué)知識，也無法從邏輯上推理問題。

未來神經(jīng)符號方法可以為人工智能系統(tǒng)提供一種方法，將問題或任務(wù)轉(zhuǎn)化為一種形式，可以以一種產(chǎn)生可靠結(jié)果的方式進(jìn)行推理。例如OpenAI正在研發(fā)代號為“草莓”的系統(tǒng)。

研究人員指出谷歌DeepMind不會讓人類數(shù)學(xué)家失業(yè)?！拔覀兊哪繕?biāo)是提供一個可以證明任何事情的系統(tǒng)，但這并不是數(shù)學(xué)家工作的終點(diǎn)，”，“數(shù)學(xué)的很大一部分是提出問題，并找到要問的有趣問題。你可能會把它看作是另一種工具，類似于滑尺、計(jì)算器或計(jì)算工具?！?/p>

本文轉(zhuǎn)載自 ??魯班模錘??，作者： 龐德公