Nature重磅：做高中生奧數題，AI接近人類金牌選手了

來源：焦糖老乾媽釋出時間：2024-01-18 15:21

Nature重磅：做高中生奧數題，AI接近人類金牌選手了

水平接近人類金牌選手，人工智慧（AI）學會做國際數學奧林匹克競賽難題了。

這個名為 AlphaGeometry 的 AI 模型由來自 Google DeepMind 和紐約大學的聯合團隊研發，是一個能解國際數學奧林匹克競賽級別幾何題的 AI 系統，於今日登上了頂級科學期刊 Nature。

據介紹，AlphaGeometry 透過自主合成數百萬個定理和證明，解決了 30 個最新奧林匹克級別（優等高中生參加的數學定理證明大賽）問題中的 25 個，接近國際數學奧林匹克競賽金牌選手的平均表現，遠超之前最好的自動化定理證明系統。

這一突破標誌著 AI 在數學問題解決方面取得了顯著的進展——無需人類演示即可自主應對複雜的幾何學挑戰。

該研究證明了 AI 能以接近人類最高水平破解複雜邏輯挑戰的潛力——這正是 AI 研究的一個主要目標。

值得一提的是，AlphaGeometry 能生成人類可閱讀的證明，甚至發現了 2004 年國際數學奧林匹克競賽定理的一個新版本。

相關研究論文以“Solving olympiad geometry without human demonstrations”為題，剛剛發表在 Nature 上。

AI 搞定奧數題，很難嗎？

自 20 世紀 50 年代以來，追求更好的定理證明能力一直是 AI 研究的焦點。數學奧林匹克競賽是世界上最著名的定理證明競賽，其歷史可以追溯到 1959 年，在發現卓越人才方面有著重要作用。

國際數學奧林匹克競賽的題目通常涉及深度的數學理論和抽象的數學概念，需要獨立思考、創造性解決問題和運用直覺。這些問題往往要求高度的邏輯推理和創造性的思維，這是人類數學家所具備的，但超越了傳統的機器學習方法的應用範圍。

此外，與其他領域相比，人類解決數學問題的過程不容易轉化為大規模的可用於訓練的資料集。幾何學具有特有的翻譯困難，在通用數學語言中的證明示例也很少。並且幾何語言具有非常精準的定義，無法表達許多使用幾何範圍之外的人類證明，比如複數。

圖｜IMO2000P6的人類證明和 AlphaGeometry 證明的並排比較。這是一個較難的問題（人類平均得分 = 1.05/7），問題陳述中包含大量物件。左圖，人類解決方案使用複數。透過精心選擇的座標系，問題會大大簡化，並且透過代數運算自然可以得出解決方案。右圖，AlphaGeometry 解決方案涉及兩個輔助構造和100多個推導步驟，其中許多低階步驟對於人類來說極其乏味。在這種情況下，基於搜尋的解決方案的可讀性和直觀性要差得多。更具結構性的組織，即高階的證明大綱，可以大大提高AlphaGeometry 解決方案的可讀性。在AlphaGeometry中構建許多高階推導規則，有助於減少低階推導並簡化證明步驟。（來源：該論文）

缺乏足夠的樣本資料，特別是包含人類專業數學家的解答過程，使得機器學習模型難以學習和理解解題方法。因此，目前的幾何方法仍主要依賴於符號方法和人工設計的硬編碼搜尋啟發式。

無需人類，自主解決複雜問題

在該研究中，AlphaGeometry 的關鍵創新點在於，其能夠綜合數百萬條複雜程度各異的定理和證明，利用從頭訓練的神經語言模型進行自主訓練。這意味著 AlphaGeometry 能夠獨立學習和解決各類複雜問題，而無需依賴人類輸入。

神經語言模型在引導符號演繹引擎（能夠搜尋難題中的大量分支點）方面具有獨特的優勢。神經模型的引入使得 AlphaGeometry 在處理具有挑戰性的問題時能夠做出更為精準的推理。這種綜合運用符號演繹引擎和神經語言模型的方法是該研究的重要創新之一。

圖｜AlphaGeometry 概述以及它如何解決簡單問題和IMO2015問題3。頂行顯示 AlphaGeometry 如何解決簡單問題。a）簡單的例子及其圖表。b）模型透過執行符號推演引擎來啟動證明搜尋。引擎從定理前提中詳盡地推匯出新的陳述，直到定理被證明或新的陳述被窮舉為止。c）由於符號引擎未能找到證明，語言模型構造一個輔助點，在符號引擎重試之前增長證明狀態。迴圈繼續直到找到解決方案。d）對於簡單的例子，迴圈在第一個輔助結構“D作為BC的中點”之後終止。該證明包括另外兩個步驟，這兩個步驟都利用了中點屬性：“BD = DC”和“B、D、C 共線”。底行顯示了 AlphaGeometry 如何解決 IMO 2015 Problem 3 (IMO 2015 P3)。e）IMO 2015 P3 問題陳述和圖表。f IMO 2015 P3的解有3個輔助點。（來源：該論文）

儘管 AlphaGeometry 在解決奧林匹克級別的幾何問題上取得了顯著的成功，但也存在一些侷限性。

據論文描述，AlphaGeometry 主要專注於解決奧林匹克級別的幾何問題，應用範圍相對狹窄。這限制了該方法在其他數學領域或實際問題中的推廣。未來的研究需要探討如何擴充套件該方法以涵蓋更廣泛的數學領域。

而且，研究團隊採用了大規模的人工合成數據來訓練 AlphaGeometry，這雖然為模型提供了廣泛的學習材料，但合成數據仍然可能無法完全覆蓋真實數學問題的多樣性和複雜性。因此，模型在真實場景中的效能可能會受到資料不足的影響。

此外，雖然 AlphaGeometry 能夠生成人類可讀的證明，但在處理極其複雜的推理時，其生成的結果可能變得難以理解。這使得人們在一些情況下難以追蹤和解釋模型的推理過程。

解決數學問題，AI 大有可為

近年來，使用 AI 技術來理解和證明數學定理，是科學家們重點關注的研究方向之一。

例如，AI 可以被用來開發自動定理證明系統，這些系統可以獨立地推導和證明數學定理。這種方法旨在減輕人工證明的負擔，並提供更高效的證明方法。

此外，AI 也可以被用來構建數學知識圖譜，有助於將數學概念之間的關係建模成圖結構。這種圖譜可以用於改進定理的推理和證明，使得系統能夠更好地理解數學領域的知識體系。

對於創造性思維的開發，AI 也有一席之地。一些研究採用生成式模型，比如生成對抗網路（GANs），來生成符合數學結構和規範的新定理。這種方法有助於拓展數學領域的創造性思維，引入新的數學概念和結論。

當然，要使得 AI 在數學領域展現出如人類頂尖數學家一般的水平，還有很長的路要走。

儘管如此，AlphaGeometry 展現出了 AI 在數學方面的應用潛力，這一成果不僅為數學領域帶來了創新，也為 AI 在其他領域的應用帶來了新的可能。

論文連結：