2024年1月17日，DeepMind團(tuán)隊(duì)在《自然》期刊上發(fā)表了一篇名為《無需人類示例即可解決奧數(shù)幾何問題》（Solving olympiad geometry without human demonstrations）的文章。
該篇文章介紹了DeepMind團(tuán)隊(duì)最新的人工智能系統(tǒng)AlphaGeometry。正如論文標(biāo)題所說的，AlphaGeometry可以自行求解國際奧數(shù)難度的平面幾何問題。據(jù)論文中所說，在對30道奧數(shù)幾何題的基準(zhǔn)測試中，AlphaGeometry在標(biāo)準(zhǔn)奧數(shù)時(shí)限內(nèi)解決了25道。相比之下，之前最先進(jìn)的系統(tǒng)解決了其中10個(gè)幾何問題。與之對應(yīng)的，人類金牌得主平均解決了25.9個(gè)問題，銀牌得主平均解決了22.9個(gè)問題，而銅牌得主平均解決了19.3個(gè)問題。
一個(gè)男孩在寫滿數(shù)學(xué)公式的黑板前。視覺中國|圖
這是繼2016年3月和2017年5月，同樣由DeepMind團(tuán)隊(duì)研發(fā)的AlphaGo，在圍棋上接連戰(zhàn)勝李世石和柯潔之后，人工智能系統(tǒng)再一次在純智力競賽領(lǐng)域，達(dá)到人類最頂點(diǎn)選手的水平。也是繼2022年ChatGPT引發(fā)的新一輪大型語言模型類人工智能系統(tǒng)熱潮以來，人工智能系統(tǒng)在求解數(shù)學(xué)問題領(lǐng)域取得的最驚人的成功。
平面幾何的特殊性
與2023年加州理工、英偉達(dá)、MIT等機(jī)構(gòu)的學(xué)者共同撰寫的論文中聲稱的，面向所有數(shù)學(xué)問題的人工智能系統(tǒng)Leandojo不同，這次DeepMind發(fā)布的人工智能系統(tǒng)，是專門為了解決數(shù)學(xué)中的平面幾何問題而特化的。這一點(diǎn)，從AlphaGeometry的名字，阿爾法幾何就能看出來。這是因?yàn)�，在所有的�?shù)學(xué)分支當(dāng)中，平面幾何是極為特殊的。
現(xiàn)代數(shù)學(xué)的一大特征就是公理化。所謂公理化數(shù)學(xué)，首先要約定幾條“不可辯駁”的公理，或者說公設(shè)。然后由此作為基礎(chǔ)，通過邏輯和數(shù)學(xué)的推理過程，來推演引理、定理和推論，從而推演出整個(gè)數(shù)學(xué)體系。只要承認(rèn)公理，那么所有的推導(dǎo)結(jié)果必然自動為真。在過去的一百余年時(shí)間里，數(shù)學(xué)家們逐步完成了各個(gè)數(shù)學(xué)分支的公理化。例如，概率論的公理化就是在二十世紀(jì)三十年代由蘇聯(lián)數(shù)學(xué)家柯爾莫哥洛夫完成的。
平面幾何的公理化則發(fā)生在兩千多年前的古希臘。早在公元前300多年，歐幾里得就在《幾何原本》中給出了平面幾何的五條公理，并以此為基礎(chǔ)，嚴(yán)格證明了數(shù)十條平面幾何的定理。正因?yàn)榇�，平面幾何也被稱為歐幾里得幾何。
極早地完成公理化，使得歐幾里得幾何在古希臘時(shí)期就獲得了巨大的進(jìn)展。而當(dāng)一個(gè)數(shù)學(xué)分支的理論框架搭建完畢，能夠被解決的問題都被解決之后，對于數(shù)學(xué)家們來說，這個(gè)分支也就失去了繼續(xù)被研究的價(jià)值。因此，過早地發(fā)展成熟，也使得歐幾里得幾何成為了第一個(gè)“死掉”的數(shù)學(xué)分支。
但是，就像死掉的拉丁語因?yàn)椴辉僮兓�，而成為生物學(xué)中物種命名的唯一指定語言一樣，死掉的歐幾里得幾何，也在數(shù)學(xué)的其他方面，發(fā)揮了深遠(yuǎn)而長久的作用。
因?yàn)闅W幾里得幾何直觀易懂的五條公理體系，和清晰簡明的命題推理過程，使得歐幾里得幾何成為了學(xué)習(xí)數(shù)學(xué)公理和證明方式的最佳模板。正因?yàn)榇�，歐幾里得幾何一直都是義務(wù)教育階段初中數(shù)學(xué)課程當(dāng)中非常重要的一部分。
另外一方面，同樣因?yàn)闅W幾里得幾何清晰的推理過程，以及相關(guān)的內(nèi)容在很早就有了非常透徹的研究，這也就使得歐幾里得幾何成為了數(shù)學(xué)家們的一塊極佳的“試驗(yàn)田”。在數(shù)學(xué)史上，很多數(shù)學(xué)理論、工具和觀念的新發(fā)展，都會先在歐幾里得幾何上進(jìn)行實(shí)驗(yàn)和推演。
代數(shù)化、坐標(biāo)化、符號化與機(jī)械化
在歷史上，歐幾里得幾何第一次完全的“改頭換面”來自于笛卡爾。通過引入坐標(biāo)系以及線段的運(yùn)算概念，笛卡爾將平面上的點(diǎn)對應(yīng)于一個(gè)有序的實(shí)數(shù)對，而直線、圓之類的幾何圖形，則可以由一個(gè)特定的代數(shù)關(guān)系式來表示。在他的著作《幾何》中，笛卡爾向世人證明，幾何問題可以歸結(jié)成代數(shù)問題。更進(jìn)一步地，可以通過代數(shù)運(yùn)算來發(fā)現(xiàn)、證明幾何性質(zhì)。由此，笛卡爾成功地將當(dāng)時(shí)完全分開的代數(shù)和幾何學(xué)整合，創(chuàng)立了后來被叫做解析幾何的數(shù)學(xué)分支。
一百多年前，希爾伯特發(fā)起的“形式主義綱領(lǐng)”，同樣始于歐幾里得幾何。
希爾伯特想要建立的形式化的數(shù)學(xué)公理體系應(yīng)該滿足三個(gè)條件。即：完備性：可以發(fā)現(xiàn)所有數(shù)學(xué)真命題；自洽性：數(shù)學(xué)內(nèi)部不存在矛盾；可決定性：能夠判斷每一個(gè)數(shù)學(xué)命題的真?zhèn)巍?/p>
按照形式主義的要求，首先應(yīng)當(dāng)有一個(gè)只有有限個(gè)符號的符號表，用這些符號來代替討論數(shù)學(xué)問題的自然語言。用這些符號，就可以像用字母拼寫單詞一樣地去“拼寫”出有意義的命題公式，即：“合式公式”。在指定了相應(yīng)的命題作為公理之后，數(shù)學(xué)中邏輯推理的過程就可以用符號推演代替語言，形式地表達(dá)為符號串構(gòu)成的“單詞”間的對比。由此，數(shù)學(xué)推理的過程就完全變成了“形式化”的符號操作了。
在希爾伯特這樣的形式主義數(shù)學(xué)家看來，所有已經(jīng)發(fā)現(xiàn)和尚未發(fā)現(xiàn)的數(shù)學(xué)定理，都可以寫成這樣或長或短的一串符號。
雖然后來哥德爾不完備定理證明了，對于整個(gè)數(shù)學(xué)體系而言，希爾伯特的這一宏偉圖景是無法實(shí)現(xiàn)的。但是僅限于歐幾里得幾何這一數(shù)學(xué)分支的話，希爾伯特的形式化公理體系是完全成立的。這是因?yàn)闅W幾里得幾何公理體系不包含初等數(shù)論，這一哥德爾不完備定理的成立條件，因而歐幾里得幾何公理體系是完備的。
被希爾伯特形式化之后的歐幾里得幾何，則被稱為希爾伯特幾何。
上世紀(jì)七十年代，吳文俊用這種代數(shù)化和符號化的方法，將歐幾里得幾何與計(jì)算機(jī)科學(xué)相結(jié)合，開創(chuàng)了機(jī)器幾何定理證明的方向，推動了數(shù)學(xué)機(jī)械化自動證明的發(fā)展。這套被數(shù)學(xué)界稱為“吳方法”的機(jī)械化自動證明，用復(fù)雜的形式、符號計(jì)算推演來代替抽象的數(shù)學(xué)推理，從而用計(jì)算機(jī)來輔助數(shù)學(xué)家去發(fā)現(xiàn)自然結(jié)構(gòu)、獲取數(shù)學(xué)真理。
基于吳方法的自動幾何定理證明，首先需要將幾何問題代數(shù)化，將命題中給定的幾何條件和幾何結(jié)論翻譯成多項(xiàng)式方程，然后用特定的計(jì)算機(jī)算法去計(jì)算這些多項(xiàng)式，最終判定幾何命題是否成立。
因?yàn)闅W幾里得幾何是完備的，所有歐幾里得幾何中的命題，都可以用符號化的形式語言，在有限的步驟內(nèi)證明或者證偽。因此，理論上來說，吳文俊發(fā)明的吳方法，完全可以證明所有歐幾里得幾何的定理。
這里所謂的“理論上”，就像是理論上來說，圍棋按照規(guī)則只有有限多種下法，因此可以通過窮盡所有的步驟，來找到必勝策略一樣。在實(shí)際操作中，因?yàn)樗懔蜁r(shí)間的限制，吳方法也只能解決某些幾何問題。
盡管如此，在近幾年的人工智能熱潮之前，吳方法，及其相關(guān)改進(jìn)版本，仍然是機(jī)器證明歐幾里得幾何命題最為行之有效的方法。本文開頭提到的，用來和AlphaGeometry比較的，“解決了其中10個(gè)幾何問題”的“之前最先進(jìn)的系統(tǒng)”，就是吳方法。
AlphaGeometry做了什么
AlphaGeometry相較于“之前最先進(jìn)的系統(tǒng)”的巨大提升，代表了DeepMind之前包括AlphaGo在內(nèi)的技術(shù)積累，與當(dāng)下大型語言模型結(jié)合之后，在歐幾里得幾何這個(gè)特定的數(shù)學(xué)分支下，所展現(xiàn)出的驚人效果。
AlphaGeometry是個(gè)神經(jīng)符號系統(tǒng)，主要包括一個(gè)神經(jīng)語言模型（大語言模型）和一個(gè)符號演繹引擎。
在這兩部分當(dāng)中，大型語言模型擅長識別數(shù)據(jù)中的一般模式和關(guān)系，因此它們可以快速預(yù)測可能有用的結(jié)構(gòu)。但通常情況下，大型語言模型缺乏嚴(yán)格推理或解釋的能力。這也是之前包括ChatGPT和GPT-4等大型語言模型在數(shù)學(xué)能力方面表現(xiàn)難如人意的原因。
在AlphaGeometry這里，大型語言模型的這一弱點(diǎn)被另外一部分，即符號演繹引擎所解決。符號演繹引擎基于形式邏輯，并使用明確的規(guī)則來得出結(jié)論。這兩部分協(xié)同工作，類似于卡尼曼 《思考，快和慢》一書中提到的系統(tǒng)1和系統(tǒng)2的概念，系統(tǒng)1提供快速、“直觀”的想法，而系統(tǒng)2則提供“更深思熟慮、更理性的決策”的想法。
在大型語言模型的訓(xùn)練上，DeepMind為AlphaGeometry搭建了包含1.51億參數(shù)的模型。在“命題、結(jié)論、證明”上進(jìn)行了預(yù)訓(xùn)練，合成了5億個(gè)幾何證明，其中有900萬個(gè)帶輔助線的題目。
通過這種訓(xùn)練，DeepMind成功地讓AlphaGeometry的大型語言模型學(xué)會了幾何證明中最為重要的技巧：添加和使用輔助線。
AlphaGeometry能夠?qū)γ恳粋�(gè)幾何圖形，窮舉該圖形能夠得到的命題。并且能夠反過來回溯每個(gè)命題所包含的幾何圖形的集合。在解題過程中，AlphaGeometry會搜尋題目條件中的幾何圖形所能夠得到的命題，以及包含題目所要證明的結(jié)論命題的幾何圖形的集合。通過比對這兩個(gè)集合中集合對象的差異，找到輔助線的位置。
這是數(shù)學(xué)的未來嗎
在驚異于AlphaGeometry的出色表現(xiàn)之余，我們不由得會想要知道，AlphaGeometry的這種模式，是數(shù)學(xué)發(fā)展的未來么？或者說，在可以預(yù)見的時(shí)間內(nèi)，人工智能能否獨(dú)立進(jìn)行數(shù)學(xué)研究，并且做出有價(jià)值的結(jié)果？
雖然AlphaGeometry體現(xiàn)了現(xiàn)階段大型語言模型“足夠好的數(shù)據(jù)就意味著足夠好的智能”，這一用大量參數(shù)、大樣本集解決問題的暴力美學(xué)的特征。但是，AlphaGeometry本身極度依賴歐幾里得幾何本身的特點(diǎn)。而正如前文所說，歐幾里得幾何，在數(shù)學(xué)當(dāng)中是極為特殊的一個(gè)分支。AlphaGeometry的這一做法能否推廣到其他數(shù)學(xué)分支，還是一個(gè)未知數(shù)。
而且，正如楊立昆等人多次提到的，現(xiàn)階段大型語言模型對于數(shù)據(jù)的利用率相當(dāng)?shù)拖隆渭優(yōu)榱饲蠼鈳缀螁栴}，AlphaGeometry的參數(shù)和訓(xùn)練集，就來到了如此量級。因此，即使AlphaGeometry的做法能夠以某種方式擴(kuò)展到一般的數(shù)學(xué)問題上，面對各種類型的數(shù)學(xué)問題，這樣的人工智能系統(tǒng)需要的參數(shù)和訓(xùn)練集數(shù)量，在現(xiàn)階段的實(shí)際操作層面也很可能是無法實(shí)現(xiàn)的。
盡管如此，AlphaGeometry所展示的，人工智能不斷增長的邏輯推理能力以及發(fā)現(xiàn)和驗(yàn)證新知識的能力，仍然足夠讓人印象深刻。
正如AlphaGeometry的作者之一在社交媒體上所說的：“目前組合數(shù)學(xué)的形式化還處于初期，為不同領(lǐng)域構(gòu)建強(qiáng)大的符號引擎需要深入的領(lǐng)域?qū)I(yè)知識。我們考慮將該框架應(yīng)用于更廣泛的范圍，作為未來的工作，并期待進(jìn)一步的創(chuàng)新來應(yīng)對這些挑戰(zhàn)。”
就文章所展示的內(nèi)容來看，AlphaGeometry的思路很直接，但是其中各種細(xì)節(jié)上的技術(shù)難點(diǎn)，和解決這些難點(diǎn)的做法，都非常得不平凡。這充分體現(xiàn)了作者們極強(qiáng)的能力和毅力。因此，現(xiàn)在就對AlphaGeometry下一個(gè)定論顯然還為時(shí)尚早，但是完成AlphaGeometry這項(xiàng)工作所呈現(xiàn)出的一切，讓我們有理由期待作者未來的工作。
南方周末特約撰稿 左力
責(zé)編 朱力遠(yuǎn)
