HAGeo：讓計算機像奧數金牌選手一樣解幾何題的華盛頓大學新突破

這項由瑞士蘇黎世聯邦理工學院的段博艷、加州大學洛杉磯分校的梁肖等研究人員與微軟研究院合作完成的研究，于2025年11月發表在arXiv預印本平臺，論文編號為arXiv:2512.00097v1。有興趣深入了解的讀者可以通過該編號查詢完整論文。

想象一下，有一臺計算機能夠像國際數學奧林匹克競賽的金牌選手一樣，輕松解決那些讓普通人頭疼不已的幾何難題。這聽起來像是科幻小說中的情節，但華盛頓大學和微軟研究院的科學家們真的做到了。他們開發出一個名為HAGeo的系統，這個系統就像一個永不疲倦的數學天才，能夠自動解決復雜的幾何證明題，而且成績比之前最先進的AI系統還要好。

要理解這項研究的意義，我們可以把幾何證明想象成一場復雜的推理游戲。就像福爾摩斯破案一樣，你需要從已知的線索出發，通過嚴密的邏輯推理，一步步揭示最終的答案。傳統的幾何證明需要人類數學家具備豐富的經驗和敏銳的直覺，特別是在添加輔助線這個關鍵環節——這就像在推理過程中找到關鍵的突破口，往往決定著整個問題能否被解決。

在此之前，最強的幾何證明AI系統是谷歌的AlphaGeometry，它就像一個需要強大GPU支持的超級計算機，通過神經網絡來尋找解題的輔助構造。然而，HAGeo的研究團隊發現了一個令人意外的現象：即使用最簡單的隨機策略來添加輔助點，也能達到AlphaGeometry的水平。這個發現就像發現了一條通往寶藏的捷徑，讓他們意識到可能存在更優雅的解決方案。

基于這個洞察，研究團隊開發出HAGeo系統。這個系統最大的特點是完全依靠CPU運算，不需要昂貴的GPU或復雜的神經網絡，就像一個只需要紙筆就能工作的數學大師。更令人印象深刻的是，HAGeo在國際數學奧林匹克幾何題基準測試IMO-30上解決了30道題中的28道，達到了"金牌"水平，超越了AlphaGeometry的24道題成績。

一、HAGeo的核心創新：啟發式輔助構造

HAGeo系統的工作原理就像一個經驗豐富的幾何老師在解題時的思考過程。當面對一道幾何題時，系統首先會嘗試用基礎的推理規則去解決問題，這就像是用最直接的方法去驗證答案。如果基礎方法行不通，系統就會開始添加輔助構造，但不是盲目地嘗試，而是根據幾何圖形的特殊性質來選擇最有希望的輔助點。

這種啟發式方法就像一個熟練的廚師根據食材的特點來決定烹飪方式。HAGeo會尋找那些具有良好幾何性質的點，比如多條直線的交點、圓與直線的切點等。這些點之所以重要，是因為它們往往隱藏著圖形中的關鍵關系，就像拼圖中的關鍵拼塊，一旦找到就能讓整個圖案豁然開朗。

系統的智能之處在于它能夠通過數值計算來驗證某個輔助點是否真的有用。這個過程就像一個偵探在驗證線索的真實性，只有那些能夠產生非平凡幾何關系的點才會被采用。比如，如果一個新構造的點恰好位于某條重要直線上，或者與其他點形成特殊的角度關系，系統就會認為這個點很有價值。

研究團隊將這些啟發式方法分為六大類。第一類是尋找多條直線的交點，這就像找到幾條道路的匯合點，往往蘊含著重要的幾何信息。第二類是尋找直線與圓的交點，這類似于找到軌道與邊界的接觸點。第三類是利用中點的特殊性質，中點往往是對稱性的體現。第四類是反射變換，就像在鏡子中找到對應點。第五類是垂足構造，類似于找到最短距離點。最后一類是隨機構造，為系統提供了探索未知可能性的機會。

二、大幅提升的推理引擎

除了智能的輔助構造策略，HAGeo還對底層的推理引擎進行了重大改進，就像給一臺老式汽車換上了全新的發動機。傳統的DDAR（演繹數據庫和代數推理）引擎雖然功能強大，但運行速度相對較慢，這在處理復雜幾何問題時會成為瓶頸。

