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

圖片來(lái)源：由無(wú)界 AI生成

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

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

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

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

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

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

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

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

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

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

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

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

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

無(wú)需人類(lèi)，自主解決復(fù)雜問(wèn)題

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

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

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

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

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

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

此外，雖然 AlphaGeometry 能夠生成人類(lèi)可讀的證明,，但在處理極其復(fù)雜的推理時(shí)，其生成的結(jié)果可能變得難以理解,。這使得人們?cè)谝恍┣闆r下難以追蹤和解釋模型的推理過(guò)程,。

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

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

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

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

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

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

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

論文鏈接：

https://www.nature.com/articles/s41586-023-06747-5