谷歌DeepMind發布消息稱，它所开發的AI系統AlphaProof和AlphaGeometry2在數學上取得突破，解答了今年國際數學奧林匹克競賽（IMO）6道題中的4道，相當於銀牌水平。

谷歌還自豪宣稱，這是AI第一次取得如此耀眼的成績。可惜就像之前所鼓吹的其它AI一樣，谷歌的說法也有誇大之嫌。

離金牌线只有一步之遙

根據谷歌的解釋，AlphaProof用增強學習技術在开源求證輔助系統Lean環境中證明數學命題。Lean是微軟公司計算機科學家萊昂納多·德莫拉开發的，採用了由所謂“有效的老式人工智能”(GOFAI)——即從邏輯學汲取靈感的符號人工智能——所驅動的自動推理。

谷歌系統具備自我學習能力，它生成並驗證數百萬個數學證明，在解決復雜數學問題時進步明顯。在此之前，谷歌开發過幾何AI模型，AlphaGeometry2相當於升級版本，它是谷歌以Gemini語言模型作爲基礎，用大量數據訓練出來的。

知名數學家SirTimothyGowers和Dr.JosephMyers用國際數學奧林匹克競賽標准對谷歌AI系統進行評估，國際數學奧林匹克競賽的金牌线爲29分，總分42分，谷歌系統拿到28分，離金牌线只有一步之遙。在最難的問題上谷歌系統完美解答，今年只有5人解決此問題。

國際數學奧林匹克競賽始於1959年，面向預科數學天才（也就是還沒進入大學的數學天才），主要涉及代數、組合數學、幾何和數論。

用競賽問題測試AI已經成爲評估AI推理能力的重要標准。AlphaProof解決了兩個代數問題，一個數論問題；AlphaGeometry2解決了一個幾何問題，但谷歌AI被兩個組合數學問題挫敗。在解決問題時，有一個只用了幾分鐘，其它耗時較長，最多三天。

谷歌AI用於數學也有局限

爲什么說谷歌的說法也有誇大之嫌呢？

首先，谷歌將競賽問題轉化爲正式數學語言，方便AI模型處理。這一做法與官方競賽流程不符，人類參賽者會直接面對問題。

AI模型可以生成文章或者其它形式的文本，但面對復雜數學問題時往往會捉襟見肘，因爲當中牽涉到復雜的邏輯推理，這正是目前AI系統所欠缺的。復雜數學問題會涉及到抽象概念、子目標設定、回溯、嘗試新路徑，這些都給AI帶來挑战。

專注於數學和AI研究的劍橋大學研究人員KatieCollins說：“如果你有辦法檢查答案（也就是正式語言），訓練數學AI模型就會容易很多，難點在於網上自然語言（非正式語言）數據超級多，但正式數學語言數據卻很少。”

谷歌DeepMindAI可以自動將用自然非正式語言編寫的數學問題轉化爲正式語言，這是谷歌之所以取得突破的關鍵。愛丁堡大學混合AI講師WendaLi說，對於數學社區而言，自動將非正式語言轉化爲非正式語言是一大進步。

在參加今年的競賽之前，AlphaGeometry2曾嘗試解答之前25年積累的國際數學奧林匹克競賽幾何問題，83%都能解答——之前的AI只能解答53%。面對今年的幾何問題，谷歌系統只用19秒就給出答案。

其次，谷歌AI模型花費的時間有時顯著過長。SirTimothyGowers承認DeepMind模型取得突破，表現遠超之前的自動定理證明者，但AI解答時花費的時間遠長於人類參賽者，有些問題需要的時間甚至超過60個小時，AI的處理速度本來比人類快很多，但還是需要更長時間，如果人類參賽者有同樣長的時間解答，得分肯定更高。

SirTimothyGowers還說，在正式答題之前，人類已經手動將題目轉化爲正式語言Lean，然後AI才着手處理，雖然核心數學推理是由AI完成的，但“自動化”步驟卻由人類操刀。

替代數學家還需時日

到底谷歌系統會給數學研究造成什么影響？SirTimothyGowers只能說“不確定”。他表示：“是不是到了數學家即將成爲多余的地步？很難說。我想我們離這個目標還差一個或者兩個突破。”

他認爲，谷歌系統解答時需要更長時間說明AI並沒有很好解決數學問題，但在操作時應該發生了一些有趣的事情。

雖然存在諸多局限性，SirTimothyGowers仍認爲類似的AI系統將會成爲富有價值的研究工具。在程序的輔助下，對於那些不是特別難的問題（幾個小時就能解決），AI可以幫助數學家尋找答案，如此一來，即使AI本身無法解決开放問題，也能成爲數學家的實用工具。

不管怎樣，开發一套AI系統，讓它解決富有挑战的數學問題，可以爲未來的人機協作掃清障礙，還可以讓人類深入了解自身是如何解決數學問題的。

當然必須意識到，在人類解決復雜數學問題方面，目前還有很多未解之謎，AI也一樣。

---

標題：谷歌AlphaProof攻克國際奧賽數學題 數學家會不會被淘汰？

地址：https://www.utechfun.com/post/403391.html