HAGeo的研究團隊通過優化推理規則和實現方式，將推理速度提升了約20倍。這種提升就像從步行改為開車，不僅大大節省了時間，還讓系統能夠在相同時間內嘗試更多的解題路徑。具體來說，在IMO-30測試中，原始AlphaGeometry的DDAR引擎平均需要42.77秒來處理一道題，而HAGeo只需要1.75秒。

這種速度提升的秘密在于對推理規則的精心重新設計。研究團隊發現，許多傳統規則在保持邏輯正確性的同時，可以用更高效的方式來表達。就像簡化復雜的數學公式，在不改變結果的前提下讓計算變得更快更簡潔。

比如，原來需要檢查多個條件的角度推理規則，現在可以通過更直接的方式來實現。這就像從繞遠路到走直線，雖然到達的目的地相同，但路徑更加高效。這種優化不僅體現在單個規則上，更重要的是在整個推理網絡中形成了更流暢的信息流動。

三、更嚴苛的評測基準：HAGeo-409

研究團隊意識到，僅僅在現有的測試基準上取得好成績是不夠的，就像一個學生只在簡單的練習題上表現優秀，并不能證明真正掌握了知識。現有的IMO-30基準測試雖然廣泛使用，但存在一些局限性：問題數量較少（只有30道題），難度分布不均勻，且大多數題目相對簡單。

為了更全面地評估幾何證明系統的能力，研究團隊構建了一個全新的評測基準HAGeo-409，包含409道經過專業數學家評估的幾何題目。這個數據集就像從小測驗升級為綜合大考，不僅題目數量大幅增加，難度范圍也更加廣泛和均衡。

HAGeo-409的構建過程就像精心策劃一場全面的能力測試。研究團隊從藝術問題解決網站收集了2000多道幾何題，然后通過人工智能輔助將這些自然語言描述的題目轉換為標準的幾何語言格式。這個過程就像把各種方言翻譯成統一的標準語言，確保系統能夠準確理解題目要求。

更重要的是，每道題目都配有專業的難度評級，范圍從1到7分，其中1分代表相對簡單，7分代表極具挑戰性。在HAGeo-409中，難度1-3分的題目有161道，占39%；難度3-4分的有112道，占27%；而最具挑戰性的6-7分題目也有22道。相比之下，IMO-30中70%的題目都屬于較簡單的1-3分范圍，平均難度只有2.85分，而HAGeo-409的平均難度達到3.47分。

四、卓越的實驗表現

在這個更加嚴苛的測試環境中，HAGeo展現出了令人印象深刻的能力。就像一位優秀的學生不僅在簡單題目上游刃有余，在困難題目上也能發揮出色。在IMO-30基準測試中，HAGeo解決了28道題目中的28道，達到了"金牌"級別的表現，明顯超越了AlphaGeometry的24道題成績。

更令人驚訝的是，即使是使用隨機策略添加輔助點的簡單版本，也能解決25道題目，與AlphaGeometry的成績相當。這個發現就像發現了一個被忽視的簡單真理，讓人重新思考問題的本質。它表明，幾何證明中輔助構造的重要性可能被低估了，而復雜的神經網絡可能并非必需。

在更具挑戰性的HAGeo-409基準測試中，HAGeo的優勢更加明顯。在8192次嘗試的設置下，HAGeo在最簡單的1-3分難度范圍內解決了149道題目中的149道，成功率達到92.5%，比AlphaGeometry高出19.2個百分點。在3-4分的中等難度范圍內，HAGeo解決了93道題目中的93道，成功率為83.0%，超過AlphaGeometry 43.7個百分點。

即使在最困難的6-7分題目中，HAGeo也成功解決了2道題目，而AlphaGeometry在這個難度級別上完全束手無策。這就像在奧數競賽中，不僅基礎題目全部正確，連最難的壓軸題也能解出幾道，展現了系統的全面能力。

五、技術架構的巧妙設計

