原文來源：學(xué)術(shù)頭條

圖片來源：由無界 AI生成

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

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

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

這一突破標(biāo)志著 AI 在數(shù)學(xué)問題解決方面取得了顯著的進(jìn)展——無需人類演示即可自主應(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 研究的焦點(diǎn)。數(shù)學(xué)奧林匹克競賽是世界上最著名的定理證明競賽,，其歷史可以追溯到 1959 年,，在發(fā)現(xiàn)卓越人才方面有著重要作用。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

此外,，AI 也可以被用來構(gòu)建數(shù)學(xué)知識圖譜，有助于將數(shù)學(xué)概念之間的關(guān)系建模成圖結(jié)構(gòu),。這種圖譜可以用于改進(jìn)定理的推理和證明,，使得系統(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