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

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

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

1.AlphaProof

形式語言的優勢在于能夠驗證數學證明的正確性，但由于數據稀缺，在機器學習的過程成為瓶頸。自然語言方法可以擁有更多的數據，但會產生不正確的推理步驟。AlphaProof通過微調語言模型將自然語言問題陳述轉化為正式陳述來彌合這一差距，從而創建一個具有不同難度級別的大型正式問題庫。

AlphaProof使用Gemini模型的微調版本，將自然語言的數學問題轉換為一種稱為 Lean 的正式斷言，同時將預訓練的語言模型與AlphaZero強化學習算法相結合。

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

該系統針對涵蓋各種困難和數學主題的數百萬個問題進行了訓練，這些問題涉及到廣泛的數據領域，且都是相當困難的問題。哪怕它在參加國際數學奧林匹克競賽 （IMO） 競賽期間也進行了循環訓練。

“事實上，程序可以提出像這樣不明顯的結構，這非常令人印象深刻，遠遠超出了我的認知。” — Timothy Gowers 爵士教授，IMO 金牌得主和菲爾茲獎獲得者。

在今年的比賽之前，AlphaGeometry 2可以解決過去25年中所有歷史IMO幾何問題的83%，而第一代只能解決53%。

對于IMO 2024，AlphaGeometry 2在收到其形式化后的19秒內解決了問題4。

問題4要求證明∠KIL和∠XPY之和等于 180°。AlphaGeometry 2建議構造 E，即直線BI上的一個點，使∠AEB = 90°。點E有助于確定AB的中點L，從而創建許多相似三角形對，例如證明結論所需的 ABE ~ YBI和ALE ~ IPC。

2.正式的推理方法

AlphaProof訓練自己用形式語言Lean來證明數學斷言。它將預訓練的語言模型與AlphaZero強化學習算法相結合，該算法以前自學如何掌握國際象棋、將棋和圍棋的游戲。

上圖為AlphaProof的強化學習訓練循環的過程信息圖。大約有100萬個非正式數學問題被形式化網絡翻譯成正式的數學語言。然后，求解器網絡搜索問題的證明或反駁，通過AlphaZero算法逐步訓練自身以解決更具挑戰性的問題。

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

未來神經符號方法可以為人工智能系統提供一種方法，將問題或任務轉化為一種形式，可以以一種產生可靠結果的方式進行推理。例如OpenAI正在研發代號為“草莓”的系統。

研究人員指出谷歌DeepMind不會讓人類數學家失業。“我們的目標是提供一個可以證明任何事情的系統，但這并不是數學家工作的終點，”，“數學的很大一部分是提出問題，并找到要問的有趣問題。你可能會把它看作是另一種工具，類似于滑尺、計算器或計算工具。”

本文轉載自 ??魯班模錘??，作者： 龐德公