DeepMind AI解決本世紀以來84% IMO幾何題，達到真人金牌得主的水平

一年前，由GoogleDeepMind 創建的 AI 數學模型 AlphaGeometry 在國際數學奧林匹克競賽（IMO，International Mathematical Olympiad）中展現出比肩真人銀牌得主的水平。

近日，DeepMind 正式推出 AlphaGeometry2，它在 IMO 中達到真人金牌得主的水平，並能解決 21 世紀以來 25 屆 IMO 全部幾何問題的 84%。

而 AlphaGeometry1 僅能解決 54% 的問題，這意味著 AlphaGeometry2 可以像頂尖人類選手一樣解決棘手的數學問題。

（來源：https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry/）

對於過去 25 屆 IMO 幾何問題的覆蓋率，此前 AlphaGeometry1 的幾何問題覆蓋率為 66%，AlphaGeometry2 則將幾何問題覆蓋率提高到 88%。

英國倫敦帝國理工學院的數學家凱文·布紮德（Kevin Buzzard）告訴媒體：「我認為不久之後，計算機就會在 IMO 上獲得滿分。」

用合成技術為 AlphaGeometry 尋找解題思路

IMO 賽題以其高難度而聞名，解決這些賽題需要對數學概念有著深入的理解，並且能夠創造性地應用這些數學概念。幾何賽題是 IMO 四個賽題類別之一，非常適合基礎推理研究。但是，幾何賽題會對 AI 提出特定的技能要求，比如 AI 必須針對平面上幾何物體的陳述提供嚴格的證明。

自動解決幾何問題有兩種主要方法。一種是用代數的方法嘗試；另一種方法依賴於合成技術。DeepMind 的研究人員專注於後者，因為它是一種更像人類的方法，適合將研究知識轉移到其他領域。

儘管 AlphaGeometry1 取得了成功，但它在幾個關鍵領域表現出局限性。而且，它的性能受到其領域特定語言範圍、符號引擎效率和初始語言模型容量的限制。

為瞭解決上述局限性並提高性能，在打造 AlphaGeometry2 時，研究人員擴展了原始的 AlphaGeometry 語言，以便解決涉及到物體運動的幾何賽題，以及解決包含角度、比率和距離的線性方程賽題。

同時，研究人員通過使用 Gemini 架構進行了更好的語言建模，並結合多個搜索樹的新型知識共享機制讓 AlphaGeometry2 的搜索過程得到極大改進。此外，研究人員還進一步增強了符號引擎和合成數據的生成能力。

AlphaGeometry2，更強更快的符號引擎

符號引擎是 AlphaGeometry 的核心組件。DeepMind 將其稱之為演繹數據庫算術推理（DDAR，Deductive Database Arithmetic Reasoning）。它是一種計算演繹閉包的算法，即給定一組核心初始事實，計算所有可推論事實的集合。

DDAR 通過遵循一組固定的推理規則來構建這個推理閉包，然後不斷將新的事實添加到推理閉包中，直到無法再添加為止。DDAR 既能驅動語言模型的訓練數據生成，又驅動推理步驟的搜索。在這兩種情況之下，速度都至關重要。

更快的數據生成，將能產生更多以及更有力的數據過濾。而更快的證明搜索，則能帶來更加廣泛的搜索。這樣一來，就能增加 AlphaGeometry2 在給定時間內找到解決方案的可能性。

為了提高速度，研究人員通過在 C++ 中實現其核心計算（高斯消元法）來進一步提高速度。新的 C++ 庫通過 Pybind11 導出到 Python，通過此所打造的 DDAR2 比 DDAR1 快了 300 多倍。

為了針對速度提升進行基準測試，研究人員找出 25 個 DDAR 無法解決的 IMO 問題，並在配備 AMD EPYC 7B13 64 核 CPU 上運行 50 次測試。

結果顯示，DDAR1 平均需要 1179.57±8.055 秒才能完成計算，而 DDAR2 的速度要快得多僅需 3.44711±0.05476 秒即可完成。

AlphaGeometry2，利用多個搜索樹進行知識共享

在 AlphaGeometry1 中，研究人員使用了比較簡單的集束搜索。在 AlphaGeometry2 中，研究人員設計了一種新的搜索算法，其能並行執行幾個不同配置的集束搜索，並允許通過知識共享機制相互幫助。（註：集束搜索，‌是一種啟髮式圖搜索算法，主要用於解決解空間較大的問題，並能減少搜索所需的時間和空間消耗。）

為了提高系統的魯棒性，研究人員為每個搜索樹配置使用了多種不同的語言模型，並將這種搜索算法稱為搜索樹共享知識集成（SKEST，Shared Knowledge Ensemble of Search Trees）。

