新智元報(bào)道
編輯：編輯部【新智元導(dǎo)讀】谷歌DeepMind的AI，終于拿下IMO金牌了！六個(gè)月前遺憾摘銀，如今一舉得金，SKEST新算法立大功。這不，它首破解了2009 IMO最難幾何題，輔助作圖的神來之筆解法讓谷歌研究員當(dāng)場(chǎng)震驚。時(shí)隔6個(gè)多月，AlphaGeometry 2直接攻下IMO金牌！
剛剛，谷歌DeepMind一篇28頁(yè)技術(shù)報(bào)告，公布了AG2最新突破
在2000-2024年IMO幾何題上，解題率從54%飆升至84%。
論文地址：https://arxiv.org/pdf/2502.03544
過去近25年IMO幾何真題（50道），AG2橫掃了42道。要知道，這個(gè)成績(jī)已經(jīng)大幅超于歷年IMO金牌得主的平均水平。
去年7月，谷歌曾官宣的兩大AI系統(tǒng)AlphaProof和AlphaGeometry 2，距離金牌只有1分之遙。
論文中，團(tuán)隊(duì)專為AG2設(shè)計(jì)了一種全新搜索算法基于知識(shí)共享集成的搜索樹（SKEST），允許多個(gè)集束搜索（beam search）并行運(yùn)行并相互幫助。
得益于這算法，AG2能夠在19秒內(nèi)，解決IMO 2024年P(guān)4題。
谷歌DeepMind高級(jí)研究科學(xué)家Thang Luong稱，「這是AI首次破解了2009年IMO最難幾何題G7（備選題）」。
此前，這道題只有計(jì)算性解法（使用復(fù)數(shù)、三角計(jì)算等）。
令人驚訝的是，AG2利用關(guān)鍵的輔助作圖（圖中的紅點(diǎn)），給出了一個(gè)只需要「角度」和「比例推導(dǎo)」的優(yōu)雅解法。
這些點(diǎn)，是由神經(jīng)符號(hào)架構(gòu)中的「神經(jīng)網(wǎng)絡(luò)模型」預(yù)測(cè)得出的。
有網(wǎng)友表示，「AGI似乎在谷歌內(nèi)部實(shí)現(xiàn)了」。
AG2，一舉超越IMO金牌得主
作為全球最具權(quán)威的高數(shù)競(jìng)賽，IMO幾何題不僅考驗(yàn)選手對(duì)數(shù)學(xué)概念深刻理解，更需要極強(qiáng)的創(chuàng)造性思維。而今天，數(shù)學(xué)這個(gè)人類智慧的結(jié)晶，正被人工智能以驚人的速度攻克。
在當(dāng)時(shí)看來，這個(gè)成績(jī)已是相當(dāng)?shù)伢@人。
AG1使用了簡(jiǎn)單特定域語(yǔ)言，主要由表1列出的九個(gè)基本的「謂詞」組成
不過，AG1仍在幾個(gè)關(guān)鍵領(lǐng)域存在局限性，比如特定語(yǔ)言范圍、符號(hào)引擎效率，以及初始語(yǔ)言模型的能力均會(huì)影響其性能。
新一代AlphaGeometry 2，得到了全新升級(jí)。
它采用了基于Gemini更強(qiáng)大的語(yǔ)言模型，其在更大更多樣化數(shù)據(jù)集中完成訓(xùn)練，顯著提升了理解和推理能力。
同時(shí)，谷歌還引入了更快速、更穩(wěn)健的「符號(hào)引擎」，融入了簡(jiǎn)化規(guī)則集、增強(qiáng)雙重點(diǎn)處理等優(yōu)化。
此外，模型領(lǐng)域語(yǔ)言范圍也進(jìn)行了擴(kuò)展，涵蓋了更廣泛的幾何概念，包括軌跡定理和線性方程。
為了進(jìn)一步提升性能，團(tuán)隊(duì)還開發(fā)了一種新型搜索算法，探索更多樣的輔助作圖策略，并采用知識(shí)共享機(jī)制，來擴(kuò)展和加速搜索過程。
AG2最令人矚目的進(jìn)展之一是，完全自動(dòng)化的處理能力。
它可以直接理解自然語(yǔ)言形式的幾何問題，借助Gemini團(tuán)隊(duì)的技術(shù)將問題轉(zhuǎn)化為專用語(yǔ)言，實(shí)現(xiàn)了一種全新的「自動(dòng)圖形生成」算法。
得益于以上的改進(jìn)，AG2在所有IMO幾何題上，取得了令人印象深刻的84%解題率。
這意味著，它已經(jīng)超越了IMO金牌得主的平均水平。
總結(jié)來說，AG2帶來了幾項(xiàng)重大升級(jí)：
擴(kuò)展了領(lǐng)域特定語(yǔ)言（DSL）的覆蓋范圍，可覆蓋88%的IMO幾何題目，相比此前的66%有顯著提升
改進(jìn)了符號(hào)引擎，使其更加穩(wěn)健，且速度提升了兩個(gè)數(shù)量級(jí)
增強(qiáng)了語(yǔ)言模型，該模型基于Gemini并在更大規(guī)模（提升一個(gè)數(shù)量級(jí)）和更多樣化的數(shù)據(jù)集上訓(xùn)練
創(chuàng)新性地提出了一種名為「基于知識(shí)共享集成的搜索樹」（SKEST）的新算法，能夠?qū)崿F(xiàn)多個(gè)搜索樹之間的知識(shí)共享
更通用的域語(yǔ)言，覆蓋88%題目
如上，表1列出的AG1九個(gè)基本「謂詞」，已經(jīng)覆蓋了2000-2024年IMO幾何題目中66%的問題。但是，AG1的語(yǔ)言無(wú)法表達(dá)線性方程、點(diǎn)/線/圓的移動(dòng)，也無(wú)法處理「求角度...」這樣的常見問題。
由此，谷歌研究人員在AG1的基礎(chǔ)上，增加了兩個(gè)「謂詞」，可以解決「查找X」類型的問題：
另外，在某些幾何問題中，包括IMO 2024中的一道題目，存在AG1無(wú)法表達(dá)的幾何量（角度、距離）的線性方程。
為了表達(dá)這些概念，AG2增加了以下三個(gè)謂詞：
還有一點(diǎn)是，AG1不支持所謂的「軌跡問題」，這類問題涉及點(diǎn)、線和圓等對(duì)象的運(yùn)動(dòng)，AG2則通過新的謂詞語(yǔ)法捕捉這類問題。
表2列出了11種軌跡情況及其對(duì)應(yīng)的謂詞和語(yǔ)法。這里使用了一個(gè)新的符號(hào)*作為固定點(diǎn)的占位符。
除此以外，AG2通過引入一個(gè)新的謂詞 overlap a b（點(diǎn)A和點(diǎn)B是重合點(diǎn)）來證明點(diǎn)的非獨(dú)立性，其中涉及A的任何謂詞也可以用于B，反之亦然。
在推理閉包（deduction closure）過程中，重合點(diǎn)可以通過作為同一個(gè)圓的圓心來定義；
因此，團(tuán)隊(duì)引入另一個(gè)謂詞cyclic_with_center來描述這種情況。因此，cyclic_with_center a1 a2 ... an x表示a_1=a_2=...=a_x是經(jīng)過點(diǎn)a_x+1...a_n的圓的圓心（當(dāng)x=0 時(shí)，等同于cyclic）。
自動(dòng)形式化和圖形生成
自動(dòng)形式化AG1以及其他類似的神經(jīng)符號(hào)系統(tǒng)有一個(gè)主要弱點(diǎn)，需要手動(dòng)將自然語(yǔ)言的輸入轉(zhuǎn)換成特定領(lǐng)域的語(yǔ)言。
例如，一個(gè)簡(jiǎn)單的自然語(yǔ)言幾何問題「給定三角形ABC，其中兩邊相等AB=AC，證明角B和角C相等」，在AlphaGeometry的領(lǐng)域特定語(yǔ)言中變成了：「triangle a b c; a b = a c ? eqangle b a b c c b c a」。
在AG2中，團(tuán)隊(duì)首先通過人工將幾十個(gè)幾何問題翻譯成AG語(yǔ)言。然后，使用這些示例編寫少樣本提示，要求Gemini將給定的幾何問題從自然語(yǔ)言翻譯成AG語(yǔ)言。
用這個(gè)提示在Gemini中查詢五次，然后再調(diào)用一次將這些結(jié)果合并成一個(gè)最終答案。
通過這種方法，AG2能夠?qū)MO 2000-2024中的39個(gè)幾何問題形式化30個(gè)。對(duì)于簡(jiǎn)單的幾何問題，這種方法非常有效，幾乎沒有錯(cuò)誤。
自動(dòng)圖形生成對(duì)于無(wú)法直接通過幾何作圖構(gòu)建的圖形（非構(gòu)造性問題），AG2采用兩階段數(shù)值優(yōu)化方法：
第一階段使用ADAM梯度下降優(yōu)化，最小化誤差，同時(shí)防止點(diǎn)重合和坐標(biāo)值過大。第二階段使用Gauss-Newton-Levenberg（高斯-牛頓-勒文伯格）方法，求解非線性方程組，得到精確的圖形坐標(biāo)。
研究團(tuán)隊(duì)在44道IMO問題上進(jìn)行了基準(zhǔn)測(cè)試，經(jīng)過上面的優(yōu)化后，AG2能夠?yàn)槠渲?1個(gè)問題找到圖形。
大多數(shù)問題在AG2第一次嘗試時(shí)，甚至幾秒鐘內(nèi)就生成了圖形。對(duì)于剩余的問題，也可以通過更長(zhǎng)的運(yùn)行時(shí)間和更多的并行化運(yùn)算獲得圖形。
例如，在使用了3333個(gè)進(jìn)程運(yùn)算了400分鐘后，AG2獲得了IMO-2011-6（2011年IMO第6題）的圖形。
更強(qiáng)大、更快的符號(hào)引擎
AlphaGeometry2的核心是「符號(hào)引擎」DDAR（演繹數(shù)據(jù)庫(kù)與算術(shù)推理）。
這是一種用來計(jì)算「演繹閉包」的算法。
所謂演繹閉包，就是從一堆最基本的已知事實(shí)出發(fā)，通過推理能得到的所有事實(shí)的集合。
DDAR有一套固定的推理規(guī)則，然后它會(huì)按照這些規(guī)則，一步步地推導(dǎo)出新的事實(shí)，把新事實(shí)加到集合里，直到?jīng)]法再推出新的東西為止。
這使它能在兩個(gè)方面發(fā)揮關(guān)鍵作用：一是為語(yǔ)言模型生成訓(xùn)練數(shù)據(jù)，二是在測(cè)試時(shí)進(jìn)行證明搜索，尋找演繹步驟。
在這兩種情況下，速度都至關(guān)重要。
更快的數(shù)據(jù)生成意味著可以進(jìn)行更大規(guī)模、更徹底的數(shù)據(jù)過濾；而更快的證明搜索則意味著可以使得搜索更廣泛，從而增加了在給定時(shí)間內(nèi)找到解決方案的可能性。
DDAR的三個(gè)主要改進(jìn)：處理重合點(diǎn)的能力（可以理解為處理更復(fù)雜幾何圖形的能力）、更快的算法和更快的實(shí)現(xiàn)。
處理重合點(diǎn)在AG1中，如果兩個(gè)點(diǎn)在幾何上重合，但名稱不同，則系統(tǒng)無(wú)法識(shí)別它們是同一個(gè)點(diǎn)。例如，如果兩條線a和b相交于點(diǎn)X，而我們想證明X在某個(gè)圓ω上，AG1可能會(huì)難以處理這種情況。
AG2通過允許使用具有不同名稱但坐標(biāo)相同的點(diǎn)來解決這個(gè)問題。
這種處理重合點(diǎn)的能力非常重要，因?yàn)樗试SAG2通過「重新表述」來解決問題。在某些情況下，直接證明某個(gè)點(diǎn)位于某個(gè)圓上可能很困難，但通過引入輔助點(diǎn)并證明該輔助點(diǎn)具有相同的性質(zhì)，可以簡(jiǎn)化證明過程。
考慮一個(gè)證明兩條直線a和b的交點(diǎn)X在圓ω上的例子。
AG2可以通過以下步驟實(shí)現(xiàn)：首先，創(chuàng)建一個(gè)新的點(diǎn) X'，該點(diǎn)是a和ω的交點(diǎn)；接下來，證明X'位于b上。由于X和X'都位于a和b上，可以得出結(jié)論，X和X'是同一點(diǎn)，從而證明X位于ω上。
下圖1直觀地展示了上述證明過程。
通過這些改進(jìn)，AG2可以更靈活地處理各種幾何問題，并且能夠以更接近人類思維的方式解決問題。
更快的算法AG1的DDAR算法在處理規(guī)則列表時(shí)，會(huì)嘗試將每條規(guī)則應(yīng)用于所有可能的點(diǎn)。
為了提高搜索效率，AG2直接硬編碼了其應(yīng)用搜索過程，從而減少了對(duì)AR子引擎的查詢次數(shù)，最多查詢?nèi)巍?br/>
AG2還丟棄了角度和距離的明確規(guī)則（例如關(guān)于垂直或平行線的規(guī)則），這些推導(dǎo)都自動(dòng)在AR引擎中進(jìn)行。此外，AG2設(shè)計(jì)了一種改進(jìn)的DDAR2算法。
通過這些改進(jìn)，AG2顯著提高了搜索速度和效率，從而加快了證明過程，使得AG2能夠更有效地解決復(fù)雜的幾何問題。
更快的實(shí)現(xiàn)AG2的核心計(jì)算部分，特別是高斯消元法，使用C++重新實(shí)現(xiàn)。為了與Python環(huán)境兼容，AG2使用pybind11將 C++庫(kù)導(dǎo)出到Python。
通過C++重新實(shí)現(xiàn)，AG2的速度比AG1快了300多倍。
這意味著AG2在相同的時(shí)間內(nèi)可以完成更多的計(jì)算，從而更有效地解決復(fù)雜的幾何問題。
更好的合成訓(xùn)練數(shù)據(jù)
AG2的成功很大程度上歸功于其改進(jìn)的合成訓(xùn)練數(shù)據(jù)。AG2使用與AG1相同的程序，但通過擴(kuò)大資源和改進(jìn)算法，生成了更大、更多樣化、更復(fù)雜的數(shù)據(jù)集，從而顯著提升了模型的性能。
AG2首先隨機(jī)采樣幾何圖形，然后使用符號(hào)引擎（DDAR）推導(dǎo)出所有可能的事實(shí)。對(duì)于每個(gè)推導(dǎo)出的事實(shí)，使用回溯算法提取相應(yīng)的前提、輔助點(diǎn)和推導(dǎo)步驟。
AG2嚴(yán)格從隨機(jī)圖開始，這樣可以消除數(shù)據(jù)污染的風(fēng)險(xiǎn)，并探索可能超出人類已知定理分布的定理。
這種方法與TongGeometry等依賴人類專業(yè)知識(shí)和現(xiàn)有問題圖來指導(dǎo)和過濾數(shù)據(jù)生成的方法形成了鮮明對(duì)比。
更大、更復(fù)雜的圖和更好的數(shù)據(jù)分布AG2探索的隨機(jī)圖大小是AG1的兩倍，從而可以提取更復(fù)雜的問題。
生成的定理在復(fù)雜性上提高了一倍，包括更多的點(diǎn)和前提。生成的證明步驟最多增加了10倍。
AG2在有和沒有輔助點(diǎn)的證明之間有更平衡的數(shù)據(jù)分布，比例接近50:50，而AG1中有輔助點(diǎn)的證明比例僅為9%。
下圖2展示了AG2相比于AG1中包含了更多復(fù)雜、更長(zhǎng)的問題，在每個(gè)問題類型中都有更平衡的分布。
更多類型的定理除了生成證明經(jīng)典陳述（如「AB = CD」）的定理外，AG2的數(shù)據(jù)生成算法還生成「軌跡」類型的問題，例如 「當(dāng)X在直線/圓Y上移動(dòng)時(shí)，Z在固定直線/圓T上移動(dòng)」。
AG2通過一個(gè)函數(shù)P(.)記錄每個(gè)點(diǎn)在隨機(jī)圖生成過程中的運(yùn)動(dòng)依賴性，從而支持軌跡類型問題的生成。
下表3顯示了P(.)函數(shù)的兩個(gè)示例，解釋了如何確定點(diǎn)的運(yùn)動(dòng)源。
更快的數(shù)據(jù)生成算法
AG1首先在隨機(jī)圖上運(yùn)行演繹閉包，然后「回溯」以獲得最小問題和證明。為了獲得AG1中的最小問題，必須窮舉地從問題中移除不同的點(diǎn)集，然后重新運(yùn)行DDAR來檢查可證明性。這對(duì)于大量的點(diǎn)來說是不可行的
AG2改用了貪心丟棄算法，該算法只需進(jìn)行線性次數(shù)的檢查，就可以判斷一組點(diǎn)是否足以證明目標(biāo)。只要檢查是單調(diào)的（如果A是B的子集，那么如果A可證明，則B也可證明），貪心算法保證能找到一個(gè)關(guān)于包含關(guān)系的最小點(diǎn)集。
新穎的搜索算法在AG2中，研究人員設(shè)計(jì)了一種新穎的搜索算法基于知識(shí)共享集成的搜索樹（SKEST）。
在每棵搜索樹中，一個(gè)節(jié)點(diǎn)對(duì)應(yīng)于一次輔助構(gòu)造嘗試以及隨后的符號(hào)引擎運(yùn)行。
如果該嘗試成功，所有搜索樹立即終止。如果嘗試失敗，該節(jié)點(diǎn)會(huì)將符號(hào)引擎成功證明的事實(shí)記錄到共享事實(shí)數(shù)據(jù)庫(kù)中。
經(jīng)過篩選，這些共享事實(shí)不會(huì)包含節(jié)點(diǎn)自身特有的輔助點(diǎn)，而只保留與原始問題相關(guān)的內(nèi)容，以確保它們對(duì)同一搜索樹中的其他節(jié)點(diǎn)以及不同搜索樹中的節(jié)點(diǎn)都具有價(jià)值。
為了確保搜索空間的不同部分都能得到有效探索，研究人員采用了以下幾種搜索樹：
「經(jīng)典」搜索樹：這種搜索樹使用與AG1相同的集束搜索，其中語(yǔ)言模型在每個(gè)節(jié)點(diǎn)僅生成一個(gè)輔助點(diǎn)。
在每個(gè)節(jié)點(diǎn)預(yù)測(cè)多個(gè)輔助點(diǎn)的搜索樹：語(yǔ)言模型被允許在每個(gè)樹節(jié)點(diǎn)生成多個(gè)輔助點(diǎn)。
這是可行的，因?yàn)檎Z(yǔ)言模型經(jīng)過訓(xùn)練，可以生成完整的證明，從輔助點(diǎn)開始，并依次推導(dǎo)出推理步驟。
盡管研究人員的目標(biāo)是讓模型在一次查詢中生成所有必要的輔助點(diǎn)，但在實(shí)踐中，他們發(fā)現(xiàn)通常需要多次調(diào)用模型，以利用先前生成的輔助點(diǎn)。允許模型生成多個(gè)輔助點(diǎn)能夠加速求解過程，并有效地增加搜索樹的深度。
訓(xùn)練設(shè)置AG1語(yǔ)言模型是一個(gè)自定義Transformer，在無(wú)監(jiān)督模式下經(jīng)過兩個(gè)階段的訓(xùn)練：首先在包含和不包含輔助構(gòu)造的題目上訓(xùn)練，然后僅在包含輔助構(gòu)造的題目上訓(xùn)練。
對(duì)于AG2，研究人員采用Gemini訓(xùn)練流水線，并將訓(xùn)練簡(jiǎn)化為一個(gè)階段，即在所有數(shù)據(jù)上進(jìn)行無(wú)監(jiān)督學(xué)習(xí)。
這個(gè)新語(yǔ)言模型是一個(gè)基于Gemini構(gòu)建的MoE模型，并在AG2的數(shù)據(jù)集上訓(xùn)練。
研究人員訓(xùn)練了多種不同規(guī)模的模型，采用三種訓(xùn)練方案：
1. 從零開始訓(xùn)練，使用領(lǐng)域特定語(yǔ)言（DSL）的自定義分詞器（與AG1相同）。2. 微調(diào)預(yù)訓(xùn)練的數(shù)學(xué)專用Gemini模型，使用自然語(yǔ)言進(jìn)行訓(xùn)練。3. 多模態(tài)訓(xùn)練，從零開始并額外引入圖像輸入，即幾何題目的圖示。
除了一個(gè)包含約3億條定理的大型合成訓(xùn)練集，研究人員還構(gòu)建了三個(gè)評(píng)估集：
1. 合成問題集「eval」：包含帶有和不帶有輔助點(diǎn)的問題。2. 合成問題集「eval_aux」：僅包含帶有輔助點(diǎn)的問題。3. IMO評(píng)估集「imo_eval」：由2000-2024年IMO中，AlphaGeometry先前成功解決的幾何問題組成。
所有這些評(píng)估集都包含完整的證明，研究人員在訓(xùn)練過程中計(jì)算它們的困惑度損失。
與AG1相同，主要衡量指標(biāo)是IMO題目的解答率，其中語(yǔ)言模型生成輔助點(diǎn)后，使用DDAR算法結(jié)合集束搜索進(jìn)行求解。
研究人員使用TPUv4進(jìn)行訓(xùn)練，并采用最大可能的批大小，以充分利用硬件資源。學(xué)習(xí)率調(diào)度策略為線性預(yù)熱（warm-up）+ 余弦退火（cosine anneal），其中學(xué)習(xí)率的超參數(shù)基于scaling laws設(shè)定。
圖5展示了不同規(guī)模Gemini模型的學(xué)習(xí)曲線（以參數(shù)量為度量）。
如預(yù)期所示，模型規(guī)模越大，訓(xùn)練集、評(píng)估集以及IMO評(píng)估集的困惑度損失均會(huì)降低。
推理設(shè)置在搜索算法方面，研究人員通過多個(gè)搜索樹和不同規(guī)模的語(yǔ)言模型來解決一個(gè)新的問題。
與AG1不同，研究人員使用了溫度t=1.0和k=32的top-k采樣。需要注意的是，高溫度和多個(gè)采樣對(duì)于解決IMO問題至關(guān)重要。
在貪心解碼模式下（即t=0.0，k=1，且不使用搜索樹），模型只能解決26個(gè)需要輔助構(gòu)造的問題中的2個(gè)。
而當(dāng)溫度提高到t=1.0并使用k=32個(gè)采樣（但不使用搜索樹）時(shí)，語(yǔ)言模型可以解決26個(gè)問題中的9個(gè)。
如果溫度低于t=1.0，則生成的輔助構(gòu)造不夠多樣化（見圖6）；而如果溫度過高，則會(huì)增加語(yǔ)言模型輸出的錯(cuò)誤領(lǐng)域語(yǔ)言語(yǔ)法的比例。
這個(gè)AI，顯示出超凡的創(chuàng)造力
谷歌團(tuán)隊(duì)中的幾位幾何專家和IMO獎(jiǎng)牌得主仔細(xì)看過AlhpaGeometry的解題過程后，忍不住贊嘆道：它展示出了超凡的創(chuàng)造力！
不同配置的AlphaGeometry2，以及其他系統(tǒng)的對(duì)比
比如，下面這條題的∠KIL是由中點(diǎn)和內(nèi)心形成的角度，這兩個(gè)幾何元素通常難以建立關(guān)聯(lián)，且無(wú)法直接通過主三角形ABC的角度來計(jì)算。
在傳統(tǒng)解法中，人類參賽者通常會(huì)借助三角函數(shù)、復(fù)數(shù)或其他計(jì)算方法來求解。而對(duì)于AlphaGeometry而言，其DDAR系統(tǒng)僅依靠基本的角度關(guān)系推導(dǎo)和比例關(guān)系推導(dǎo)，因此需要引入一些輔助點(diǎn)的構(gòu)造。
為此，AlphaGeometry在直線BI上巧妙地構(gòu)造了點(diǎn)E，使得∠AEB = 90°。這一構(gòu)造優(yōu)雅地將那些看似無(wú)關(guān)的幾何元素聯(lián)系起來，形成了兩對(duì)相似三角形：△ABE與△YBI、△ALE與△IPC。這些相似三角形產(chǎn)生了新的等角關(guān)系和等比關(guān)系，同時(shí)也揭示了點(diǎn)E與線段AB中點(diǎn)L之間的重要聯(lián)系。
要完成證明，關(guān)鍵在于證明兩組三角形的相似性：△AKI △BPY和△ALI △CPX，從而得出∠AIK = ∠BYP和∠AIL = ∠CPX。這一過程可以通過運(yùn)用前述相似三角形所產(chǎn)生的邊長(zhǎng)比例關(guān)系來完成。
正如開篇所述，下面這道題一直以來都只有計(jì)算性的解法，例如使用復(fù)數(shù)、三角計(jì)算或通過不等式進(jìn)行反證法。而AlphaGeometry既不能使用這些計(jì)算和推理工具，也不具備高級(jí)歐幾里得幾何知識(shí)。
但是，最終的結(jié)果卻出乎意料AlphaGeometry通過構(gòu)建關(guān)鍵的輔助作圖，在只用角度和比例追蹤的情況下，給出了一個(gè)優(yōu)雅的解決方案。
首先，AlphaGeometry證明了X和Z關(guān)于BI對(duì)稱，根據(jù)對(duì)稱性可知I是三角形XYZ的外心。由此可以證明AB = AC，根據(jù)對(duì)稱性可知三角形ABC是等邊三角形。
但是，這個(gè)問題的主要挑戰(zhàn)在于使用三角形XYZ是等邊三角形的條件，即XY=YZ及其循環(huán)變體。
為此，AlphaGeometry構(gòu)造了一系列關(guān)鍵三角形的外心：
D是三角形BXC的外心
