今年6月，陶哲軒曾在博客中預(yù)言，2026年，AI將與搜索和符號(hào)數(shù)學(xué)工具相結(jié)合，成為數(shù)學(xué)研究中值得信賴(lài)的合著者。

這個(gè)預(yù)言，如今已經(jīng)愈發(fā)成真。

就在6月底，加州理工、英偉達(dá)、MIT等機(jī)構(gòu)的學(xué)者，曾構(gòu)建了一個(gè)基于開(kāi)源LLM的定理證明器。

最近，陶哲軒又發(fā)現(xiàn)，在使用Lean進(jìn)行自然數(shù)游戲研究時(shí)，GPT-4竟然也起到一些作用。

在AI的輔助下，他得到了關(guān)于有限多個(gè)實(shí)變量不等式理論的成果，論文很快就會(huì)發(fā)在arXiv上。

圖片

如何用GPT-4研究自然數(shù)游戲

什么是自然數(shù)游戲？

圖片

這個(gè)游戲，神奇地展示了歸納的力量。

如圖所示，我們從藍(lán)色節(jié)點(diǎn)上輸入，而灰色節(jié)點(diǎn)上方的所有結(jié)點(diǎn)都完成時(shí)，灰色節(jié)點(diǎn)將變?yōu)樗{(lán)色。

在這個(gè)過(guò)程中，我們當(dāng)然可以隨時(shí)嘗試任何級(jí)別的節(jié)點(diǎn)，但如果它是灰色的，我們可能就沒(méi)有足夠的知識(shí)來(lái)完成這個(gè)節(jié)點(diǎn)。

引理：對(duì)于所有自然數(shù)x、y和z都有xy+z=xy+z。證明開(kāi)始！

在自然數(shù)游戲中，我們就會(huì)在定理證明器Lean中，得到自己的一個(gè)自然數(shù)版本——mynat。這個(gè)自然數(shù)滿(mǎn)足了數(shù)學(xué)歸納定理，以及其他原理（比如皮亞諾公理）。

圖片

不過(guò)，問(wèn)題在于，目前還沒(méi)有人證明這些關(guān)于自然數(shù)的定理，比如，你可以定義加法，但還沒(méi)有人證明x + y = y + x。

皮亞諾公理

而自然數(shù)游戲，就需要你解決游戲中的關(guān)卡，用Lean定理證明器來(lái)證明數(shù)學(xué)定理。

我們證明了n+0=n，這個(gè)證明被稱(chēng)為add_zero。但并不能證明zero_add，0+n=n。這兩個(gè)定理不是一樣嗎？并非如此！事實(shí)上x(chóng) + y = y + x，這是加法世界的BOSS級(jí)難題。

陶哲軒是出于怎樣的機(jī)緣巧合，開(kāi)始玩自然數(shù)游戲的呢？

原來(lái)，他是在IPAM機(jī)器輔助證明研討會(huì)上看到過(guò)幾次Lean的演示，并且被建議玩一玩自然數(shù)游戲，來(lái)熟悉Lean中用于證明定理的基本語(yǔ)法和策略。

讓陶哲軒感到驚喜的是，這個(gè)游戲越玩越熟悉，因?yàn)樗C明的結(jié)果和自己寫(xiě)的本科實(shí)分教材前幾章的結(jié)果分成相似。

圖片

比如，從皮亞諾公理建立基本的算術(shù)事實(shí)，例如乘法的交換性和結(jié)合性。

另外，自然數(shù)游戲還讓他想起了自己編碼的邏輯游戲。

才玩了三個(gè)小時(shí)，陶哲軒就已經(jīng)到達(dá)了「高級(jí)乘法」世界。他表示，在以后的空閑時(shí)間里他會(huì)繼續(xù)玩這個(gè)游戲。

圖片

高級(jí)乘法世界：證明兩個(gè)非零自然數(shù)的乘積為非零：a≠0 → b≠0 → a*b≠0

當(dāng)然，GPT-4也知道Lean，它可以提供一些有用的回答。

不過(guò)，因?yàn)樽匀粩?shù)游戲中可用的工具集很有限，所以GPT-4對(duì)于這個(gè)游戲沒(méi)有直接的幫助，因?yàn)樗岢龅慕鉀Q方案中涉及的方法，通常還沒(méi)有被納入游戲中。

不過(guò)，當(dāng)他開(kāi)始使用Lean的時(shí)候，GPT-4就變得非常有幫助了。

圖片