其工作原理如下：在每個搜索樹中，一個節點對應於一次輔助構造嘗試，隨後是一次符號引擎運行嘗試。如果嘗試成功，則所有搜索樹終止。如果嘗試失敗，節點將把符號引擎設法證明的事實寫入共享事實數據庫。

這些共享事實經過過濾之後，便不再是特定於節點本身的輔助點，而僅僅與原始問題相關。這樣一來，這些事實對於同一搜索樹中的其他節點以及不同搜索樹中的節點也可以起到作用。

對於證明搜索，研究人員使用Google的 AI 芯片 TPUv4 來為每個模型提供多個副本，並讓同一模型內的不同搜索樹根據自己的搜索策略查詢同一服務器。（註：證明搜索，指的是機器在產生正確策略的過程中，會通過回溯來探索新的替代方案。）

除了異步運行這些搜索樹外，研究人員還使用 DDAR workers 異步運行 LM workers。LM workers 將研究人員所探索的節點內容寫到數據庫中，然後 DDAR workers 異步地拾取這些節點並進行嘗試。

研究人員表示，DDAR workers 通過相互協調來確保它們能夠平等地分配工作。如果是一次解決多個問題，單個 DDAR 工作池會在不同問題之間共享，這樣一來先前已被解決的問題就會釋放自己的 DDAR 計算資源，從而用於其餘正在解決中的問題。

AlphaGeometry2，利用 Gemini 架構進行訓練

研究人員表示，AlphaGeometry1 的語言模型是一個自定義轉換器，它採取無監督的方式，並分為兩個階段進行訓練。它先是針對擁有輔助結構和沒有輔助結構的問題進行培訓，然後再只針對包含輔助結構的題進行培訓。

而對於 AlphaGeometry2，研究人員利用 Gemini 訓練流程並將訓練過程簡化為一個階段：即對所有數據進行無監督學習。

與此同時，研究人員本次使用的新語言模型是一個基於稀疏混合專家 Transformer 的模型，該模型以 Gemini 為基礎，並在 AlphaGeometry2 數據上進行訓練。

在打造 AlphaGeometry2 的時候，研究人員使用三種訓練設置來訓練多個大小不同的模型。除了創建大約 3 億條定理的大型綜合訓練集外，其還創建了三個評估集。所有這些評估集都包含完整的證明，同時在訓練期間研究人員會計算它們的困惑度損失。

需要指出的是，和 AlphaGeometry1 一樣的是，研究人員在推理過程中只使用語言模型建議的輔助點，並在整個證明上計算困惑度。同樣與 AlphaGeometry1 一樣的是，研究人員的主要下遊指標是達成 IMO 賽題的解決率，而語言模型可以生成輔助點，然後通過集束搜索運行 DDAR。

研究中，研究人員使用 TPUv4 以硬件允許的最大 batch 大小來訓練模型。在下圖中，研究人員展示了不同大小的 Gemini 模型在參數計數方面的學習曲線。

通過以上努力，研究人員讓 AI 學會瞭解答幾何題。數學對 AI 模型來說真的很難，解答幾何題需要複雜的推理技能，許多 AI 研究人員認為解決數學問題的能力可能預示著更強大、更智能的系統。

像 AlphaGeometry 這樣的創新表明，人類正在開發具有人類一樣推理技能的機器。這可以讓人類構建更強大的 AI 工具，用於幫助數學家求解方程，也許還可以成為更好的輔導工具。

AlphaGeometry2 將在第 66 屆 IMO 再「秀肌肉」

儘管 AlphaGeometry2 初步結果不錯，但是研究人員認為仍然可以通過更多的形式化示例和監督微調，該進一步提高 AlphaGeometry2 的解題能力。

目前，受限於研究人員的領域語言（domain language），AlphaGeometry2 還不能解決可變點數、非線性方程和不等式等問題，而只有解決這些問題 AlphaGeometry2 才能實現 100% 地解決幾何問題。

另外，AlphaGeometry2 並沒有解決 IMO 和 IMO 短名單（IMOSL，International Mathematical Olympiad Shortlisted Problems）的所有賽題。研究人員認為，未來將這些賽題分解為子問題，並使用強化學習方法或許可以縮小這一差距。

另據悉，第一個在 IMO 測試中獲得金牌的 AI 系統將贏得 AI Mathematical Olympiad Prize，並將獲得 500 萬美元的獎金。不過該獎勵要求算法必須是開源的，因此 AlphaGeometry2 並不符合這一要求。

值得注意的是，2025 年 7 月研究人員將帶著 AlphaGeometry2 參加第 66 屆 IMO，屆時或許會帶來新的成績。

參考資料：

https://www.nature.com/articles/d41586-025-00406-7

https://arxiv.org/pdf/2502.03544

運營/排版：何晨龍