DeepMind表示,儘管基於自然語言的方法可以訪問更多資料,但會產生看似合理但不正確的中間推理步驟和解決方案。而形式語言提供了一個重要優勢,即涉及數學推理的證明可以被形式化地驗證其正確性。
DeepMind人工智慧系統在IMO 2024上相對於人類競爭者的表現。在42分的總分中,人工智慧系統獲得了28分。
GoogleDeepMind的AI模型解決了今年國際數學奧林匹克競賽(IMO)六個問題中的四個問題,人工智慧首次達到了銀牌標準。
當地時間7月25日,GoogleDeepMind公佈專用於數學推理的模型AlphaProof,以及專注於幾何的模型更新版本AlphaGeometry 2。DeepMind表示,AlphaProof和AlphaGeometry 2解決了數學中的高級推理問題,具有先進數學推理能力的通用人工智慧或開啟科學和技術的新領域。
IMO是歷史最悠久、規模最大、最負盛名的青年數學家競賽,自1959年以來每年舉辦一次。選手要解決代數、組合學、幾何和數論方面六個異常困難的問題。菲爾茲獎是數學家的最高榮譽之一,菲爾茲獎獲得者也會代表他們的國家參加IMO。
近年來,IMO競賽被認為是機器學習領域的重大挑戰,也是衡量人工智慧系統高級數學推理能力的理想基準。
GoogleDeepMind表示,IMO的數學問題被人工翻譯成數學語言,供系統理解。在正式比賽中,學生們分兩次提交答案,每次4.5小時。而人工智慧系統在幾分鐘內解決了一個問題,花了三天時間來解決其他問題。基於強化學習的推理系統AlphaProof解決了兩個代數問題和一個數論問題並被證明答案正確,這些問題包括今年IMO比賽中只有5名選手解決的最難的問題。AlphaGeometry 2證明了幾何問題,但兩個組合問題仍未解決。
六道題每題可得7分,總分最高可達42分。DeepMind的人工智慧系統最終得分28分。DeepMind表示,今年金牌的門檻從29分開始,在正式比賽的609名選手中,有58名達到了這個門檻。
“事實上,這個程序能想出這樣一個不明顯的結構是非常令人印象深刻的,遠遠超出了我認為的最先進的水平。”IMO金牌得主和菲爾茲獎牌得主蒂莫西·高爾斯(Timothy Gowers)表示。
在大量書面文字上訓練的人工智慧模型歷來在數學推理方面很困難,往往傾向於語言智能而非數學智能,解決數學問題需要更複雜的推理技能。AlphaProof將預先訓練好的語言模型與AlphaZero強化學習演算法結合在一起,AlphaZero此前自學了如何掌握國際象棋、將棋和圍棋。
大語言模型容易產生幻覺,或以令人信服的方式傳遞錯誤資訊。DeepMind表示,儘管基於自然語言的方法可以訪問更多資料,但會產生看似合理但不正確的中間推理步驟和解決方案。而形式語言提供了一個重要優勢,即涉及數學推理的證明可以被形式化地驗證其正確性。“我們通過微調Gemini模型,在這兩個互補的領域之間建立了一座橋樑,自動將自然語言問題語句轉換為形式語句,建立了一個不同難度的龐大形式問題庫。”
當遇到一個數學問題時,AlphaProof會生成候選解決方案,然後搜尋可能的證明步驟來證明或反駁它們。每一個被發現和驗證的證明都被用來強化AlphaProof的語言模型,增強其解決後續更具挑戰性問題的能力。
AlphaGeometry 2解決的幾何問題:證明∠KIL與∠XPY之和等於180°。AlphaGeometry 2提出在直線BI上構造點E,使∠AEB=90°。點E有助於為AB的中點L提供作用,創造了許多對相似三角形,如三角形ABE和三角形YBI、三角形ALE和三角形IPC,以證明結論。
AlphaGeometry 2是AlphaGeometry的一個改進版本。AlphaGeometry 2是一個神經符號混合系統,其中的語言模型基於Gemini模型,並在比前身多一個數量級的合成資料上從零開始訓練。這幫助模型解決更具挑戰性的幾何問題,包括物體運動問題和角度、比例或距離方程。在今年的比賽之前,AlphaGeometry 2可以解決過去25年中IMO歷史幾何問題的83%,而AlphaGeometry只有53%。在今年的比賽中,AlphaGeometry 2收到形式語言後19秒內解決了問題。
但Google研究人員也表示,人工智慧遠不能以其解決問題的能力取代人類數學家。“即使我們有最大的雄心壯志,我認為我們的目標是提供一個可以證明任何事情的系統。”GoogleDeepMind強化學習副總裁大衛·西爾弗(David Silver)表示,“但這並不是數學家工作的終點。”
西爾弗說,DeepMind的人工智慧模型更類似於強大的計算工具,有朝一日可能會幫助人類提出數學證明,但人工智慧系統缺乏的是想像力,而“數學家提出了有趣的問題”。 (澎湃新聞科技頻道)