隨著關(guān)卡變得越來(lái)越難，GPT的作用開(kāi)始逐漸顯現(xiàn)出來(lái)。

在Z顯而易見(jiàn)是X和Y的結(jié)果的情況下，如果向GPT提問(wèn)——

如果我已經(jīng)知道X和Y，該如何證明Z呢？

這個(gè)過(guò)程就解決了各種微妙的語(yǔ)法問(wèn)題，否則這些問(wèn)題會(huì)十分令人沮喪。

圖片

而且，陶哲軒發(fā)現(xiàn)，自然數(shù)游戲中包含的Lean庫(kù)，似乎比文件中宣稱(chēng)的要多得多。

GitHub Copilot，讓我不安

總之，AI工具輔助研究數(shù)學(xué)的奇跡，一次次讓陶哲軒稱(chēng)贊不已，甚至發(fā)展到了讓他「不安」。

前不久陶哲軒發(fā)現(xiàn)，GitHub Copilot已經(jīng)能夠預(yù)測(cè)到自己文章中數(shù)學(xué)論證的步驟了。

圖片

在10月初，陶哲軒表示，Github Copilot的能力驚艷到他了。

而且他強(qiáng)調(diào)，并不是它的編碼能力，而是它編碼之外的補(bǔ)充其他內(nèi)容的能力，經(jīng)常能讓他喜出望外。

最近，他又稱(chēng)贊到——

我發(fā)現(xiàn)Github Copilot在我最近撰寫(xiě)博客文章的過(guò)程中出奇地有幫助。它能夠正確預(yù)測(cè)該帖子中數(shù)學(xué)論證的幾個(gè)步驟；在下面給出的示例中，我將積分分成三部分，并描述了如何估計(jì)第一部分，然后copilot正確地說(shuō)明了如何估計(jì)其余兩部分。

陶哲軒給出的例證

只要簡(jiǎn)單說(shuō)明一下如何對(duì)第一部分進(jìn)行估計(jì)，剩下的工作GitHub Copilot就能完成了，這也太驚艷了！

對(duì)此，陶哲軒的評(píng)價(jià)是：「Copilot的性能給我留下了深刻的印象（并且讓我有點(diǎn)不安）」。

他補(bǔ)充說(shuō)「雖然其中的許多建議并不那么合適，我估計(jì)Copilot可能建議了十幾句話(huà)，最終以某種形式出現(xiàn)在我的博客文章中?！?/p>

而他說(shuō)的博客文章就是這篇關(guān)于「非負(fù)量的和或積分的上界」。

圖片

博文地址：https://terrytao.wordpress.com/2023/09/30/bounding-sums-or-integrals-of-non-negative-quantities/

估計(jì)某個(gè)量的大小，是數(shù)分、概率論、組合學(xué)等領(lǐng)域中的常見(jiàn)問(wèn)題，如估計(jì)函數(shù)、序列、結(jié)合等的和或積分。

因此陶哲軒這篇估計(jì)非負(fù)量的和或積分上界，探討的正是數(shù)學(xué)領(lǐng)域的重要問(wèn)題。

圖片

陶哲軒在博客中總結(jié)了3種估算大量非負(fù)量和以及積分的方法，如算術(shù)平均值-幾何平均值不等式、Holder不等式、Markov不等式等。

圖片

其中的內(nèi)容和代碼沒(méi)有關(guān)系，但是Github Copilot依然給出了讓陶哲軒都感到驚嘆的內(nèi)容建議。

圖片

能讓陶哲軒都感到有點(diǎn)不安的Github Copilot，源于Github和OpenAI的合作。

它主要功能是利用生成式AI的能力為程序提供編碼的建議，自動(dòng)補(bǔ)充等編碼功能。而之所以它有如此強(qiáng)大的功能，和背后微軟，OpenAI的大量投入是分不開(kāi)的。

最近外媒報(bào)道，微軟提供的Github Copilot每月10刀的訂閱服務(wù)，在算力成本上，每個(gè)用戶(hù)要讓微軟虧損20美元/月。

圖片

文章地址：https://www.wsj.com/tech/ai/ais-costly-buildup-could-make-early-products-a-hard-sell-bdd29b9f?mod=followamazon

這些服務(wù)成本如此高昂的原因之一，是使用了最強(qiáng)大的AI模型，與普通的軟件或云服務(wù)相比，這些模型需要更多的電力，并對(duì)處理器的運(yùn)行造成更大的壓力。