HAGeo的技術架構就像一個精心設計的工作流程，每個環節都有其特定的作用和價值。整個系統采用幾何特定語言來描述問題，這種語言就像數學的通用語言，能夠準確表達各種幾何對象和關系。與AlphaGeometry只考慮點的方法不同，HAGeo的語言系統包括點、直線和圓等多種幾何對象，更貼近自然的幾何描述方式。

系統的核心工作流程可以比作一個經驗豐富的數學老師的解題過程。首先，系統會將幾何問題轉換為內部表示，建立一個包含所有幾何對象和關系的推理圖。然后，演繹數據庫引擎會像篩網一樣，通過暴力搜索所有可能的推理規則來發現新的幾何關系。

代數推理引擎則像一個精密的計算器，將長度、比率和角度關系轉換為線性方程，通過高斯消元法來發現隱藏的數學關系。這兩個引擎協同工作，就像左右手的配合，互補各自的優勢。

當基礎推理無法解決問題時，輔助構造模塊就會發揮作用。這個模塊就像一個創意大師，能夠根據當前幾何配置的特點，智能地選擇最有希望的輔助構造。系統會通過數值計算來驗證每個候選輔助點的價值，只保留那些能夠產生非平凡幾何關系的構造。

六、突破性意義和未來影響

HAGeo的成功具有多重意義，它不僅在技術上實現了突破，更重要的是驗證了一個重要的理念：有時候最優雅的解決方案來自于對問題本質的深刻理解，而非復雜技術的堆砌。這就像古代數學家僅憑紙筆就能證明深刻的幾何定理，現代計算機也可以通過巧妙的算法設計達到類似的效果。

從計算資源的角度來看，HAGeo的純CPU設計意味著更低的部署成本和更廣泛的應用可能性。這就像從需要大型發電廠的設備改為普通家用電器，讓更多的研究機構和教育單位能夠使用這種技術。這種可訪問性的提升可能會推動幾何證明自動化技術的普及。

在教育領域，HAGeo可能會成為數學教師的有力助手，幫助生成題目解答、驗證證明步驟，甚至為學生提供個性化的輔導。它就像一個永遠有耐心的數學導師，能夠反復演示解題過程，幫助學生理解幾何證明的邏輯。

對于數學研究而言，HAGeo展示了人工智能在形式化推理領域的巨大潛力。雖然目前主要專注于平面幾何，但其核心思想可能適用于更廣泛的數學領域。這就像掌握了一種通用的解題方法，可以舉一反三應用到其他數學分支。

研究團隊創建的HAGeo-409基準測試也為該領域建立了新的標準。這個更加全面和嚴格的評測體系就像為競賽設定了新的規則，將推動整個領域向更高的目標邁進。

說到底，HAGeo的研究向我們展示了一個令人振奮的可能性：計算機不僅可以進行復雜的數值計算，還能夠進行抽象的邏輯推理，甚至在某些方面超越人類的表現。這項研究就像在人工智能的能力邊界上又推進了一大步，讓我們看到了機器智能在形式化推理領域的無限潛力。

當然，這種技術突破也提醒我們思考人機協作的新模式。HAGeo不會取代數學家，但它可以成為數學研究和教育中的強大工具，就像計算器沒有取代數學家一樣，但極大地提升了計算效率。這種人機結合的方式可能會開啟數學研究和教育的新時代，讓復雜的幾何證明變得更加可及和高效。

Q&A

Q1：HAGeo與AlphaGeometry相比有什么優勢？

A：HAGeo最大的優勢是只需要CPU就能運行，不需要昂貴的GPU和神經網絡，但性能更好。在IMO-30測試中，HAGeo解決了28道題，而AlphaGeometry只解決了24道，而且運行速度快20倍。

Q2：HAGeo是如何添加輔助線的？

A：HAGeo使用啟發式策略，會尋找具有良好幾何性質的輔助點，比如多條直線的交點、圓與直線的切點等。它通過數值計算驗證這些點是否能產生有用的幾何關系，就像經驗豐富的數學老師根據圖形特點選擇最有希望的輔助構造。

Q3：HAGeo-409基準測試有什么特別之處？

A：HAGeo-409包含409道幾何題，比現有的IMO-30基準更全面嚴格。每道題都有專業的難度評級，平均難度3.47分比IMO-30的2.85分更高，能更好地測試幾何證明系統的真實能力。