谷歌AI可媲美奧賽金牌選手，但為何只侷限在這些幾何題？_風聞

圖片由董彬老師用DALL-E生成

撰文 | 高國雄、姜傑東、董彬

八年前，橫空出世的AlphaGo橫掃圍棋賽場，點燃了人工智能的熱潮，也從根本上改變了圍棋領域。近日，谷歌Deepmind團隊一篇瞄準國際奧林匹克競賽（IMO）幾何題目的論文“AlphaGeometry”[1]再度一石激起千層浪。國內外對此已有鋪天蓋地的報道與討論，諸如“解決前沿數學問題指日可待”“奧賽金牌近在咫尺”等評價將大眾對人工智能解數學題的期許推上了新的高峯。本文將深度解讀AlphaGeometry，簡要分析其與之前最好的基準模型的差距，並對該模型的發展前景給予評述。

01

模型概述

圖1

歐氏幾何題目因其規範的敍述和標準化的解題流程，是各類國內國際數學競賽的“常客”。平面幾何相比其他數學領域所具有的封閉性、簡潔性、可驗證性，也讓它更適合機器證明。上世紀七十年代，吳文俊院士提出的“吳方法”[2]是這一領域的奠基之作，而隨後湧現的推理數據庫 (deductive database，簡記為DD) 方法[3, 4]則在保留證明的有效性的同時，大大提升了證明的可解釋性。

圖2

以文獻[3]為例，DD的核心是一系列包括共線、平行、中點、共圓、等角、等比等歐氏幾何基本要素的共七十五條的推理規則。在給定的圖形中，DD系統可以從給定前提（premises）出發，反覆應用這些推理規則，不斷得到新的結論，直到所有可能得到的結論都被窮盡。此時所有生成的定理按其推理路徑組成一個有向無環圖，這被稱為在給定圖形中指定前提的推理閉包（deduction closure）。此時，如果待證的結論就在推理閉包中，回溯證明路徑就得到一個合規的證明。在圖1中，以BE⊥AC，AD⊥BC為前提，往證∠EBC=∠DAC，DD在搜索中很容易通過BE⊥AC,AD⊥BC⇒∠ADB=∠AEB⇒AEDB共圓⇒∠EBC=∠DAC的路徑得到結論。

然而，DD並不能在現有的圖形基礎上添加任何輔助點，這大大限制了DD的表達能力。在圖2中，對△ABC，以AB=AC作為前提，除非添加一個輔助點，如AB中點D，否則DD系統無法在推理閉包中得到∠ABC=∠ACB的結論。即便是如此簡單的初中幾何題目也超出了DD的能力範疇，因此，添加輔助點的能力對幾何推理系統的重要性不言自明。對於高難度的平面幾何競賽題目來説，光靠DD這種遍歷搜索的方法，而不依賴輔助點的添加，是不可能取得好成績的。

在AlphaGeometry這篇工作中，作者還在DD的基礎上，額外使用了用於處理角、邊的相加和比例關係的線性代數規則系統 (algebraic rules，簡記為AR) 以補充DD的推理能力的不足。後面我們把DD和AR聯合的推斷系統記為DD+AR。

儘管DD+AR已有較強的推理能力，但還是無法解決添加輔助點的問題。在過去的研究中，人們就已經設計了啓發式的（heuristic）策略來添加輔助點以拓展DD和AR的搜索空間。AlphaGeometry在自己構建的30道IMO題目上測試DD+AR+heuristic，可以做對其中的18道題。在這個基礎上，AlphaGeometry的主要貢獻是訓練了一個151M大小的語言模型來代替啓發式算法，以實現更好的加輔助點策略，獲得了從做對18道題目到25道題目的進步。

為訓練這一語言模型，作者首先利用已有的DD+AR框架合成了大量數據。添加輔助點被限定在約五十條規則組成的框架內。通過反覆進行“運行DD+AR生成定理閉包→隨機添加輔助點”的循環，我們可以得到一個足夠複雜的有向無環推理依賴圖，每個節點均為一個結論，每條邊為所調用的推理規則。對任意一個結論進行反向回溯搜索其最小生成樹，可以得到“<所用前提>，<所得結論>，<證明路徑>”的三元組，這就是用於訓練語言模型的一個數據。在調用100,000個CPU線程並行運算72小時後，作者得以生成約5億個數據，排除重複後剩餘約1億個，其中約900萬個包含“添加輔助點”的步驟。最終使用的語言模型為先在這1億個數據上預訓練，再在這900萬個含添加輔助點步驟的數據上微調得到。

圖3

在解決實際幾何問題時，AlphaGeometry以給定的前提和基礎圖作為根節點和初始篩選節點，在每輪中先對當前全部進行篩選的節點運行DD+AR以生成推理閉包。如果此時往證結論仍未出現，則在所有篩選節點的所有可能加輔助點的方案中，選取在語言模型中生成概率最高的512個作為下一輪的篩選集合。循環將持續進行，直到篩選輪數達到設定的搜索深度或往證結論在某個推理閉包中出現時終止。

如圖3所示，通過反覆交替調用DD+AR和語言模型，讓二者分別專注於幾何推理和輔助點構造，AlphaGeometry得以解決多數IMO幾何題目。按論文作者估算，在1.5小時限時（這是IMO競賽中每道題的平均限時）下，提供四個並行的V100加速的語言模型和76個CPU線程就足以解決AlphaGeometry能解決的25道題目中的24道。這證明了AlphaGeometry構架的有效性。

