OpenAI 與 DeepSeek 卷得不可開交的時(shí)候，谷歌 DeepMind 的數(shù)學(xué)推理模型又偷偷驚艷了所有人。

在最新的一篇論文中，谷歌 DeepMind 介紹了全新進(jìn)化的 AlphaGeometry 2，該系統(tǒng)在解決奧林匹克幾何問題方面已經(jīng)超過了金牌得主的平均水準(zhǔn)。

• 論文標(biāo)題：Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
• 論文鏈接：https://arxiv.org/pdf/2502.03544

國(guó)際奧林匹克數(shù)學(xué)競(jìng)賽（IMO）是一項(xiàng)面向全球高中生的著名數(shù)學(xué)競(jìng)賽。IMO 問題以難度大著稱，解決這些問題需要對(duì)數(shù)學(xué)概念有深刻理解，并能創(chuàng)造性地應(yīng)用這些概念。幾何是 IMO 四大題型之一，各題型之間最為統(tǒng)一，非常適合基礎(chǔ)推理研究。因此，這項(xiàng)賽事也成為了衡量人工智能系統(tǒng)高級(jí)數(shù)學(xué)推理能力的理想基準(zhǔn)。

在 2024 年 7 月，谷歌 DeepMind 曾經(jīng)介紹了 AlphaGeometry (AG1)，這是一個(gè)神經(jīng)符號(hào)系統(tǒng)，在 2000-2024 年 IMO 幾何問題上的解題率達(dá)到 54%，距離金牌也只有一步之遙。AG1 將語(yǔ)言模型 (LM) 與符號(hào)引擎相結(jié)合，有效地解決了這些具有挑戰(zhàn)性的問題，造就了數(shù)學(xué)領(lǐng)域的「AlphaGo 時(shí)刻」。

盡管 AG1 取得了成功，但它在幾個(gè)關(guān)鍵領(lǐng)域仍存在局限性。其性能受限于特定領(lǐng)域語(yǔ)言的范圍、符號(hào)引擎的效率以及初始語(yǔ)言模型的容量。因此，在考慮 2000 年至今的所有 IMO 幾何問題時(shí)，AG1 只能達(dá)到 54% 的解題率。

最新的這篇論文介紹了 AlphaGeometry2（AG2），它是解決了這些限制的升級(jí)版本，并顯著提高了性能。AG2 利用了更強(qiáng)大的基于 Gemini 的語(yǔ)言模型，該模型是在一個(gè)更大、更多樣化的數(shù)據(jù)集上訓(xùn)練出來的。團(tuán)隊(duì)還引入了速度更快、更強(qiáng)大的符號(hào)引擎，并進(jìn)行了優(yōu)化，如減少規(guī)則集和增強(qiáng)對(duì)二重點(diǎn)的處理。此外，團(tuán)隊(duì)還擴(kuò)展了領(lǐng)域語(yǔ)言，以涵蓋更廣泛的幾何概念，包括軌跡定理（locus theorem）和線性方程（linear equation）。

為了進(jìn)一步提高性能，他們開發(fā)了一種新型搜索算法，可探索更廣泛的輔助構(gòu)造策略，并采用知識(shí)共享機(jī)制來擴(kuò)展和加速搜索過程。最后，他們?cè)诮⒁粋€(gè)用自然語(yǔ)言解決幾何問題的全自動(dòng)可信賴系統(tǒng)方面取得了進(jìn)展。為此，谷歌利用 Gemini 將問題從自然語(yǔ)言翻譯成 AlphaGeometry 語(yǔ)言，并實(shí)施了新的自動(dòng)圖解生成算法。

這些改進(jìn)最終大大提高了性能：AG2 在 2000-2024 年 IMO 所有幾何問題上的解題率達(dá)到了令人印象深刻的 84%，這表明人工智能在處理具有挑戰(zhàn)性的數(shù)學(xué)推理任務(wù)方面實(shí)現(xiàn)了重大飛躍，并超越了 IMO 金牌得主的平均水準(zhǔn)。

