數學界迎來AlphaGo時刻:GoogleAI用19秒答完一道IMO幾何題,差1分即可摘金
近日,GoogleDeepMind 宣佈其人工智能系統在數學解題能力上取得了突破性進展。
在 2024 年國際數學奧林匹克競賽(IMO,International Mathematical Olympiad)的六道題目中,該公司的人工智能系統成功解決了其中的四道,獲得了相當於銀牌的成績。
這標誌著人工智能系統首次在這項全球頂級少年數學家競賽中達到了獎牌級別的表現。
DeepMind 開發了兩個專門的人工智能系統 AlphaProof 和 AlphaGeometry 2,兩者協作拿到了這一成績。
![(來源:DeepMind)](http://n.sinaimg.cn/spider20240726/75/w1072h603/20240726/2a14-bd197af1210e9547ada47a209769d4d1.png)
AlphaProof 解決了兩道代數題和一道數論題,其中包括本次比賽中最難的一道題目。而 AlphaGeometry 2 則成功解決了一道幾何題,僅僅耗時 19 秒。未能完成的兩道題屬於組合數學的範疇。
這兩個人工智能系統的總成績獲得了 42 分中的 28 分,僅差 1 分就達到了金牌的門檻。
![圖丨AI 系統相較於所有人類選手的表現(來源:DeepMind)](http://n.sinaimg.cn/spider20240726/372/w616h556/20240726/61e1-0e621a8054a07652d878c59bf615cc1f.png)
IMO 作為自 1959 年以來每年舉辦的重大數學賽事,一直吸引著全球精英學生參與。
比賽涵蓋代數、組合數學、幾何和數論等領域,題目難度極高。近年來,IMO 問題的解決能力已成為評估人工智能系統數學推理能力的重要基準。
據 DeepMind 介紹,AlphaProof 是一個基於強化學習的系統,它通過生成和驗證數百萬個證明來自我訓練,逐步解決越來越困難的問題。該系統使用形式化語言 Lean 來證明數學陳述。
訓練數據不足是常見的問題之一,為解決該問題,研究團隊設計了一個額外的網絡,試圖將現有的百萬個用自然語言寫成的問題翻譯成 Lean 語言,而不包含人工編寫的答案。
![](http://n.sinaimg.cn/spider20240726/672/w1070h402/20240726/97a9-032a1a4df4ebc0f1ecd05f76895578ef.jpg)
圖丨AlphaProof 強化學習訓練循環:形式化網絡將大約一百萬個非形式化數學問題翻譯成形式化數學語言。然後,求解器網絡搜索問題的證明或反證,通過 AlphaZero 算法逐步訓練自身以解決更具挑戰性的問題(來源:DeepMind)
AlphaGeometry 2 是Google之前幾何解題人工智能模型的升級版本,現在由基於 Gemini 的語言模型驅動。它可以解決與物體運動以及涉及角度、比率和距離的方程式有關的問題。
由於它比其前身接受了更多合成數據的訓練,因此能夠解決更具挑戰性的幾何問題。
在嘗試本次 IMO 之前,AlphaGeometry 2 能夠解決過去 25 年 IMO 幾何問題的 83%,遠高於其前身 53% 的成功率。
在今年的比賽中,該系統在接收到幾何題的形式化版本後僅用 19 秒就找到瞭解決方法。
值得注意的是,人工智能系統解題的過程與人類參賽者有所不同。Google首先將 IMO 問題翻譯成形式化的數學語言,然後交由人工智能模型處理。
而在正式比賽中,人類參賽者需要在兩個 4.5 小時的環節中直接面對數學陳述。
![圖丨AI 系統用 19 秒解決的幾何題:要求證明 ∠KIL 與 ∠XPY 之和等於 180°(來源:DeepMind)](http://n.sinaimg.cn/spider20240726/324/w616h508/20240726/eefe-e8d9f177d37a5adfeaafe3d17ca9c29c.png)
儘管取得了令人矚目的成就,但這項技術仍存在一些局限性。費爾茲獎得主、著名數學家蒂莫西·高爾斯爵士(Timothy Gowers)指出了幾個關鍵的限制因素。
首先,人工智能系統需要比人類參賽者更長的時間來解題,有些問題花費了 60 小時以上,而且人工智能系統的處理速度也比人類大腦快得多。如果給予人類參賽者同樣的時間,他們的分數可能會更高。
其次,數學題需要人工將其翻譯成形式化語言 Lean,然後人工智能模型才能開始工作。
雖然人工智能執行了最重要的數學推理,但這個「自動形式化」步驟仍需由人類完成。
此外,目前尚不清楚這種技術是否能擴展到其他數學領域,特別是那些訓練數據較少的領域。
值得注意的是,人工智能系統未能解決兩道組合數學問題,這表明它在某些數學領域還有待進步。
儘管存在這些限制,但專家們認為這項技術仍有巨大的潛力。高爾斯推測,這樣的人工智能系統可能成為有價值的研究工具,能夠幫助數學家回答廣泛的問題,只要這些問題不太困難。這將極大地推動數學研究的發展。
劍橋大學專門研究數學和人工智能的研究員凱蒂·柯林斯(Katie Collins)指出,能夠解決複雜數學問題的人工智能系統可能為「人類+人工智能」的協作模式開闢新的道路,幫助數學家解決和發明新類型的問題。
這反過來也可能幫助我們更好地理解人類是如何解決數學問題的。
GoogleDeepMind 研究副總裁普什米特·高利表示,這是機器學習和人工智能領域的重大進展,迄今為止,還沒有哪個系統能以這樣的成功率和通用性來解決問題。
此外,作為 IMO 工作的一部分,DeepMind 還試驗了一種基於Google Gemini 和 DeepMind 最新研究的自然語言推理系統,以實現高級問題解決技能。
有了該系統後,不僅不用把問題翻譯為形式語言,而且它還能夠和其他人工智能系統結合使用。DeepMind 還在今年的 IMO 問題上測試了這種方法,結果顯示出巨大的潛力。
「我們的團隊正在繼續探索多種用於推進數學推理的人工智能方法,並計劃很快發佈有關 AlphaProof 的更多技術細節。」DeepMind 在博客中寫道。
可以預見的是,隨著技術的不斷進步,我們將會看到更多令人興奮的人類+人工智能協作,推動數學和人工智能領域的共同發展。
參考資料:
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
https://arstechnica.com/information-technology/2024/07/google-ai-earns-silver-medal-equivalent-at-international-mathematical-olympiad/
https://www.technologyreview.com/2024/07/25/1095315/google-deepminds-ai-systems-can-now-solve-complex-math-problems/
運營/排版:何晨龍