AlphaGeometry：DeepMind 大算力再造奇跡，但「算力代替智力」或許并非最優(yōu)解

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

“AlphaGeometry 所針對的幾何問題，「表達」的難度屬于數(shù)學中較低的一種，解析幾何、代數(shù)幾何的出現(xiàn)，其實已經(jīng)實現(xiàn)了通過數(shù)值來表示幾何形狀和幾何對象間的關(guān)系，加之吳文俊院士在 20 世紀 70 年代所提出的「數(shù)學機械化」，也在一定程度上為平面幾何定理與機器語言之間構(gòu)建了連接橋梁?！?/p>

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

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

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

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

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

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

值得一提的是，AlphaGeometry 使用了合成數(shù)據(jù)進行模型訓練，解決了相關(guān)數(shù)據(jù)庫匱乏的問題。

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

合成數(shù)據(jù)生成過程

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

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

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

研究人員發(fā)現(xiàn)，在 GPU V100 加速語言模型有四個并行副本的情況下，解決所有 25 個問題并保持在規(guī)定時間內(nèi)的最少并行 CPU 數(shù)量如下圖所示：

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

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

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

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

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

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

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

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

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

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

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

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

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

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

我信奉的信條是物理學家路德維?！げㄆ澛拿裕簺]有什么比一個好的理論更實用的了。我現(xiàn)在想招數(shù)學能力強（但這并不意味著你必須來自數(shù)學系）、對理論分析非常感興趣的博士研究生，以便與我一起享受如何優(yōu)雅地使用數(shù)學解決實際問題。歡迎發(fā)送簡歷給我。

——林宙辰