核心提升如下：

• 擴(kuò)展領(lǐng)域語(yǔ)言：涵蓋軌跡型定理、線性方程和非構(gòu)造性問題陳述；
• 更強(qiáng)更快的符號(hào)引擎：優(yōu)化了規(guī)則集，增加了對(duì)二重點(diǎn)的處理，以及更快的 C++ 實(shí)現(xiàn)；
• 先進(jìn)新穎的搜索算法：利用知識(shí)共享的多搜索樹；
• 增強(qiáng)的語(yǔ)言模型：利用 Gemini 架構(gòu)在更大和更多樣化的數(shù)據(jù)集上進(jìn)行訓(xùn)練。

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

符號(hào)引擎是 AlphaGeometry 的核心組件，谷歌稱之為演繹數(shù)據(jù)庫(kù)算術(shù)推理（Deductive Database Arithmetic Reasoning，DDAR）。它是一種計(jì)算演繹閉包的算法，即給定一組核心初始事實(shí)的所有可演繹事實(shí)集合。DDAR 遵循一組固定的演繹規(guī)則來構(gòu)建此演繹閉包，并迭代地將新的事實(shí)添加到演繹閉包中，直到無法再添加。

DDAR 驅(qū)動(dòng)語(yǔ)言模型的訓(xùn)練數(shù)據(jù)生成以及測(cè)試時(shí)證明搜索期間的演繹步驟搜索。在這兩種情況下，速度都至關(guān)重要。更快的數(shù)據(jù)生成可以達(dá)成更大規(guī)模、更積極的數(shù)據(jù)過濾，而更快的證明搜索可以實(shí)現(xiàn)更廣泛的搜索，從而增加給定時(shí)間預(yù)算內(nèi)找到解決方案的可能性。

DDAR 有以下三項(xiàng)主要改進(jìn)：

• 處理二重點(diǎn)（double ponit）的能力；
• 更快的算法；
• 更快的實(shí)現(xiàn)。

處理二重點(diǎn)

在重新實(shí)現(xiàn) DDAR 時(shí)，谷歌試圖保持與原始算法大致相同的邏輯強(qiáng)度，只是由于實(shí)現(xiàn)差異而稍微強(qiáng)一些（例如泰勒斯定理被更通用的圓心角定理取代）。然而，DDAR 缺少一個(gè)對(duì)解決難題至關(guān)重要的關(guān)鍵特性：它無法接受兩個(gè)名稱不同但坐標(biāo)相同的點(diǎn)。

例如，想象一個(gè)問題：在點(diǎn) ?? 處兩條線 ??,?? 相交，并打算證明 ?? 位于某個(gè)圓 ?? 上。最合理的方法可能是重構(gòu)，不證明 ??,?? 的交點(diǎn)在 ?? 上，而是證明 ??,?? 的交點(diǎn)在 ?? 上。這是等效的，但更容易證明，因?yàn)榭梢栽趫A上移動(dòng)角度。具體可參見圖 1。

要對(duì)雙重點(diǎn)推理實(shí)現(xiàn)這種重構(gòu)，需要執(zhí)行以下四個(gè)步驟：

• 構(gòu)造一個(gè)新點(diǎn)??′作為 ??,?? 的交點(diǎn)（不知道 ??′ 是否與 ?? 重合）。這是一個(gè)輔助構(gòu)造，必須由語(yǔ)言模型預(yù)測(cè)；
• 證明??位于??上；
• 由于??和??′都位于??,??上，得出?? = ??′；
• 因此??位于??上。

更快的算法

DDAR 算法可以處理一系列規(guī)則，并嘗試將每條規(guī)則應(yīng)用于所有點(diǎn)的組合。此過程涉及以下兩個(gè)部分：

• 候選搜索步驟，它的時(shí)間復(fù)雜度是點(diǎn)數(shù)的多項(xiàng)式；
• 子句匹配步驟，它的時(shí)間復(fù)雜度是每個(gè)前提的子句數(shù)的指數(shù)。

