谷歌DeepMind最新數(shù)學AI，一舉解決了2000-2024年IMO競賽中84%的幾何問題。

AlphaGeometry2論文發(fā)布，在總共50道題中完成了42道，相比去年的一代多完成了15道。

作為對比，純語言模型OpenAI o1和Gemini Flash Thinking一道都解決不了。

Nature發(fā)文評價：DeepMind AI粉碎了數(shù)學難題，達到金牌得主水平，與頂級人類選手相當。

就比如說2024年競賽中的第四題，AlphaGeometry2完成它只需要19秒。

如圖所示，這道題要求證明∠KIL和∠XPY的合等于180°（藍色表示）。

AlphaGeometry2構(gòu)造的輔助線用紅色表示，E是BI延長線上的點，使得∠AEB=90°，通過E點進一步得到了幾對相似三角形，最終完成證明。

通訊作者Thang Luong分享了更瘋狂的一道題，來自IMO Shortlist 2009。

根據(jù)谷歌咨詢的IMO教練，此問題以前僅有數(shù)值解。

但AlphaGeometry2巧妙地構(gòu)造出了復(fù)雜的輔助結(jié)構(gòu)（紅色表示），給出優(yōu)雅的證明，這些輔助點的位置都是神經(jīng)網(wǎng)絡(luò)預(yù)測的。

AlphaGeometry2四大升級

根據(jù)論文介紹，AlphaGeometry2取得大幅提升主要來自于4項升級：

- 擴展版的領(lǐng)域?qū)Ｓ谜Z言
- 升級版的符號推理引擎DDAR2
- 全新的搜索算法SKEST
- 更強大的語言模型

擴展幾何領(lǐng)域?qū)Ｓ谜Z言

AlphaGeometry1中的領(lǐng)域?qū)Ｓ谜Z言只包含9個基本“謂詞”，包括相等、垂直、平行、共線、共圓等。

這足以覆蓋2000-2024年所有IMO幾何問題中66%的情況，但無法表示線性方程、點/線/圓的移動，以及“計算某個角度”等常見問題。

在進行補充之后，覆蓋率從66%提高到88%。

借助領(lǐng)域?qū)Ｓ谜Z言，AlphaGeometry系統(tǒng)可以做到自動形式化和自動生成示意圖。

這樣一來，只剩下12%涉及3D幾何、不等式、非線性方程和可數(shù)的多個點問題。

對于這些問題，AI只能跳過，在圖中標記為“Not attempted”。

更強大、更快的符號推理引擎DDAR2

符號引擎推理是AlphaGeometry的核心組件，稱為DDAR（Deductive Database
Arithmetic Reasoning，演繹數(shù)據(jù)庫算術(shù)推理）。

它基于給定的一組核心初始事實，計算所有可推導(dǎo)事實的集合，遵循一組固定的演繹規(guī)則迭代地將新事實添加到集合中，直到不能再添加為止。

DDAR既負責生成語言模型的訓練數(shù)據(jù)，在測試時也負責搜索推理步驟。

DDAR2有三個主要改進：

增加處理兩個名稱不同但坐標相同的點的能力。   

更快的算法：提取所有關(guān)鍵規(guī)則并硬編碼，把最壞情況的時間復(fù)雜度從8次方減少到三次方級別；舍棄了關(guān)于角度和距離的顯式規(guī)則，改為自動完成。

更快的代碼實現(xiàn)，從Python改成C++，在AMD EPYC 7B13 64核CPU上快了300倍。

全新的搜索算法SKEST

多個配置不同的搜索樹并行運行，通過知識共享機制相互啟發(fā)，從而更高效地尋找證明路徑。

在每個搜索樹中，一個節(jié)點包括一次輔助結(jié)構(gòu)構(gòu)造和符號引擎的嘗試。

如果成功了，所有搜索樹便會終止。

如果失敗了，這次嘗試成功證明的事實會被記錄到共享事實庫中，事實對同一搜索樹中的其他節(jié)點以及不同搜索樹中的節(jié)點都可能有用。

更強大的語言模型：最新Gemini

AlphaGeometry2的語言模型采用最新的Gemini架構(gòu)，設(shè)計了三種訓練方法：

• 在領(lǐng)域?qū)Ｓ谜Z言的自定義分詞器上從頭預(yù)訓練
• 在自然語言上微調(diào)預(yù)訓練的數(shù)學版Gemini
• 用額外的圖像輸入從頭開始多模態(tài)訓練。

通過實驗得出如下結(jié)論：

分詞器和訓練數(shù)據(jù)，都不是關(guān)鍵因素。

• 較小詞匯表的分詞器和通用Gemini分詞器，取得了相似的結(jié)果
• 自然語言訓練和領(lǐng)域?qū)Ｓ谜Z言訓練，也是相似的結(jié)果

視覺信息和圖示對解決幾何問題并不重要，幾何問題解決的核心在于代數(shù)推理，而不是幾何推理。

• 單獨使用多模態(tài)模型，沒有顯著提高系統(tǒng)的能力
• 多模態(tài)模型生成的輔助點與其他模型不同，通過知識共享和其他模型組合起來可以提高整體性能

One More Thing

2023年，專門為AI設(shè)立的數(shù)學競賽AIMO開辦，第一個獲得金牌的AI系統(tǒng)能贏500萬美元獎金，但要求系統(tǒng)必須開源。

雖然現(xiàn)在AlphaGeometry2已經(jīng)有了獲得金牌的能力，但他不開源。

對這個領(lǐng)域感興趣的團隊還有機會哦～

最后，2025年的IMO競賽將于7月份在澳大利亞舉行。

論文地址：https://arxiv.org/pdf/2502.03544