文章中甚至將現(xiàn)在的AI工具的能力和成本做了一個(gè)讓人繃不住的比喻：

「用AI去做文章總結(jié)就像開(kāi)著蘭博基尼去送披薩一樣」。

足見(jiàn)現(xiàn)在科技巨頭們，為了讓用戶(hù)充分享受AI帶來(lái)的便利，真的是下了血本！

所以讓陶哲軒驚嘆的Github Copilot能在編碼之外還有如此強(qiáng)大的能力，也似乎不那么奇怪了。

AI如何輔助數(shù)學(xué)研究

顯然，現(xiàn)在所有人都已經(jīng)意識(shí)到：AI具有巨大潛力，它可以通過(guò)指導(dǎo)猜想生成、協(xié)助形式化數(shù)學(xué)等方式為數(shù)學(xué)發(fā)展做出貢獻(xiàn)。

在9月26日舉行的一場(chǎng)關(guān)于使用AI輔助數(shù)學(xué)推理的網(wǎng)絡(luò)研討會(huì)上，眾數(shù)學(xué)大咖云集，一起討論了人工智能技術(shù)如何用于推進(jìn)數(shù)學(xué)科學(xué)，跨學(xué)科合作如何開(kāi)辟新的機(jī)會(huì)。

陶哲軒也參與了會(huì)議，并結(jié)合自己與AI合作的經(jīng)歷談了自己的觀點(diǎn)。

圖片

大會(huì)對(duì)于AI輔助數(shù)學(xué)研究，AI專(zhuān)家和數(shù)學(xué)家協(xié)作配合的新機(jī)會(huì)和新挑戰(zhàn)，都展開(kāi)了充分地討論，可謂是干貨滿(mǎn)滿(mǎn)：

嘗試應(yīng)用機(jī)器學(xué)習(xí)方法來(lái)輔助或完成形式數(shù)學(xué)論證，現(xiàn)在已經(jīng)是人工智能應(yīng)用的一個(gè)獨(dú)特領(lǐng)域

AI在輔助數(shù)學(xué)研究中的獨(dú)特之處在于，數(shù)學(xué)具有一種自我驗(yàn)證的方法，可以用來(lái)檢查AI產(chǎn)生的結(jié)果，而其他AI任務(wù)通常需要人類(lèi)參與來(lái)評(píng)估反饋的質(zhì)量。

數(shù)學(xué)表達(dá)本身具有一種內(nèi)在的準(zhǔn)確性，因此機(jī)器學(xué)習(xí)在數(shù)學(xué)領(lǐng)域能夠在數(shù)據(jù)相對(duì)稀缺的情況下有效地推進(jìn)工作，這使得AI在數(shù)學(xué)領(lǐng)域具備明顯的優(yōu)勢(shì)。

在研討會(huì)上，多位數(shù)學(xué)領(lǐng)域?qū)＜疫M(jìn)行了知識(shí)分享和交流。

圖片

在使用機(jī)器學(xué)習(xí)協(xié)助數(shù)學(xué)發(fā)現(xiàn)方面,會(huì)議中數(shù)學(xué)家Heather提到了具體的幾個(gè)例子:

圖片

(1) DeepMind和數(shù)學(xué)家合作，利用機(jī)器學(xué)習(xí)從大量數(shù)據(jù)中尋找模式，形成了關(guān)于模形的新猜想。

(2) Sutherland等數(shù)學(xué)家也使用機(jī)器學(xué)習(xí)在模形式的工作中找到了新公式。

(3) Adam Wagner使用機(jī)器學(xué)習(xí)來(lái)尋找圖論問(wèn)題的反例。

(4) Javier Pena利用機(jī)器學(xué)習(xí)找到偏微分方程近似的數(shù)值解,以方便后續(xù)的嚴(yán)格數(shù)值方法的推進(jìn)。

在使用AI輔助證明方面,會(huì)議提到形式化證明可以將一個(gè)大證明分解成小塊,不同人可以負(fù)責(zé)不同部分。

圖片

這可能會(huì)開(kāi)啟新的科研協(xié)作模式——計(jì)算機(jī)可以自動(dòng)化證明中的某些步驟，已經(jīng)有許多前沿的數(shù)學(xué)領(lǐng)域使用了這種模式。

這種形式化證明的過(guò)程有利于數(shù)學(xué)家以新方式與AI進(jìn)行創(chuàng)造性的互動(dòng)。

