史上首次，AI超越人類奧賽金牌得主！吳方法加持，30題做出27道破紀錄

新智元報道

編輯：編輯部

【新智元導讀】就在剛剛，首位超越人類數學奧賽金牌得主的AI誕生了！劍橋大學等機構的研究者發現，結合「吳方法」的DeepMind數學模型AlphaGeometry，在解決奧數題時直接秒殺了人類IMO金牌得主，30道幾何題中做對了27道。

首位超越國際奧林匹克競賽金牌得主的AI，剛剛誕生了！

印度理工學院海得拉巴分校、圖賓根AI中心、劍橋大學的研究者發現——

通過「吳方法」，可以讓AI變成和人類數學奧賽銀牌得主同樣的水平，而「AI數學大師」AlphaGeometry，則直接超越了IMO金牌得主。

吳方法，是吳文俊在1970年代提出的開創性算法。

經過改進後，它變得非常強大，可以解決國際數學奧林匹克競賽30個問題中的27個！直接秒殺人類。

相比之下，之前的AlphaGeometry，僅能解決25個。

論文地址：https://arxiv.org/abs/2404.06405

項目地址：https://huggingface.co/datasets/bethgelab/simplegeometry

之前曾有人估計，到2026年代，AI才能達到IMO人類金牌得主的水平。而如今，這個時間表再次被打破了。

AI做IMO奧數題，有新SOTA了

證明幾何定理是視覺推理的重要表現，它融合了直覺和邏輯思維。

因此，自動化證明奧林匹克級別的幾何題目，代表着人類級自動推理的一個重要里程碑。

此前推出的AlphaGeometry，是一個通過1億個合成樣本訓練的神經符號模型，代表了一個重大的突破。

論文地址：https://www.nature.com/articles/s41586-023-06747-5

它成功解決了國際數學奧林匹克（IMO）30個問題中的25個，而傳統的基於吳方法的系統，僅能解決10個。

但這一次，研究者們重新評估了AlphaGeometry引入的IMO-AG-30挑戰，有了新的發現——

吳方法異常強大！

僅靠吳方法，就能解決15個問題，其中一些問題是靠其他方法根本無法解決的。

而這就帶來了兩個關鍵發現：

1. 通過將「吳方法」和經典的演繹數據庫（DD）以及角度、比率和距離追蹤（AR）的合成方法相結合，僅使用一臺配備CPU的筆記本，在每個問題的5分鐘限時內，就能解決30個問題中的21個。

這種經典組合方法（Wu&DD+AR）僅比AlphaGeometry少解決了4個問題，並建立了第一個完全基於符號的基準，其性能足以與國際數學奧林匹克（IMO）銀牌得主媲美。

2. 吳方法還解決了AlphaGeometry未能解決的5個問題中的2個。

因此，現在IMO-AG-30有新的SOTA了！

通過將AlphaGeometry與吳方法結合產生的新AI，直接解決了30個問題中的27個，一舉超越IMO金牌得主，成爲世上首個達此成就的AI。

歐氏幾何，AI推理能力的試金石

如何測試AI的推理能力強不強？歐幾里得幾何就是一個很好的標準。

因爲，歐幾里得幾何已經被有限地公理化了，而且這麼多年來，有許多非常適合自動定理證明的歐幾里得幾何證明系統被提了出來。

此外證明的搜索可以通過圖形表示、概率驗證，或是使用人類設計的啓發式方法，來對角度、面積和距離進行大量推理引導。

國際數學奧林匹克中，這些方法被參賽者戲稱爲「三角破解」和「重心破解」。

還有一件有趣的事，就是這個領域的缺陷——它需要定義特定的證明系統來指定問題，缺乏訓練數據，問題時常涉及複雜的退化情況。

這些困難非常棘手，由此坊間有這樣一句戲言——「幾何問題永遠不會解決退化問題。」

在幾何自動推理領域，可以將方法分爲代數方法和合成方法。

演繹數據庫（DD）這個合成方法就頗受關注。

它會模仿人類的證明技巧，通過將定理證明視爲依據一組幾何公理進行的逐步搜索問題，從而生成易於理解的證明。

比如，DD會採用一組固定的、由專家策劃的幾何規則，這些規則會不斷地應用到初始的幾何配置上，直至系統達到一個狀態，即用現有規則無法推導出新的事實爲止。

而神經符號證明器AlphaGeometry在這一領域取得了突破性的進展。

在DD的基礎上，它增加了新的規則，用於進行角度、比率和距離的追蹤（AR），並通過大模型（DD+AR+LLM-構造）提出的構建方法，進一步增強了由此生成的符號引擎。該模型是基於1億個合成證明訓練的。

而吳方法和Gröbner基方法之類的代數方法，能夠將幾何假設，轉換成多項式系統，來驗證結論。

這些方法已被證實，能夠有效處理廣泛的幾何問題。

其中，對於所有假設和結論都能用代數方程表示的問題，吳方法都能處理，並且還能自動產生非退化條件。