理論上，在 AG1 中搜索相似三角形候選的最壞情況是 ??(??^8)，這是最耗時(shí)的步驟之一。指數(shù)級(jí)子句匹配是另一個(gè)成本高昂的步驟。

DDAR 最耗時(shí)的兩個(gè)部分是搜索相似三角形和搜索圓內(nèi)接四邊形。在 AG2 中，谷歌設(shè)計(jì)了一種改進(jìn)的 DDAR2 算法。對(duì)于相似三角形，他們遍歷所有的點(diǎn)三元組，對(duì)它們的「形狀」進(jìn)行哈希處理。如果兩次識(shí)別出形狀，則檢測(cè)出相似的對(duì)。

對(duì)于圓內(nèi)接四邊形，谷歌遍歷所有對(duì)（點(diǎn)??、線段????），并對(duì)（??，??，∠??????）的值進(jìn)行哈希處理。如果這樣的三元組重復(fù)出現(xiàn)，就得到一個(gè)圓內(nèi)接四邊形。線段 ???? 或 ∠?????? 的「值」是指 AR 子模塊計(jì)算出的符號(hào)范式。該子模塊跟蹤角度、距離和對(duì)數(shù)距離之間的已知線性方程，了解其代數(shù)結(jié)果，并將任何線性表達(dá)式簡(jiǎn)化為其標(biāo)準(zhǔn)范式。

更快的實(shí)現(xiàn)

雖然新算法已經(jīng)顯著加快了 DDAR 的速度，但谷歌使用 C++ 實(shí)現(xiàn)其核心計(jì)算（高斯消元法），從而進(jìn)一步提升了速度。

新的 C++ 庫(kù)通過 pybind11 導(dǎo)出到 Python，速度是 DDAR1 的 300 多倍。為了對(duì)速度改進(jìn)進(jìn)行基準(zhǔn)測(cè)試，谷歌選擇了一組 25 道 DDAR 無法解決的 IMO 問題（見圖 8），并在配備 AMD EPYC 7B13 64 核 CPU 的機(jī)器上運(yùn)行測(cè)試 50 次。

結(jié)果顯示，DDAR1 平均可以在 1179.57±8.055 秒內(nèi)完成計(jì)算，但 DDAR2 的速度要快得多，在 3.44711 ± 0.05476 秒內(nèi)完成。

更好的合成訓(xùn)練數(shù)據(jù)

與 AG1 類似，谷歌使用的合成數(shù)據(jù)生成方法從隨機(jī)圖采樣開始，并使用符號(hào)引擎從中推斷出所有可能的事實(shí)。并且對(duì)于每個(gè)推斷出的事實(shí)，他們都使用回溯算法來提取可以證明事實(shí)的相應(yīng)前提、輔助點(diǎn)和推理步驟。

谷歌的數(shù)據(jù)生成方法刻意避免使用人為設(shè)計(jì)的問題作為初始圖種子，并嚴(yán)格從隨機(jī)圖開始。這種設(shè)計(jì)選擇消除了數(shù)據(jù)污染的風(fēng)險(xiǎn)，并允許探索可能超出現(xiàn)有人類知識(shí)的定理分布。

更大、更復(fù)雜的圖表和更好的數(shù)據(jù)分布。首先，谷歌擴(kuò)大數(shù)據(jù)生成的來源，并更仔細(xì)地重新平衡數(shù)據(jù)分布。圖 2 展示了 AG2 與 AG1 的訓(xùn)練數(shù)據(jù)比較：

• 探索兩倍大小的隨機(jī)圖，從而提取更復(fù)雜的問題；
• 生成的定理復(fù)雜了兩倍，即點(diǎn)和前提的數(shù)量；
• 生成的證明復(fù)雜了 10 倍，即證明步驟多 10 倍；
• 問題類型之間的數(shù)據(jù)分布更均衡；
• 有無輔助點(diǎn)的問題之間的數(shù)據(jù)分布更均衡。