這也體現(xiàn)了AI協(xié)助數(shù)學(xué)發(fā)現(xiàn)和傳統(tǒng)數(shù)學(xué)研究的不同：既有大公司提供計(jì)算資源的大規(guī)模合作，也有小規(guī)模的個(gè)人之間的合作探索。

學(xué)界需要對(duì)這些不同的合作模式保持開(kāi)放。

圖片

會(huì)議中，還有多位學(xué)者討論了AI在數(shù)學(xué)翻譯中的應(yīng)用

數(shù)學(xué)翻譯是指將一個(gè)數(shù)學(xué)問(wèn)題從一個(gè)領(lǐng)域翻譯到另一個(gè)領(lǐng)域的等價(jià)表達(dá),這是數(shù)學(xué)家解決問(wèn)題的基本工具之一。

數(shù)學(xué)家以一個(gè)圖論問(wèn)題為例。圖論問(wèn)題可以翻譯成代數(shù)問(wèn)題，兩者邏輯上是等價(jià)的，但表達(dá)上的術(shù)語(yǔ)和形式明顯不同。

AI轉(zhuǎn)換工具可以將一個(gè)看似毫無(wú)頭緒的問(wèn)題，轉(zhuǎn)化成一個(gè)可以用已有技術(shù)來(lái)解決的問(wèn)題。

還有學(xué)者進(jìn)一步指出，證明思路到形式證明的轉(zhuǎn)換，以及形式證明到實(shí)際算法的轉(zhuǎn)換，也是一種翻譯過(guò)程。

鑒于AI在不同語(yǔ)言之間的翻譯上取得了巨大進(jìn)展，未來(lái)可以研究如何應(yīng)用機(jī)器學(xué)習(xí)來(lái)實(shí)現(xiàn)數(shù)學(xué)領(lǐng)域內(nèi)的翻譯。

例如將不完整的證明草圖自動(dòng)翻譯成可證明的形式表達(dá)。這是當(dāng)前一個(gè)非常有前景的研究方向。

會(huì)議中多位數(shù)學(xué)家也強(qiáng)調(diào)了。由于數(shù)學(xué)翻譯能顯著拓展問(wèn)題解決的視角，應(yīng)用機(jī)器學(xué)習(xí)來(lái)實(shí)現(xiàn)數(shù)學(xué)翻譯將可能大大推進(jìn)數(shù)學(xué)研究。

圖片

AI專(zhuān)家和數(shù)學(xué)家進(jìn)行跨界合作，需要面對(duì)的差異和挑戰(zhàn)

AI界和數(shù)學(xué)界，存在著諸多差異。

比如，機(jī)器學(xué)習(xí)研究者習(xí)慣處理大規(guī)模數(shù)據(jù)集，而數(shù)學(xué)家習(xí)慣于處理相對(duì)較少的數(shù)據(jù)。機(jī)器學(xué)習(xí)研究者注重在一類(lèi)任務(wù)上的平均表現(xiàn)，而數(shù)學(xué)家則更關(guān)注單個(gè)案例的解釋。

另外，兩者的出版文化不同，機(jī)器學(xué)習(xí)界會(huì)公開(kāi)發(fā)表絕大部分研究?jī)?nèi)容，數(shù)學(xué)界則不然。機(jī)器學(xué)習(xí)界普遍第一作者為主要貢獻(xiàn)者，數(shù)學(xué)界作者順序就比較隨機(jī)。

大規(guī)模合作項(xiàng)目的學(xué)術(shù)貢獻(xiàn)認(rèn)定上，二者也存在差異。形式化研究使得每個(gè)參與者只負(fù)責(zé)一小塊，如何評(píng)價(jià)貢獻(xiàn)是一個(gè)新問(wèn)題。

還有一個(gè)差異，是資源獲取方式。

機(jī)器學(xué)習(xí)需要大數(shù)據(jù)集和計(jì)算資源，數(shù)學(xué)家對(duì)這方面的需求就相對(duì)較少。如何使各界研究者公平獲取資源也會(huì)是一個(gè)問(wèn)題。開(kāi)源文化不同。機(jī)器學(xué)習(xí)界更看重開(kāi)源共享,而數(shù)學(xué)界不一定。如何處理二者關(guān)系需要考量。

由于這是一個(gè)全新的交叉領(lǐng)域,雙方在一些根本理念和工作方式上存在差異，需要在合作中加以認(rèn)識(shí)和調(diào)適，以實(shí)現(xiàn)更好的協(xié)同效果。

參考資料：

https://mathstodon.xyz/@tao/111206761117553482