作者：李寶珠

編輯：三羊

封面圖來源：Google DeepMind

DeepMind 用算力堆出奇跡？被夸上天的 AlphaGeometry 含金量有多高

近日，谷歌 DeepMind 的 Alpha 系列再添新成員——AlphaGeometry，依舊聲勢浩大，「里程碑」、「史詩級」、「逼近人類」等贊美之詞溢出屏幕。那么，這個號稱奧數能力金牌級的 AI 系統到底有多少含金量呢？

AlphaGeometry 由谷歌 DeepMind 團隊和紐約大學的研究人員共同研發，**將神經語言模型 (neural language model) 與符號引擎 (symbolic deduction engine) 相結合，**能夠解決復雜的幾何問題，并且水平接近人類。

在對 30 道國際奧林匹克數學競賽 (IMO) 幾何題的基準測試中，在給定時間內 AlphaGeometry 解決了其中的 25 道題，之前 SOTA 的「吳方法」解決了 10 道，而人類 IMO 金牌得主平均可以解決 25.9 個問題。

誠然，自 AlphaGo 面世以來，伴隨著多次面向不同學科的革新性突破，「DeepMind 出品，必屬精品」的定位逐漸在人們心中扎根。但同時，業內也不乏理性、辯證的聲音——算力替代智力固然可喜，但實際應用價值更加重要。所以，借著 AlphaGeometry 的發布，我們想淺談一下，這到底是算力優勢下的狂歡，還是 AI for Science 的探路。

值得一提的是，**我們采訪到了北京大學智能學院教授林宙辰，針對相關學術問題進行了探討與學習。**林宙辰教授曾先后在南開大學、北京大學、香港理工大學攻讀數學和應用數學專業，而后又回到了北京大學數學學院攻讀博士學位，開始進入人工智能領域。（點擊查看林宙辰教授專訪）

表達與計算量：AI for Math 的兩大挑戰

林宙辰教授表示：“過去，數學定理的「表達」與大規模的計算量是 AI 進行數學定理證明的兩大挑戰。”

“首先，作為十分抽象化、且高度依賴邏輯推理的學科，數學擁抱 AI 的第一步就是要解決「表達」問題，將數學定理表達為計算機可以計算的方式是后續 AI 應用的基礎。”

“AlphaGeometry 所針對的幾何問題，「表達」的難度屬于數學中較低的一種，解析幾何、代數幾何的出現，其實已經實現了通過數值來表示幾何形狀和幾何對象間的關系，加之吳文俊院士在 20 世紀 70 年代所提出的「數學機械化」，也在一定程度上為平面幾何定理與機器語言之間構建了連接橋梁。”

“其次，吳文俊院士提出的「吳方法」以及傳統的Gr?bner基等方法，已經從理論上解決了平面幾何定理證明的問題，但是卻囿于算力，換言之，由于存儲量、計算量大，尤其是在面對比較難的平面幾何問題時，操作空間會呈指數級增長，所以過往的很多方法都難以處理高難度問題。”

“計算量大的問題對于「財大氣粗」的 DeepMind 而言顯然不是主要障礙，主要困難在于如何避免操作空間指數級增長，此時機器學習方法可以幫上忙。”

具體而言，AlphaGeometry 基于 1 億個合成數據進行訓練，無需人類演示即可自主應對復雜的幾何學挑戰，并生成人類可閱讀的證明。

如下圖所示，以我國中小學生最熟悉的「等腰定理」為例，想要證明 ∠ABC=∠BCA，需要先手動將問題轉化為計算機語言，進而將其輸入到 AlphaGeometry。

AlphaGeometry 通過運行符號推演引擎啟動證明搜索，該引擎從定理前提中「窮盡」地推演出新的陳述，直到定理得到證明或新的陳述被用盡。如果符號推演引擎未能找到證明，語言模型就會構建一個輔助點，增加可證明的條件，進而重新開始通過符號引擎搜索證明。如此循環，直到找到解決方案。

解決方案將會被自動解析為人類可閱讀的語言，所以還能夠進行驗證、評估。

值得一提的是，AlphaGeometry 使用了合成數據進行模型訓練，解決了相關數據庫匱乏的問題。

研究人員通過在各種隨機定理前提上使用現有的符號引擎，利用 10 萬個 CPU 運行了 72 小時后，獲得了大約 5 億個合成的定理證明示例，進行形式規范化及去重后，最終得到了 1 億個定理證明示例，其中有 900 萬個示例涉及至少一個輔助構造，許多證明步驟超過 200 步，是國際奧林匹克數學競賽幾何題平均證明長度的 4 倍。

合成數據生成過程

為了對比測試 AlphaGeometry 解決實際問題的能力，研究人員嘗試將自 2000 年以來的 IMO 競賽中的幾何問題轉化為符號引擎可讀的機器語言，并發現其中只有 75% 可以成功表達，進而形成了一個由 30 道經典幾何問題組成的測試集 IMO-AG-30。