更快的數(shù)據(jù)生成算法。谷歌還提升了數(shù)據(jù)生成算法的速度?；叵?AG1，谷歌首先在隨機(jī)圖上運(yùn)行演繹閉包，然后回溯以獲得可以證明閉包中每個(gè)事實(shí)的最小問題和最小證明。為了獲得 AG1 中的最小問題，必須從問題中徹底刪除不同的點(diǎn)子集，然后重新運(yùn)行 DDAR 以檢查可證明性。這樣的搜索可以找到基數(shù)最小的子集，但是作為指數(shù)級(jí)搜索，對(duì)于大量的點(diǎn)而言不可行。

因此，谷歌切換到圖 3 所示的貪婪丟棄算法，該算法僅使用線性數(shù)量的檢查來判斷一組點(diǎn)是否足以證明目標(biāo)。只要檢查是單調(diào)的（如果 ?? ? ??，則 check_provable (??) ? check_provable (??)），貪婪算法就保證找到一組關(guān)于包含（inclusion）的最小點(diǎn)集。

新穎的搜索算法

在 AG1 中，谷歌使用簡(jiǎn)單的束搜索來發(fā)現(xiàn)證明。在 AG2 中，他們?cè)O(shè)計(jì)了一種新穎的搜索算法，可以并行執(zhí)行多個(gè)不同配置的束搜索，并允許它們通過知識(shí)共享機(jī)制互相幫助，具體可見圖 4。為了提高系統(tǒng)的穩(wěn)健性，谷歌還為每個(gè)搜索樹配置使用多個(gè)不同的語(yǔ)言模型。這種搜索算法被稱為搜索樹的共享知識(shí)集合（Shared Knowledge Ensemble of Search Trees，SKEST） 。

該搜索算法的工作原理如下所示：在每個(gè)搜索樹中，一個(gè)節(jié)點(diǎn)對(duì)應(yīng)于一次輔助構(gòu)造嘗試，然后是一次符號(hào)引擎運(yùn)行嘗試。如果嘗試成功，所有搜索樹都會(huì)終止。如果嘗試失敗，節(jié)點(diǎn)將把符號(hào)引擎設(shè)法證明的事實(shí)寫入共享事實(shí)數(shù)據(jù)庫(kù)。這些共享事實(shí)經(jīng)過過濾，使它們不是特定于節(jié)點(diǎn)本身的輔助點(diǎn)，而僅與原始問題相關(guān)。這樣一來，這些事實(shí)也可以對(duì)同一搜索樹中的其他節(jié)點(diǎn)以及不同搜索樹中的節(jié)點(diǎn)產(chǎn)生助益。

系統(tǒng)設(shè)計(jì)細(xì)節(jié)。對(duì)于證明搜索，谷歌使用 TPUv4 為每個(gè)模型提供多個(gè)副本，并讓同一模型內(nèi)的不同搜索樹根據(jù)自身的搜索策略來查詢同一服務(wù)器。除了異步運(yùn)行這些搜索樹之外，谷歌還對(duì) DDAR 工作器與 LM 工作器進(jìn)行異步運(yùn)算，其中 LM 工作器將它們探索的節(jié)點(diǎn)內(nèi)容寫入數(shù)據(jù)庫(kù)，DDAR 工作器異步拾取這些節(jié)點(diǎn)并嘗試它們。DDAR 工作器之間相互協(xié)調(diào)，以確保它們平等分配工作。單個(gè) DDAR 工作器池在不同問題之間共享（如果一次解決多個(gè)問題），這樣先前解決的問題就會(huì)為正在解決的其余問題釋放自己的 DDAR 計(jì)算資源。

更好的語(yǔ)言模型

AG2 的最后一項(xiàng)改進(jìn)是使用新的語(yǔ)言模型。下面將討論全新的訓(xùn)練和推理設(shè)置。

訓(xùn)練設(shè)置

