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

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

這個名為 AlphaGeometry 的 AI 模型由來自 Google DeepMind 和紐約大學(xué)的聯(lián)合團隊研發(fā)，是一個能解國際數(shù)學(xué)奧林匹克競賽級別幾何題的 AI 系統(tǒng)，于今日登上了頂級科學(xué)期刊 Nature。

據(jù)介紹，AlphaGeometry 通過自主合成數(shù)百萬個定理和證明，解決了 30 個最新奧林匹克級別（優(yōu)等高中生參加的數(shù)學(xué)定理證明大賽）問題中的 25 個，接近國際數(shù)學(xué)奧林匹克競賽金牌選手的平均表現(xiàn)，遠超之前最好的自動化定理證明系統(tǒng)。

這一突破標(biāo)志著 AI 在數(shù)學(xué)問題解決方面取得了顯著的進展——無需人類演示即可自主應(yīng)對復(fù)雜的幾何學(xué)挑戰(zhàn)。

該研究證明了 AI 能以接近人類最高水平破解復(fù)雜邏輯挑戰(zhàn)的潛力——這正是 AI 研究的一個主要目標(biāo)。

值得一提的是，AlphaGeometry 能生成人類可閱讀的證明，甚至發(fā)現(xiàn)了 2004 年國際數(shù)學(xué)奧林匹克競賽定理的一個新版本。

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

AI 搞定奧數(shù)題，很難嗎？

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

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

此外，與其他領(lǐng)域相比，人類解決數(shù)學(xué)問題的過程不容易轉(zhuǎn)化為大規(guī)模的可用于訓(xùn)練的數(shù)據(jù)集。幾何學(xué)具有特有的翻譯困難，在通用數(shù)學(xué)語言中的證明示例也很少。并且?guī)缀握Z言具有非常精準(zhǔn)的定義，無法表達許多使用幾何范圍之外的人類證明，比如復(fù)數(shù)。

圖｜IMO2000P6的人類證明和 AlphaGeometry 證明的并排比較。這是一個較難的問題（人類平均得分 = 1.05/7），問題陳述中包含大量對象。左圖，人類解決方案使用復(fù)數(shù)。通過精心選擇的坐標(biāo)系，問題會大大簡化，并且通過代數(shù)運算自然可以得出解決方案。右圖，AlphaGeometry 解決方案涉及兩個輔助構(gòu)造和100多個推導(dǎo)步驟，其中許多低級步驟對于人類來說極其乏味。在這種情況下，基于搜索的解決方案的可讀性和直觀性要差得多。更具結(jié)構(gòu)性的組織，即高級的證明大綱，可以大大提高AlphaGeometry 解決方案的可讀性。在AlphaGeometry中構(gòu)建許多高級推導(dǎo)規(guī)則，有助于減少低級推導(dǎo)并簡化證明步驟。（來源：該論文）

缺乏足夠的樣本數(shù)據(jù)，特別是包含人類專業(yè)數(shù)學(xué)家的解答過程，使得機器學(xué)習(xí)模型難以學(xué)習(xí)和理解解題方法。因此，目前的幾何方法仍主要依賴于符號方法和人工設(shè)計的硬編碼搜索啟發(fā)式。

無需人類，自主解決復(fù)雜問題

在該研究中，AlphaGeometry 的關(guān)鍵創(chuàng)新點在于，其能夠綜合數(shù)百萬條復(fù)雜程度各異的定理和證明，利用從頭訓(xùn)練的神經(jīng)語言模型進行自主訓(xùn)練。這意味著 AlphaGeometry 能夠獨立學(xué)習(xí)和解決各類復(fù)雜問題，而無需依賴人類輸入。

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

圖｜AlphaGeometry 概述以及它如何解決簡單問題和IMO2015問題3。頂行顯示 AlphaGeometry 如何解決簡單問題。a）簡單的例子及其圖表。b）模型通過運行符號推演引擎來啟動證明搜索。引擎從定理前提中詳盡地推導(dǎo)出新的陳述，直到定理被證明或新的陳述被窮舉為止。c）由于符號引擎未能找到證明，語言模型構(gòu)造一個輔助點，在符號引擎重試之前增長證明狀態(tài)。循環(huán)繼續(xù)直到找到解決方案。d）對于簡單的例子，循環(huán)在第一個輔助結(jié)構(gòu)“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 在解決奧林匹克級別的幾何問題上取得了顯著的成功，但也存在一些局限性。

據(jù)論文描述，AlphaGeometry 主要專注于解決奧林匹克級別的幾何問題，應(yīng)用范圍相對狹窄。這限制了該方法在其他數(shù)學(xué)領(lǐng)域或?qū)嶋H問題中的推廣。未來的研究需要探討如何擴展該方法以涵蓋更廣泛的數(shù)學(xué)領(lǐng)域。

而且，研究團隊采用了大規(guī)模的人工合成數(shù)據(jù)來訓(xùn)練 AlphaGeometry，這雖然為模型提供了廣泛的學(xué)習(xí)材料，但合成數(shù)據(jù)仍然可能無法完全覆蓋真實數(shù)學(xué)問題的多樣性和復(fù)雜性。因此，模型在真實場景中的性能可能會受到數(shù)據(jù)不足的影響。

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

解決數(shù)學(xué)問題，AI 大有可為

近年來，使用 AI 技術(shù)來理解和證明數(shù)學(xué)定理，是科學(xué)家們重點關(guān)注的研究方向之一。

例如，AI 可以被用來開發(fā)自動定理證明系統(tǒng)，這些系統(tǒng)可以獨立地推導(dǎo)和證明數(shù)學(xué)定理。這種方法旨在減輕人工證明的負(fù)擔(dān)，并提供更高效的證明方法。

此外，AI 也可以被用來構(gòu)建數(shù)學(xué)知識圖譜，有助于將數(shù)學(xué)概念之間的關(guān)系建模成圖結(jié)構(gòu)。這種圖譜可以用于改進定理的推理和證明，使得系統(tǒng)能夠更好地理解數(shù)學(xué)領(lǐng)域的知識體系。

對于創(chuàng)造性思維的開發(fā)，AI 也有一席之地。一些研究采用生成式模型，比如生成對抗網(wǎng)絡(luò)（GANs），來生成符合數(shù)學(xué)結(jié)構(gòu)和規(guī)范的新定理。這種方法有助于拓展數(shù)學(xué)領(lǐng)域的創(chuàng)造性思維，引入新的數(shù)學(xué)概念和結(jié)論。

當(dāng)然，要使得 AI 在數(shù)學(xué)領(lǐng)域展現(xiàn)出如人類頂尖數(shù)學(xué)家一般的水平，還有很長的路要走。

盡管如此，AlphaGeometry 展現(xiàn)出了 AI 在數(shù)學(xué)方面的應(yīng)用潛力，這一成果不僅為數(shù)學(xué)領(lǐng)域帶來了創(chuàng)新，也為 AI 在其他領(lǐng)域的應(yīng)用帶來了新的可能。

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