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

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

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

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

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

一、HAGeo的核心創(chuàng)新：啟發(fā)式輔助構(gòu)造

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

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

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

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

二、大幅提升的推理引擎

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

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

這種速度提升的秘密在于對推理規(guī)則的精心重新設(shè)計。研究團(tuán)隊發(fā)現(xiàn)，許多傳統(tǒng)規(guī)則在保持邏輯正確性的同時，可以用更高效的方式來表達(dá)。就像簡化復(fù)雜的數(shù)學(xué)公式，在不改變結(jié)果的前提下讓計算變得更快更簡潔。

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

三、更嚴(yán)苛的評測基準(zhǔn)：HAGeo-409

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

為了更全面地評估幾何證明系統(tǒng)的能力，研究團(tuán)隊構(gòu)建了一個全新的評測基準(zhǔn)HAGeo-409，包含409道經(jīng)過專業(yè)數(shù)學(xué)家評估的幾何題目。這個數(shù)據(jù)集就像從小測驗升級為綜合大考，不僅題目數(shù)量大幅增加，難度范圍也更加廣泛和均衡。

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

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

四、卓越的實驗表現(xiàn)

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

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

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

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

五、技術(shù)架構(gòu)的巧妙設(shè)計

HAGeo的技術(shù)架構(gòu)就像一個精心設(shè)計的工作流程，每個環(huán)節(jié)都有其特定的作用和價值。整個系統(tǒng)采用幾何特定語言來描述問題，這種語言就像數(shù)學(xué)的通用語言，能夠準(zhǔn)確表達(dá)各種幾何對象和關(guān)系。與AlphaGeometry只考慮點的方法不同，HAGeo的語言系統(tǒng)包括點、直線和圓等多種幾何對象，更貼近自然的幾何描述方式。

系統(tǒng)的核心工作流程可以比作一個經(jīng)驗豐富的數(shù)學(xué)老師的解題過程。首先，系統(tǒng)會將幾何問題轉(zhuǎn)換為內(nèi)部表示，建立一個包含所有幾何對象和關(guān)系的推理圖。然后，演繹數(shù)據(jù)庫引擎會像篩網(wǎng)一樣，通過暴力搜索所有可能的推理規(guī)則來發(fā)現(xiàn)新的幾何關(guān)系。

代數(shù)推理引擎則像一個精密的計算器，將長度、比率和角度關(guān)系轉(zhuǎn)換為線性方程，通過高斯消元法來發(fā)現(xiàn)隱藏的數(shù)學(xué)關(guān)系。這兩個引擎協(xié)同工作，就像左右手的配合，互補(bǔ)各自的優(yōu)勢。

當(dāng)基礎(chǔ)推理無法解決問題時，輔助構(gòu)造模塊就會發(fā)揮作用。這個模塊就像一個創(chuàng)意大師，能夠根據(jù)當(dāng)前幾何配置的特點，智能地選擇最有希望的輔助構(gòu)造。系統(tǒng)會通過數(shù)值計算來驗證每個候選輔助點的價值，只保留那些能夠產(chǎn)生非平凡幾何關(guān)系的構(gòu)造。

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

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

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

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

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

研究團(tuán)隊創(chuàng)建的HAGeo-409基準(zhǔn)測試也為該領(lǐng)域建立了新的標(biāo)準(zhǔn)。這個更加全面和嚴(yán)格的評測體系就像為競賽設(shè)定了新的規(guī)則，將推動整個領(lǐng)域向更高的目標(biāo)邁進(jìn)。

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

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

Q&A

Q1：HAGeo與AlphaGeometry相比有什么優(yōu)勢？

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

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

A：HAGeo使用啟發(fā)式策略，會尋找具有良好幾何性質(zhì)的輔助點，比如多條直線的交點、圓與直線的切點等。它通過數(shù)值計算驗證這些點是否能產(chǎn)生有用的幾何關(guān)系，就像經(jīng)驗豐富的數(shù)學(xué)老師根據(jù)圖形特點選擇最有希望的輔助構(gòu)造。

Q3：HAGeo-409基準(zhǔn)測試有什么特別之處？

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