（視覺中國/圖）
隨著GPT熱潮的不斷發(fā)展，包括ChatGPT在內(nèi)的大型語言模型（Large Language Model；LLM）開始逐漸進(jìn)入各種原來被認(rèn)為是人類智力活動(dòng)專屬的領(lǐng)域當(dāng)中。例如，菲爾茲獎(jiǎng)得主、華裔數(shù)學(xué)家陶哲軒就在一篇博客中宣稱，他已經(jīng)開始使用GPT-4來協(xié)助自己的工作。而2023年7月27日發(fā)布在預(yù)印本網(wǎng)站（arXiv）上的一篇由加州理工、英偉達(dá)、MIT等機(jī)構(gòu)的學(xué)者共同撰寫的論文聲稱，他們構(gòu)建了一個(gè)基于開源LLM的定理證明器。似乎一夜之間，AI就攻陷了數(shù)學(xué)，這個(gè)人類智慧最純粹的領(lǐng)域之一。
實(shí)際上，追本溯源起來，數(shù)學(xué)家尋找自動(dòng)化證明的過程，已經(jīng)有一百多年的歷史了。甚至計(jì)算機(jī)的誕生與發(fā)展，也與這一探尋過程有著密不可分的關(guān)系。
數(shù)學(xué)基礎(chǔ)與哥德爾不完備定理
在1900年4月27日英國皇家學(xué)會(huì)的一次演講上，物理學(xué)家開爾文男爵發(fā)表了著名的物理學(xué)“兩朵烏云”的演講。后來的事情大家都知道了，兩朵烏云掀起了狂風(fēng)暴雨，從中誕生了二十世紀(jì)現(xiàn)代物理學(xué)的兩大支柱相對(duì)論和量子力學(xué)。
就在開爾文男爵發(fā)表演講的同一年，數(shù)學(xué)家大衛(wèi)希爾伯特在巴黎舉行的第二屆國際數(shù)學(xué)家大會(huì)上，作了題為《數(shù)學(xué)問題》的演講，提出了二十三道他認(rèn)為最重要的數(shù)學(xué)問題。這些問題隨后被稱作“希爾伯特問題”或者“希爾伯特的23個(gè)問題”。針對(duì)這些問題的研究，在很大程度上促進(jìn)了二十世紀(jì)數(shù)學(xué)的發(fā)展。
在希爾伯特提出的這23個(gè)問題當(dāng)中，就有諸如“連續(xù)統(tǒng)假設(shè)”“算術(shù)公理之相容性”“公理化物理”這樣涉及數(shù)學(xué)以及科學(xué)基礎(chǔ)的問題。這些問題的提出，來源于希爾伯特的雄心壯志：他希望能夠建立起一套統(tǒng)一的數(shù)學(xué)公理化體系。不止于此，在公理化體系之上，他還有一個(gè)更加宏大的設(shè)想，那就是所謂的“希爾伯特形式主義綱領(lǐng)”。
按照希爾伯特的設(shè)想，他想要建立的形式化的數(shù)學(xué)公理體系應(yīng)該滿足三個(gè)條件。即：完備性：可以發(fā)現(xiàn)所有數(shù)學(xué)真命題；自洽性：數(shù)學(xué)內(nèi)部不存在矛盾；可決定性：能夠判斷每一個(gè)數(shù)學(xué)命題的真?zhèn)巍?/p>
作為數(shù)學(xué)家的希爾伯特，他所關(guān)心的是“數(shù)學(xué)大廈”本身如何建造。至于這座大廈的地基建在哪里，在希爾伯特看來是一件無需考慮的事情。但是，就是這件“無需考慮”的事情，卻出現(xiàn)了意想不到的問題。
1901年，年僅29歲的英國哲學(xué)家羅素發(fā)現(xiàn)了著名的羅素悖論。這一悖論，最簡單的表述形式就是所謂的“理發(fā)師悖論”。即：小城里的理發(fā)師放出豪言：他要為城里人刮胡子，而且一定只要為城里所有“不為自己刮胡子的人”刮胡子。那么，理發(fā)師該為自己刮胡子嗎？
這一悖論說明了，當(dāng)時(shí)作為“數(shù)學(xué)大廈”的基礎(chǔ)的樸素集合論，在邏輯上是不嚴(yán)謹(jǐn)?shù)�。這就是所謂的“第三次數(shù)學(xué)危機(jī)”。為此，數(shù)學(xué)家們最終將樸素集合論發(fā)展成了公理化集合論。更為重要的是，數(shù)學(xué)家們認(rèn)識(shí)到，不僅數(shù)學(xué)本身需要公理化，數(shù)學(xué)基礎(chǔ)更需要公理化。
為此，羅素和他在劍橋大學(xué)三一學(xué)院時(shí)的老師、著名哲學(xué)家懷特海德，花費(fèi)了十年時(shí)間，完成了三卷本的巨著《數(shù)學(xué)原理》。
羅素的做法，屬于對(duì)數(shù)學(xué)基礎(chǔ)進(jìn)行探究的另外一個(gè)學(xué)派：“邏輯主義”。這部三卷本的《數(shù)學(xué)原理》，正是邏輯主義發(fā)展的高峰。在《數(shù)學(xué)原理》中， 數(shù)學(xué)大廈的一部分被從邏輯出發(fā)直接構(gòu)筑了出來。
這一宏大的目標(biāo)的代價(jià)之一就是推理的極度曲折和冗長。比方說，“1”這個(gè)最簡單的數(shù)字在《數(shù)學(xué)原理》中直到第363頁才被定義；1+1=2這個(gè)最簡單的小學(xué)算術(shù)題直到第379頁才有結(jié)果。
《數(shù)學(xué)原理》滿滿兩大箱的手稿，被羅素用馬車運(yùn)到了劍橋大學(xué)出版社。而出版社對(duì)這部巨著的利潤估計(jì)為：出版這部書會(huì)讓出版社虧損600英鎊。1910年的600英鎊，約等于現(xiàn)在的60萬元人民幣。幸好，劍橋大學(xué)出版社并不是純粹的盈利性出版社，他們?cè)敢鉃檫@部學(xué)術(shù)著作承擔(dān)300英鎊的虧損。剩下的300英鎊中，英國皇家學(xué)會(huì)資助了200英鎊。最后這100英鎊只得由羅素和懷特海德個(gè)人承擔(dān)。
但是，就在《數(shù)學(xué)原理》出版之后不久的1931年，年僅25歲的數(shù)學(xué)家哥德爾證明并發(fā)表了兩條日后被稱作“哥德爾不完備定理”的數(shù)學(xué)定理。這兩條定理表明，包含算術(shù)公理的數(shù)學(xué)體系是不完備的，同時(shí)也是不自洽的。
就像開爾文男爵口中的“兩朵烏云”徹底改變了物理學(xué)大廈的形態(tài)一樣。哥德爾不完備定理也宣告了，希爾伯特和羅素所希望建立的數(shù)學(xué)大廈是永遠(yuǎn)不可能竣工的。
前AI時(shí)代的機(jī)器證明
雖然希爾伯特和羅素的宏偉計(jì)劃被哥德爾證明是無法實(shí)現(xiàn)的。但是他們的工作，對(duì)于數(shù)學(xué)和計(jì)算機(jī)的發(fā)展，卻起到了難以估量的作用。
一方面，這些工作，使得現(xiàn)代數(shù)學(xué)有了一個(gè)相對(duì)堅(jiān)實(shí)的基矗另外一方面，這些工作中對(duì)公理化和形式化數(shù)學(xué)的探究，也徹底改變了自古以來數(shù)學(xué)家們描述數(shù)學(xué)的語言和研究數(shù)學(xué)的方式。這一變化最顯著的例子就是，現(xiàn)在幾乎所有的數(shù)學(xué)專著，都會(huì)選擇幾乎一模一樣的開篇方式。即在開頭部分，用集合論之類的語言，給出書中討論的數(shù)學(xué)對(duì)象的嚴(yán)格定義。
而對(duì)希爾伯特公理化三條準(zhǔn)則的研究，也催生出現(xiàn)代計(jì)算機(jī)的理論基矗
哥德爾不完備定理宣告了希爾伯特公理體系中的完備性和自洽性是不成立的。而在同一時(shí)期，對(duì)于希爾伯特公理體系可決定性的研究也在進(jìn)行。就在哥德爾發(fā)表不完備定理幾年后，波蘭裔數(shù)學(xué)家阿爾弗雷德塔斯基和英國數(shù)學(xué)家阿蘭圖靈各自獨(dú)立地證明了，希爾伯特公理體系中的可決定性，也是不成立的。
在證明的過程中，圖靈提出了“圖靈機(jī)”的概念。這一概念，就是現(xiàn)代計(jì)算機(jī)的理論模型。從本質(zhì)上講，包括算盤、機(jī)械計(jì)算機(jī)、電子計(jì)算機(jī)在內(nèi)的所有計(jì)算“機(jī)”，都可以看做是一種具體的圖靈機(jī)。另外，圖靈還證明了，希爾伯特公理體系中的可決定性，和圖靈機(jī)的停機(jī)問題是等價(jià)的。
圖靈的這些研究，成為日后計(jì)算機(jī)發(fā)展的理論基矗因?yàn)樵谌斯ぶ悄茴I(lǐng)域開創(chuàng)性的奠基作用，圖靈被稱為“人工智能之父”。
二戰(zhàn)之后，隨著第一代真空管計(jì)算機(jī)在美國的發(fā)展，數(shù)學(xué)家們也開始嘗試在真正的“機(jī)器”上去實(shí)現(xiàn)那些已有的形式化的數(shù)學(xué)結(jié)論。為了做到這一點(diǎn)，首先需要?jiǎng)?chuàng)造出“機(jī)器”能夠“聽懂”，而且能夠用來進(jìn)行邏輯推理的語言。這時(shí)，希爾伯特和羅素所使用的那一套形式化的邏輯符號(hào)，也就成為之后發(fā)展出的“機(jī)器”所使用的各種“數(shù)學(xué)語言”的基矗
這一時(shí)期的主要結(jié)果，都是在普林斯頓高等研究院重達(dá)2.3噸的真空管計(jì)算機(jī)“JOHNNIAC”上完成的。1954年，馬丁戴維斯開始嘗試為JOHNNIAC編寫包含自然數(shù)和加法的算法程序。他所取得的最大成果就是，讓JOHNNIAC證明了“兩個(gè)偶數(shù)的和還是偶數(shù)”。
在1956年，同樣是在JOHNNIAC上，艾倫紐維爾、赫伯特西蒙和JC肖，用他們開發(fā)的程序“邏輯證明機(jī)”，證明了羅素的《數(shù)學(xué)基捶中前52條定理中的38條。對(duì)于某些定理，“邏輯證明機(jī)”甚至找到了新的、更優(yōu)雅的證明。
自此，自動(dòng)化證明（Automated Theorem Proving，ATP）開始逐漸成為一個(gè)正式的研究方向。而“邏輯證明機(jī)”也被很多人認(rèn)為是“第一個(gè)人工智能程序”。盡管在當(dāng)時(shí)，人工智能這一研究領(lǐng)域還不存在。
在隨后的幾十年間，自動(dòng)化證明有了長足的發(fā)展。但是，想要真正地讓自動(dòng)化證明產(chǎn)出數(shù)學(xué)上有價(jià)值的結(jié)果，還是一件遙遙無期的事情。因?yàn)樽詣?dòng)化證明，面臨一個(gè)魚和熊掌不可兼得的兩難局面。能夠用來生成有價(jià)值的數(shù)學(xué)結(jié)論的證明器通�；诒容^強(qiáng)的邏輯系統(tǒng)，而在這類邏輯系統(tǒng)上實(shí)現(xiàn)全自動(dòng)推理還是相當(dāng)困難的。與之相對(duì)的，能夠?qū)崿F(xiàn)強(qiáng)自動(dòng)化的邏輯系統(tǒng)，如一階邏輯甚至布爾邏輯，卻無法產(chǎn)出真正有價(jià)值的數(shù)學(xué)結(jié)論。
面對(duì)這一局面，有人工引導(dǎo)的、強(qiáng)邏輯系統(tǒng)下的證明機(jī)器成為了發(fā)展的主流方向。這也就是所謂的交互式證明（Interactive Theorem Proving，ITP）。
利用交互式證明得出的最早也是最為知名的結(jié)果，就是四色定理的證明。
所謂四色定理，用通俗的話來說就是：“每個(gè)無外飛地的地圖都可以用不多于四種顏色來染色，而且不會(huì)有兩個(gè)鄰接的區(qū)域顏色相同。”這一問題最早是由南非數(shù)學(xué)家法蘭西斯古德里在1852年提出的，被稱為“四色問題”或“四色猜想”。在此后的一百多年時(shí)間里，包括閔可夫斯基在內(nèi)的知名大數(shù)學(xué)家都研究過這個(gè)問題，但是一直沒有得到完整的證明。
關(guān)于四色定理的證明思路，其實(shí)很早就已經(jīng)明確了。這是因?yàn)�，地圖上相鄰國家的接壤方式，可以分為有限多種情況。這些互不相同的情況，被稱為構(gòu)型。所以，只需要逐一驗(yàn)證所有的構(gòu)型都符合四色定理的情況，就證明了四色定理。但是這一目標(biāo)的工作量，遠(yuǎn)遠(yuǎn)超過了人類能夠完成的極限。直到1976年，數(shù)學(xué)家凱尼斯阿佩爾和沃夫?qū)�，在美國伊利諾伊大學(xué)的IBM 360電腦上，花費(fèi)了1200小時(shí)的時(shí)間，驗(yàn)證了所有的1936種構(gòu)型，從而證明了四色定理。
自那之后，包括雙泡猜想、羅賓斯猜想在內(nèi)的數(shù)十個(gè)數(shù)學(xué)問題，以與四色定理類似的方式得到了解決或者取得了重要的進(jìn)展。
數(shù)學(xué)家們想要什么？
雖然取得了這些成果，但是交互式的機(jī)器證明仍然沒有被數(shù)學(xué)界廣泛采用。甚至?xí)r至今日，還有數(shù)學(xué)家在嘗試不使用計(jì)算機(jī)，純靠人力去證明包括四色定理在內(nèi)的，這些已經(jīng)通過機(jī)器證明得到解決的數(shù)學(xué)問題。
這一方面是因?yàn)�，交互式證明能夠解決的問題是有局限性的。而且，交互式證明作為一門獨(dú)立的研究方向，是有著不低門檻的。它需要掌握相應(yīng)的人機(jī)交互語言。另外，交互式證明主流使用的，以類型論為基礎(chǔ)的邏輯體系，也和數(shù)學(xué)家們習(xí)慣的，以集合論為基礎(chǔ)的數(shù)學(xué)體系并不相同。這就導(dǎo)致了如果數(shù)學(xué)家們想要親自使用交互式證明，就先要花費(fèi)不小的學(xué)習(xí)成本來學(xué)習(xí)。
更為重要的原因，則是因?yàn)閿?shù)學(xué)這門學(xué)科本身的價(jià)值觀。
提起數(shù)學(xué)，我們的第一反應(yīng)大概率會(huì)是“嚴(yán)格”。在數(shù)學(xué)里，對(duì)就是對(duì)，錯(cuò)就是錯(cuò)。在自然數(shù)當(dāng)中1+1永遠(yuǎn)都只會(huì)等于2。數(shù)學(xué)考試的時(shí)候，哪怕最后結(jié)果算對(duì)了，只要中間步驟有錯(cuò)，也會(huì)被老師毫不留情地扣分。
不可否認(rèn)的是，嚴(yán)格性的確是數(shù)學(xué)，特別是數(shù)學(xué)證明中極為重要的價(jià)值。但是，只要稍微了解一點(diǎn)兒數(shù)學(xué)史，以及數(shù)學(xué)家們的具體工作，我們就難免會(huì)產(chǎn)生這樣的疑問：嚴(yán)格性是不是數(shù)學(xué)最重要的價(jià)值？
微積分的嚴(yán)格化是由魏爾斯特拉斯完成的。那時(shí)距離牛頓和萊布尼茨提出微積分已經(jīng)過去了快200年。但是這并不影響牛頓和萊布尼茲作為微積分的提出者，被認(rèn)為是歷史上最偉大的數(shù)學(xué)家之一。也不影響這200年間，數(shù)學(xué)家們用著不嚴(yán)格的微積分工具，發(fā)展出了極為精彩的數(shù)學(xué)理論和定理。
歐拉的很多極為精彩的工作，以現(xiàn)在的標(biāo)準(zhǔn)來看都是完全不嚴(yán)格的。時(shí)至今日，歐拉得出的那個(gè)全體自然數(shù)的和等于-1/12的結(jié)論，還在被各種營銷號(hào)拿來傳播。但是這也絲毫不影響歐拉在數(shù)學(xué)上的貢獻(xiàn)。
黎曼的很多工作是用到的數(shù)學(xué)理論，例如黎曼映照定理的證明中用到的，橢圓方程的正則性，直到20世紀(jì)很晚的時(shí)候才逐步建立起來。
直到現(xiàn)在，數(shù)學(xué)中仍然有很多這樣的例子。
對(duì)現(xiàn)代幾何學(xué)的多個(gè)領(lǐng)域做出了革命性貢獻(xiàn)的俄裔法國數(shù)學(xué)家格羅莫夫，他的很多論文，按照一般數(shù)學(xué)工作者的標(biāo)準(zhǔn)來看，已經(jīng)遠(yuǎn)遠(yuǎn)超出了“不嚴(yán)格”的程度。為了理解格羅莫夫的一篇短短十?dāng)?shù)頁的文章中的內(nèi)容，往往就需要很多數(shù)學(xué)家去寫一系列的文章。
類似的情況還有物理學(xué)家出身，卻拿下來數(shù)學(xué)界最高獎(jiǎng)菲爾茲獎(jiǎng)的愛德華威騰。他的很多工作，都來自于物理學(xué)的直覺，而不是數(shù)學(xué)的嚴(yán)格。
一個(gè)數(shù)學(xué)結(jié)果無法被嚴(yán)格寫下來，原因可能是多種多樣的。一個(gè)是數(shù)學(xué)還沒發(fā)展到可以用精煉的語言寫下嚴(yán)格的論斷的時(shí)候。牛頓和萊布尼茨、歐拉都是這種情況。在他們的時(shí)代，“無窮”還是一個(gè)相當(dāng)模糊的概念，無論是數(shù)學(xué)上還是哲學(xué)上都沒有辦法準(zhǔn)確描述什么是“無窮”。在十九世紀(jì)后期這個(gè)問題開始被解決之后，人們就能很好地嚴(yán)格化他們的論述。
另一個(gè)原因則是出于效率的考慮。即使不談這些大數(shù)學(xué)家，作為普通的數(shù)學(xué)工作者，以及數(shù)學(xué)專業(yè)的學(xué)生，在寫論文的時(shí)候，也不會(huì)事無巨細(xì)地像機(jī)器證明那樣寫出所有的細(xì)節(jié)。很多繁瑣的內(nèi)容，都被簡簡單單的“顯然”兩個(gè)字概括了。
更為主要的原因，則是對(duì)于數(shù)學(xué)理解的考慮。很多數(shù)學(xué)上的想法，未必是嚴(yán)格的，但很可能是很精彩的。無論是黎曼還是格羅莫夫和威騰，他們寫下的“證明”都是充滿內(nèi)涵和啟發(fā)性的。相較于一個(gè)嚴(yán)格的、沒有錯(cuò)誤的證明，這些“不嚴(yán)格”工作能夠讓我們對(duì)數(shù)學(xué)的理解更加深入，從而發(fā)現(xiàn)更多未知的數(shù)學(xué)。就像陳省身所說的：“有數(shù)學(xué)經(jīng)驗(yàn)和遠(yuǎn)見的人，能在大海航行下，達(dá)到重要的新的領(lǐng)域。”
因此，雖然所有的數(shù)學(xué)結(jié)果，在最后都必須要徹底地嚴(yán)格化。但是在具體的過程中，嚴(yán)格性很多時(shí)候其實(shí)并不是處在最重要的位置上的。比起一萬個(gè)嚴(yán)格寫下來的形式化的證明，現(xiàn)在數(shù)學(xué)界主流還是更欣賞一個(gè)不嚴(yán)格的但是有深刻內(nèi)涵的“證明”。
AI是解決之道嗎？
那么，現(xiàn)在風(fēng)頭正勁的，以GPT為代表的大型語言模型，能否改變這種局面，讓機(jī)器證明能夠滿足數(shù)學(xué)家們的需求，從而真的變得可用起來呢？
首先，要做到這一點(diǎn)，直接使用諸如GPT這樣的通用型的大型語言模型是不行的。
實(shí)際上，根據(jù)微軟研究院對(duì)GPT-4的測試報(bào)告，數(shù)學(xué)能力，在GPT-4的各項(xiàng)能力當(dāng)中，本身就是一個(gè)相對(duì)的弱項(xiàng)。這很大程度上是因?yàn)椋珿PT的訓(xùn)練和養(yǎng)成，主要是靠互聯(lián)網(wǎng)上的信息。想要通過這樣的方式，獲得相當(dāng)程度的專業(yè)數(shù)學(xué)能力，本身就是不現(xiàn)實(shí)的。而且，專業(yè)數(shù)學(xué)能力的培養(yǎng)，本身也不是GPT所要實(shí)現(xiàn)的目標(biāo)。
那么，如果我們換一個(gè)思路，將大型語言模型，與已有的交互式證明程序相結(jié)合，能不能制造出能夠滿足數(shù)學(xué)家們的需求的定理證明機(jī)呢？
這種想法是有著很強(qiáng)的合理性的。首先，大型語言模型這一工具，可以讓數(shù)學(xué)家們免去學(xué)習(xí)使用交互式證明的過程。他們只需要用自己熟悉的語言將問題“告訴”給大型語言模型，然后讓模型將其“翻譯”給交互式證明程序，完成之后，再將程序給出的形式化的符號(hào)結(jié)果“翻譯”成數(shù)學(xué)家們習(xí)慣的數(shù)學(xué)語言。
另外，更為重要的是，現(xiàn)在的大型語言模型，已經(jīng)展現(xiàn)出了一定的邏輯推理能力。按照AI的學(xué)習(xí)成長速度，再繼續(xù)發(fā)展下去，將來很有可能會(huì)出現(xiàn)，能夠給出在數(shù)學(xué)上做出有深刻內(nèi)涵的啟發(fā)性工作的人工智能。
本文開頭所提到的，由加州理工、英偉達(dá)、MIT等機(jī)構(gòu)的學(xué)者共同撰寫的論文中的工作，就是朝著這個(gè)方向邁出的第一步。
他們以Lean，這個(gè)由微軟研究院的萊昂納多德莫拉最初于2013年發(fā)布的開源交互式證明機(jī)為基礎(chǔ)，推出了首個(gè)基于大型語言模型的開源定理證明機(jī)：LeanDojo。
不同于GPT這樣“大”型語言模型，LeanDojo要小很多。它的核心數(shù)據(jù)集，只有96962個(gè)定理和證明過程。而且，不同于GPT需要在海量的硬件上進(jìn)行長時(shí)間的訓(xùn)練，LeanDojo的訓(xùn)練過程，只需要單張顯卡一周的時(shí)間，就可以訓(xùn)練完成。而根據(jù)論文中的說法，LeanDojo的數(shù)學(xué)能力，相較于GPT-4有著顯著的提升。
這是因?yàn)�，相較于泛用型的GPT，專注于數(shù)學(xué)的LeanDojo，所需要處理的問題要單一得多。而且，形式化數(shù)學(xué)和機(jī)器證明幾十年的發(fā)展積累，也為LeanDojo的訓(xùn)練提供了一個(gè)堅(jiān)實(shí)的基矗
盡管LeanDojo的表現(xiàn)看上去足夠讓人印象深刻，但是這篇論文的作者們卻十分地清醒。他們?cè)谡撐闹袑懙溃哼@項(xiàng)工作，旨在降低這一領(lǐng)域的進(jìn)入門檻，并且為今后的工作提供一個(gè)可以繼續(xù)前進(jìn)的起點(diǎn)。
雖然在現(xiàn)在這個(gè)時(shí)刻，想要讓AI做出數(shù)學(xué)家級(jí)別的工作還遠(yuǎn)遠(yuǎn)不可能。但是，大型語言模型和機(jī)器證明的結(jié)合，至少代表著一種可能性。就像一個(gè)小孩在紙上歪歪扭扭地寫出了“1+1=2”，所有人的反應(yīng)，都是會(huì)微笑著期待這個(gè)小孩將來長大之后會(huì)做出什么。
左力
