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

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

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

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

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

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

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

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

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

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

AlphaGeometry2四大升級(jí)

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

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

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

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

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

在進(jìn)行補(bǔ)充之后，覆蓋率從66%提高到88%。

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

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

對(duì)于這些問題，AI只能跳過，在圖中標(biāo)記為“Not attempted”。

更強(qiáng)大、更快的符號(hào)推理引擎DDAR2

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

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

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

DDAR2有三個(gè)主要改進(jìn)：

增加處理兩個(gè)名稱不同但坐標(biāo)相同的點(diǎn)的能力。   

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

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

全新的搜索算法SKEST

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

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

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

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

更強(qiáng)大的語言模型：最新Gemini

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

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

通過實(shí)驗(yàn)得出如下結(jié)論：

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

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

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

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

One More Thing

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

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

對(duì)這個(gè)領(lǐng)域感興趣的團(tuán)隊(duì)還有機(jī)會(huì)哦～

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

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