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

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

就在6月底，加州理工、英偉達(dá)、MIT等機(jī)構(gòu)的學(xué)者，曾構(gòu)建了一個(gè)基于開源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è)過程中，我們當(dāng)然可以隨時(shí)嘗試任何級別的節(jié)點(diǎn)，但如果它是灰色的，我們可能就沒有足夠的知識來完成這個(gè)節(jié)點(diǎn)。

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

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

圖片

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

皮亞諾公理

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

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

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

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

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

圖片

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

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

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

圖片

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

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

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

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

圖片

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

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

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

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

圖片

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

GitHub Copilot，讓我不安

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

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

圖片

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

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

最近，他又稱贊到——

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

陶哲軒給出的例證

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

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

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

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

圖片

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

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

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

圖片

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

圖片

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

圖片

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

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

最近外媒報(bào)道，微軟提供的Github Copilot每月10刀的訂閱服務(wù)，在算力成本上，每個(gè)用戶要讓微軟虧損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ù)相比，這些模型需要更多的電力，并對處理器的運(yùn)行造成更大的壓力。

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

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

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

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

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

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

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

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

圖片

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

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

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

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

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

圖片

在使用機(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í)來尋找圖論問題的反例。

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

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

圖片

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

這種形式化證明的過程有利于數(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é)界需要對這些不同的合作模式保持開放。

圖片

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

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

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

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

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

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

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

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

圖片

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

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

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

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

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

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

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

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

參考資料：

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