而這就表明，吳方法不僅適用於平面幾何問題，也適用於固體和更高維的幾何問題。

5秒解決14個問題

今年1月，谷歌DeepMind團隊同時推出了新的基準測試IMO-AG-30。

這是團隊從2000年至2022年間競賽題中，篩選出30道經典幾何問題組成的測試集，目的是爲了展示AlphaGeometry的性能。

基準中，問題的解決數量與IMO選手的平均解題數量相對應。

如下圖，灰色水平線所示，銅牌、銀牌和金牌得主平均分別解決了19.3個、22.9個和25.9個問題。

所有參賽者平均解題數爲15.2。

IMO-AG-30收集的具體問題集在圖1（B）的左列中有所列出。

（A）在IMO-AG-30問題集上，符號系統和增強型大模型（LLM-Augmented）的表現，以及與人類表現的對比

（B）展示了不同方法在解決IMO-AG-30問題集時的情況

實驗

研究人員根據Trinh等人提供的基線和數據集，使用IMO-AG-30基準進行性能評估。

他們通過JGEX軟件手動將IMO-AG-30問題轉換成兼容格式，並重新實現了吳方法。

同時，研究者也從AlphaGeometry代碼庫中成功重現了必要的DD+AR基線。

經過手動驗證了自己翻譯的幾個問題，團隊確認JGEX生成的假設和結論方程是正確的。

吳方法解決了AlphaGeometry未能解決的兩個問題，方案插圖如下所示。

2008-P1B（JGEX）：

生成的答案：

2021-P3（JGEX）：

生成的答案：

結果

研究結果與的先前結果，已經在圖1中進行了展示。

圖1（A）比較瞭解決問題的數量，圖1（B）展示了各種方法解決的具體問題，以此可視化不同方法之間的重疊或互補性。

具體來說，研究人員將吳方法與DD+AR結合，創建了一個新的符號性能基準（Wu&DD+AR），該基準比所有傳統方法多解決了6個問題。

這種組合解決了IMO-AG-30問題中的21個，與圖2中未經微調（僅FT-9M）的AlphaGeometry的表現相匹配。

（A）展示了在IMO-AG-30問題集上，符號方法和LLM增強（LLM-Augmented）方法的表現，以及與人類表現的對比

（B）展示了不同方法在IMO-AG-30問題上的表現

吳方法在非常低的計算需求下實現了這一表現。

在一臺裝有AMD Ryzen 7 5800H處理器和16 GB RAM的筆記本上，研究人員在5秒內解決了15個問題中的14個，其中一個問題（2015 P4）需要耗時3分鐘。

在實驗中，吳方法要麼幾乎立即解決問題，要麼在5分鐘內使筆記本內存耗盡。

值得一提的是，研究者通過吳方法解決的15個問題中的2個（2021 P3, 2008 P1B），原本是AlphaGeometry難以解決的5個問題之中的2個。

因此，通過簡單地將Wu的方法與AlphaGeometry結合，實現了在IMO-AG-30基準上解決了27個問題，這一成就在圖1的綠色/橙色條形（Wu&AG）中有所展示。

代數方法攻克IMO

代數方法，在自動化幾何推理中解決IMO幾何問題中，蘊藏着巨大的潛力。

這項研究恰恰印證了這一點，吳方法也從過往能夠解決10個問題，增加到了15個問題。

而這些問題中，有幾個對於目前流行的合成方法，以及增強LLM的方法，也具有非常高的挑戰性。

研究者表示，其設立的符號基線，是首個在性能上超越一般IMO參賽者，並接近銀牌水平。

此外，AlphaGeomtery和吳方法結合的系統，也是首個在IMO幾何問題上超越人類金牌得主的AI系統。

這一成就證明了，代數方法與合成方法在這一領域的互補性。特別是，2008 P1B和2021 P3這兩個問題目前僅有吳方法能解決，顯示了代數方法的獨特價值。

儘管代數方法以其理論保證而著稱，但之前因速度慢和難以爲人理解而受到質疑。

而最新的研究觀察顯示，吳方法在多個問題上的效率遠超預期，作者認爲不應僅因其無法生成人類可讀的證明而忽視它。

目前，研究還在進行中，受限於現有實現的不足，包括結構的限制和性能不佳。

研究者相信，傳統方法有可能超越AlphaGeometry的證明能力，並希望這份研究能促進這一領域經典計算方法軟件的改進。

另一方面，最新方法取得的顯著成功表明，儘管IMO幾何問題對人類具有挑戰性，但可能並未充分挑戰現代計算求解器的極限。

解題的成功更多依賴於，重複使用人定義的啓發式方法和有限的構造，而不是深入探索複雜的組合可能性。

這與國際象棋殘局的情況類似，其相對較早就被暴力求解器掌握了。

而研究人員希望這份研究，能激勵開發幾何領域自動定理證明器的新基準。

參考資料：

https://arxiv.org/abs/2404.06405