AG1 是一種定制版 Transformer，以無監(jiān)督方式分兩個(gè)階段進(jìn)行訓(xùn)練：先對(duì)有無輔助結(jié)構(gòu)的問題進(jìn)行訓(xùn)練，然后僅對(duì)包含輔助結(jié)構(gòu)的問題進(jìn)行訓(xùn)練。

對(duì)于 AG2，谷歌利用了 Gemini 訓(xùn)練流程并將訓(xùn)練簡(jiǎn)化為一個(gè)階段：對(duì)所有數(shù)據(jù)進(jìn)行無監(jiān)督學(xué)習(xí)。他們使用了一種基于稀疏混合專家（MoE）Transformer 的新模型，該模型以 Gemini 1.5 為基礎(chǔ)，并使用 AG2 數(shù)據(jù)進(jìn)行訓(xùn)練。

谷歌使用以下三種設(shè)置來訓(xùn)練不同大小的多個(gè)模型：

1. 使用領(lǐng)域特定語(yǔ)言中的自定義 tokenizer 從頭開始訓(xùn)練（AG1 設(shè)置）；

2. 使用自然語(yǔ)言微調(diào)已經(jīng)預(yù)訓(xùn)練的自定義專業(yè)數(shù)學(xué) Gemini 模型；

3. 使用額外的圖像輸入（給定幾何題的圖表）從頭開始進(jìn)行多模態(tài)訓(xùn)練。

谷歌使用 TPUv4，并以硬件允許的最大批大小訓(xùn)練模型。學(xué)習(xí)率計(jì)劃是先線性預(yù)熱，然后余弦退火。學(xué)習(xí)率超參由 scaling 定律確定。在圖 5 中，他們展示了基于參數(shù)量的不同大小的 Gemini 的學(xué)習(xí)曲線。正如預(yù)期的那樣，增加模型大小會(huì)降低訓(xùn)練、評(píng)估以及特殊 IMO 評(píng)估集的困惑度損失。

推理設(shè)置

在 AG2 中，谷歌在提出輔助構(gòu)造之前讓 LM 了解 DDAR 所做的推論，進(jìn)而豐富這個(gè)神經(jīng)符號(hào)接口。也就是說，他們將以下信息輸入到 LM 中

• ??_1：給定原始問題前提，DDAR 可推導(dǎo)出的事實(shí)集；
• ??_2：給定原始問題前提并假設(shè)目標(biāo)謂詞也為真，DDAR 可推導(dǎo)出的事實(shí)集；
• ??_3：數(shù)字正確的事實(shí)集（檢查圖表）。

競(jìng)賽結(jié)果

本文的主要下游指標(biāo)是 IMO 幾何題的解決率。2000-2024 年 IMO 共有 45 道幾何題，谷歌將它們轉(zhuǎn)化為了 50 道 AlphaGeometry 問題（稱該集合為 IMO-AG-50）。

圖 8 展示了主要結(jié)果，AlphaGeometry2 解決了 2000-2024 年 IMO 所有 50 道幾何題中的 42 道，從而首次超越了金牌得主平均水平。

表 4 中提供了更多詳細(xì)信息，其中將各種 AG2 配置與其他系統(tǒng)進(jìn)行了比較?？梢钥吹剑珹G2 實(shí)現(xiàn)了 SOTA。

在圖 7 中，針對(duì)通過前文「經(jīng)典」樹搜索與 DDAR 耦合的一個(gè)語(yǔ)言模型，谷歌將 IMO 解決率表示為了訓(xùn)練時(shí)函數(shù)（訓(xùn)練期間看到的 tokens）。有趣的是，AG2 僅在批大小為 256 時(shí)的 250 個(gè)時(shí)間步后（或者大約 2 億 tokens），就解決了 50 道幾何題中的 27 道。

谷歌還對(duì)推理設(shè)置如何影響整體性能進(jìn)行了消融實(shí)驗(yàn)，結(jié)果如圖 9 所示。他們發(fā)現(xiàn)，對(duì)于單個(gè)搜索樹，最優(yōu)配置是束大小 128、束深度 4 以及樣本 32。