每個問題都有不同的運行時間，這是因為其推導閉包大小各不相同。研究人員發現，運行時間與問題的難度并不相關。例如，IMO 2019 P6 比 IMO 2008 P1a 難得多，但要在 IMO 時限內求解，所需的并行化時間卻要少得多。

由于語言模型解碼過程會返回 k 個不同的序列，描述 k 個可供選擇的輔助結構，研究人員在 k 個選項上進行集束搜索 (beam search)，使用每個集束的得分作為其值函數。這種方法具有很強的并行性，在有并行計算資源的情況下，可以大幅提高搜索速度。

研究人員發現，在 GPU V100 加速語言模型有四個并行副本的情況下，解決所有 25 個問題并保持在規定時間內的最少并行 CPU 數量如下圖所示：

10 個不同的模型/方法，在 IMO-AG-30 測試集中的表現如下圖所示。有意思的是，GPT-4 在測試中竟一道題都沒有做對。

算力替代智力的背后，應用價值才是重點

最近兩天，網絡上鋪天蓋地的各類報道已經將 AlphaGeometry 的成果剖白得淋漓盡致，其影響力無需贅述，所以我們更希望能夠探究，喧鬧過后，AlphaGeometry 能為科研、為 AI 應用發展帶來哪些實際價值？

對此，林宙辰教授表示：“**目前來看，AlphaGeometry 能夠像 AlphaGo 一樣成為「老師」，在教學方面起到更大的輔助作用。**此外，AlphaGeometry 在模型性能方面的突破不可否認，其更是進一步展示了「大力出奇跡」——強大的算力優勢造就了強悍的模型性能，這也在某種程度上進一步為「崇尚」算力的研究人員、企業增添了信心。”

不過，正如林宙辰教授所言，在 AI 領域，盡管我們已經無數次見證了「算力替代智力」的有效性，但最終邁向行業專家的最后1% 的突破還是很難靠 AI 來實現的。

所以，就目前而言，無論是 AlphaGeometry，亦或 GPT 模型等其他 AI 工具，在人們的日常生活以及科研工作中，仍是「亦師亦友」的存在，靈活使用 AI 工具已是大勢所趨，如何將算力造就的「奇跡」應用于實際問題才是人類難以被取代的價值所在。

借古鑒今，AI 工具的快速崛起與計算機的普及有著很多相似之處，例如革命性的工作方式轉變，正勢如破竹地替代傳統方法，逐漸成為職場能力的考核標準……但對比之下，AI 工具的局限性也更加凸顯，那就是特異性。

林宙辰教授認為：“目前的 AI 工具缺乏統一性，即使只針對數學學科，面向數論和面向幾何學所開發的 AI 工具就已經存在很大差別，更不用提跨學科的AI工具了。AI 工具還沒有像當今的計算機一樣，成為基礎底座，可以方便取用。目前的計算機語言有 C 語言、Java、Python等，完全可以基于其中一種語言解決數學、物理、化學等多學科的問題，這體現了其通用性，但是 AI 工具則不然，光看 Alpha 系列便可知一二。”

所以，林宙辰教授認為：“未來，當 AI 工具可以抽象出來可以重用時，AI for Science 才能夠「大行其道」。”

這也是 HyperAI超神經在持續追蹤 AI for Science 發展進程時所觀察到的現象，部分課題組或研究團隊會在本學科成員之外，專門招聘一位主攻 AI 的成員，負責開發研究中需要的 AI工具，而Science 部分則還是交由傳統的科研人員來完成。

毫無疑問，AI 對科研進程的幫助與提升已經日益明顯，正在成為新趨勢，但這種 AI+Science 的團隊模式又是否是長久之計呢？

林宙辰教授認為：“未來，一方面需要將 AI 工具的使用門檻降低，達到一定的統一性，使得 Science 人員也能夠針對不同的問題自行組合使用 AI 工具的組件，就像計算機編程一樣；另一方面，Science 人員也需要逐步提升使用 AI工具的能力，才能充分發揮AI的威力。”

道阻且長，行之將至。AI for Science 由DeepMind 等大廠引發，加之國家政策推進，已經開始了漫漫征程，其中的荊棘需要科研與產業界共同肅清，才能夠真正在落地中為人類發展創造價值。

最后，感謝北京大學智能學院林宙辰教授對筆者撰文提供的幫助與支持。目前林宙辰教授的課題組正在招聘博士研究生，歡迎符合要求的學生將簡歷發送至：zlin@pku.edu.cn

我信奉的信條是物理學家路德維希·波茲曼的名言：沒有什么比一個好的理論更實用的了。我現在想招數學能力強（但這并不意味著你必須來自數學系）、對理論分析非常感興趣的博士研究生，以便與我一起享受如何優雅地使用數學解決實際問題。歡迎發送簡歷給我。

——林宙辰

來源: HyperAI超神經