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

圖片來源：由無界 AI生成

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

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

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

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

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

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

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

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

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

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

缺乏足夠的樣本數(shù)據(jù),，特別是包含人類專業(yè)數(shù)學(xué)家的解答過程，使得機(jī)器學(xué)習(xí)模型難以學(xué)習(xí)和理解解題方法。因此,，目前的幾何方法仍主要依賴于符號(hào)方法和人工設(shè)計(jì)的硬編碼搜索啟發(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)符號(hào)演繹引擎（能夠搜索難題中的大量分支點(diǎn)）方面具有獨(dú)特的優(yōu)勢(shì),。神經(jīng)模型的引入使得 AlphaGeometry 在處理具有挑戰(zhàn)性的問題時(shí)能夠做出更為精準(zhǔn)的推理。這種綜合運(yùn)用符號(hào)演繹引擎和神經(jīng)語言模型的方法是該研究的重要?jiǎng)?chuàng)新之一,。

圖｜AlphaGeometry 概述以及它如何解決簡(jiǎn)單問題和IMO2015問題3。頂行顯示 AlphaGeometry 如何解決簡(jiǎn)單問題,。a）簡(jiǎn)單的例子及其圖表,。b）模型通過運(yùn)行符號(hào)推演引擎來啟動(dòng)證明搜索。引擎從定理前提中詳盡地推導(dǎo)出新的陳述,，直到定理被證明或新的陳述被窮舉為止,。c）由于符號(hào)引擎未能找到證明，語言模型構(gòu)造一個(gè)輔助點(diǎn),，在符號(hào)引擎重試之前增長證明狀態(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 共線”。底行顯示了 AlphaGeometry 如何解決 IMO 2015 Problem 3 (IMO 2015 P3),。e）IMO 2015 P3 問題陳述和圖表,。f IMO 2015 P3的解有3個(gè)輔助點(diǎn)。（來源：該論文）? ?

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

據(jù)論文描述,，AlphaGeometry 主要專注于解決奧林匹克級(jí)別的幾何問題，應(yīng)用范圍相對(duì)狹窄,。這限制了該方法在其他數(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í)場(chǎng)景中的性能可能會(huì)受到數(shù)據(jù)不足的影響。

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

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

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

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

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

對(duì)于創(chuàng)造性思維的開發(fā),，AI 也有一席之地。一些研究采用生成式模型,，比如生成對(duì)抗網(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