陶哲軒點評GoogleAlphaProof：AI在數學競賽中展現「超凡智慧」

IMO 2024 中六個問題的每一個問題滿分為 7 分，總分最高 42 分。DeepMind 的系統最終得分為 28 分，意味著解決的 4 個問題都獲得了滿分 —— 相當於銀牌類別的最高分。

DeepMind 文章連接：https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

常用 AI 輔助證明的數學家陶哲軒近期正處在出差的忙碌中，對問題求解引擎 AlphaProof 和 AlphaGeometry2 還未完全消化。但他在自己的博客上對 DeepMind 的 AI 系統參加 IMO 競賽這件事表達了自己的看法。

陶哲軒談到，這是一項非常偉大的工作， 再次改變了我們對哪些基準挑戰可以通過 AI 輔助或完全自主的方法實現的期望。 

例如，IMO 級別的幾何問題現在對於專用的 AI 工具來說已基本解決。現在看來，通過強化學習過程可以找到形式化證明的 IMO 問題至少在某種程度上可以被 AI 攻克。雖然目前每個問題需要相當大的計算量，並且在形式化方面需要人類的幫助。

在陶哲軒看來，這種方法還有一些「buff 加成」，它能使形式化數學更容易自動化，這反過來可能會促進包含形式化成分的數學研究方法。如果更公開地共享由此產生的形式證明數據庫，它可能是一個有用的資源。 

這種方法（更多地基於強化學習而非大型語言模型，有點類似 AlphaGo 的精神，且強調整體方法）非常聰明，事後來看很有道理。正如「AI 效應」所言，一旦解釋清楚，它不會給人一種展示人類智能的感覺；但它仍然是我們 AI 輔助問題解決工具集能力的擴展。

「AI 效應」是指當人工智能技術取得進展或解決問題時，人們往往會認為這些成就並不是真正的人工智能或者不具備真正的智能。換句話說，一旦某項技術被理解或普及，它就不再被認為是智能的。這種現象表明，人們對 「智能」 的定義和期望會隨著技術的進步而不斷提高。 

他在最新博客中表示，DeepMind 的這些新工具無法與最近贏得 AIMO 進步獎的 NuminaMath 模型直接比較。NuminaMath 模型完全自動化且資源效率高出數個數量級，並且採用了完全不同的方法（使用大型語言模型生成 Python 代碼，以蠻力解決區域競賽級別的數值答案問題）。這個模型也是完全開源的。這也是非常不錯的工作，展示了嘗試使用 AI 來輔助或自動化數學問題解決過程的不同部分的多維挑戰。

其實 DeepMind 在數學推理方面有著不懈的努力。在今年年初，它的人工智能算法就已經在數學奧林匹克競賽（IMO）上取得了重大成績突破。論文《Solving olympiad geometry without human demonstrations》向世人介紹了 AlphaGeometry，還登上了國際權威期刊《自然》雜誌。專家表示，這是人工智能朝著具有人類推理能力方向邁進的重要一步。

論文鏈接：https://www.nature.com/articles/s41586-023-06747-5

未來 DeepMind 還將帶給我們怎樣的驚喜，我們拭目以待。

參考鏈接：