02

評價

總的來説，AlphaGeometry能解決所選的共30題的IMO題集中的25道，已經展現了其在幾何推理上的有效性。下面，我們從兩個方面對AlphaGeometry的能力和潛力進行評價。

1．DD+AR系統的侷限性

圖4

AlphaGeometry高度依賴DD+AR系統，其精心訓練的語言模型要和DD+AR的體系配合。因此，AlphaGeometry的能力也被DD+AR系統的表達能力所侷限。

如圖4所示，設D是正△ABC外一點，滿足DB⊥AC且∠ADC=120°。往證DA⊥AB。這是一道容易通過簡單的角度計算給出證明的題目。然而，這隻對D落在△ABC外的情形成立！如果失去了“設D是正△ABC外一點”這一描述位置關係的條件，便無法區分圖中D，D’兩點。即使所有其他前提敍述都不改變，結論也不再成立。DD+AR系統所使用的語言無法描述“D在△ABC外”這一相對位置關係，無論添加多少輔助點都無濟於事。這種對位置關係的依賴在IMO等級的題目中通過精巧的設計與規範得以儘量避免，卻在歐氏幾何所囊括的定理中廣泛存在。甚至在許多不追求規範性的題目中，題幹根本不使用文字敍述點明位置關係，僅僅敍述“如圖”二字而已。另外，DD+AR體系的推理，在所有取點互異的暗含前提下才是可靠的（例如DD中有一條規則是若ABC共線且ABD共線則CDA共線，這一論斷在AB重合時不成立）。

即便不考慮組合幾何和幾何不等式，以上兩種情況在所有值得考慮的平面幾何定理中佔比約30%。進而，DD+AR+LM（語言模型）的組合也只能支持考慮約70%的幾何題目。因此，DD+AR系統限制了AlphaGeometry的可拓展性。

2. 所訓練的語言模型帶來的實際增益

想要客觀分析語言模型帶來的增益，我們應當將AlphaGeometry (DD+AR+LM) 與DD+AR+heuristics（啓發式添輔助點）相比較。在考慮為訓練LM所耗費的龐大算力資源和一億的數據量後，前者解決25/30道題目的成績相比後者18/30道的增益並不足夠顯著。

必須指出，雖然AlphaGeometry同屬“Alpha”家族，但與AlphaGo不同，它並非利用強化學習維護一個高效的策略（policy），而是使用純粹的監督學習。這也意味着，模型並不會利用其在部署後進行推斷時的搜索的正確與否來不斷修正自己的權重。不過，想要將現有的監督模型改造為強化學習模型，DD+AR框架的高延遲（每次生成推理閉包需要幾秒到幾分鐘）是營造強化學習所需的即時大量反饋的環境的一大阻礙。

另一方面，考慮到在搜索深度（即調用語言模型來添加輔助點的次數）為4和2時，模型仍有能做出25道和21道的表現，可見想實現優秀的推理能力，並不需要很高的搜索深度。這表明在AlphaGeometry中，對分析、搜索推理空間的貢獻更多集中在DD+AR，而非所訓練的語言模型。

03

總結

AlphaGeometry給出了一個能夠解決IMO難度的平面幾何題目的有效架構。然而，受限於DD+AR的表示能力，想要將這篇工作的架構拓展到標準平面幾何剩下的約30%題目十分困難。同時，DD+AR充分利用了平面幾何簡潔明確的推理結構，但也因此被侷限在幾何的範疇內，難以拓展到數學其他領域。不過，利用DD+AR提供的回溯功能，我們可以對已證明的定理給出多種不同的回溯路徑，也就給出同一個結論的不同證明方法。這能否對學生學習幾何證明給予有效的指導，有待進一步考證。

正如論文所提到的，這篇工作所着手的對象範圍較為狹窄，其核心原因在於形式化數據的不足。以Lean為代表的一系列形式化數學語言為自動定理證明提供了邏輯嚴密、表達能力強且能自動驗證的交互環境，這是解決類似於DD+AR這樣的小領域符號引擎的表達能力限制的突破口。只有聯合Lean community等形式化社羣進行更全面、廣泛的形式化數學數據的積累和收集，AI4Math才能有本質上的進展。

文獻

[1] Trinh, T.H., Wu, Y., Le, Q.V. et al. Solving olympiad geometry without human demonstrations. Nature 625, 476–482 (2024). https://doi.org/10.1038/s41586-023-06747-5

[2] Wu, W.-T. On the decision problem and the mechanization of theorem-proving in elementary geometry. Sci. Sin. 21, 159–172 (1978)

[3] Chou, S. C., Gao, X. S. & Zhang, J. Z. A deductive database approach to automated geometry theorem proving and discovering. J. Autom. Reason. 25, 219–246 (2000)

[4] Ye, Z., Chou, S. C. & Gao, X. S. in Proc. Automated Deduction in Geometry: 7th International Workshop, ADG 2008 (eds Sturm, T. & Zengler, C.) 189–195 (Springer, 2011). geometry. Sci. Sin. 21, 159–172 (1978).

本文經授權轉載自微信公眾號“北京國際數學研究中心BICMR”，原標題為《簡評DeepMind新作AlphaGeometry》。

特 別 提 示

1. 進入『返樸』微信公眾號底部菜單“精品專欄“，可查閲不同主題系列科普文章。

2. 『返樸』提供按月檢索文章功能。關注公眾號，回覆四位數組成的年份+月份，如“1903”，可獲取2019年3月的文章索引，以此類推。