陶哲軒：幾周前，AI突破數(shù)學(xué)形式化臨界點(diǎn)

來源：量子位

數(shù)學(xué)界的“最強(qiáng)大腦”，快被AI出的證明淹沒了。

菲爾茲獎(jiǎng)得主陶哲軒分享了他在IEANTN項(xiàng)目（顯式解析數(shù)論網(wǎng)絡(luò)集成項(xiàng)目）中的最新體驗(yàn)：

AI生成正確證明的速度太快了，但證明寫得太臃腫，人類根本來不及審。

幾周前還需要志愿者花數(shù)周才能認(rèn)領(lǐng)完成的形式化任務(wù)，現(xiàn)在AI幾小時(shí)就能搞定。

一個(gè)17世紀(jì)數(shù)學(xué)家帕斯卡就注意到的現(xiàn)象正在以全新的方式困擾著當(dāng)代數(shù)學(xué)：

生成一個(gè)冗長(zhǎng)的正確證明，比生成一個(gè)簡(jiǎn)短的正確證明更容易。

陶哲軒把這個(gè)現(xiàn)象稱為“阻抗不匹配”，而AI把這個(gè)矛盾推到了極致。

從數(shù)周到數(shù)小時(shí)

陶哲軒主導(dǎo)的IEANTN項(xiàng)目，目標(biāo)是將顯式解析數(shù)論中大量技術(shù)性論文形式化，在Lean證明助手中建立一個(gè)活的、可動(dòng)態(tài)更新的數(shù)論估計(jì)網(wǎng)絡(luò)。

這個(gè)工作涉及大量繁瑣的數(shù)值驗(yàn)證和參數(shù)匹配。

用陶哲軒自己的話說，這類工作占據(jù)了他思考解析數(shù)論問題時(shí)至少70%的時(shí)間。

按傳統(tǒng)方法，他會(huì)把單個(gè)引理拆分成獨(dú)立任務(wù)發(fā)布出去，然后等待志愿者認(rèn)領(lǐng)——通常要等好幾周。

由于人工形式化本身困難，志愿者會(huì)自然而然地追求證明的簡(jiǎn)短、高效和自然，提交的代碼審查起來也很輕松。

但在最近幾周，自動(dòng)形式化技術(shù)突然跨過了某個(gè)臨界點(diǎn)。

陶哲軒發(fā)布的幾乎每一個(gè)形式化任務(wù)，都能在數(shù)小時(shí)內(nèi)被AI工具完成。

項(xiàng)目中待認(rèn)領(lǐng)的未解決issue隊(duì)列，基本清空了。

AI能做局部?jī)?yōu)化，做不了全局重構(gòu)

速度的飛躍帶來了意想不到的副作用。

AI生成的形式化證明往往比人類寫的長(zhǎng)出數(shù)百行，包含大量冗余步驟，許多引理沒有在合適的抽象層次上陳述。

單看任何一個(gè)證明，好像都不是大問題，因?yàn)檫@些證明本來就不是給人讀的。

但每個(gè)臃腫證明都會(huì)給項(xiàng)目總構(gòu)建時(shí)間增加幾十秒，累積效應(yīng)變得不可忽視。

陶哲軒把這稱為“阻抗失配”：證明生成、證明驗(yàn)證、證明消化三個(gè)環(huán)節(jié)之間的速度差距正在拉大。

生成端被AI加速了數(shù)個(gè)量級(jí)，但驗(yàn)證和消化端仍然依賴人類的認(rèn)知帶寬。

具體到實(shí)踐中，將一個(gè)包含數(shù)千行代碼（其中部分由AI生成）的中等規(guī)模Lean文檔，轉(zhuǎn)化為一個(gè)結(jié)構(gòu)優(yōu)雅、適合提交到Mathlib數(shù)學(xué)庫(kù)的版本，成了一項(xiàng)頗具挑戰(zhàn)的工作。

陶哲軒發(fā)現(xiàn)了當(dāng)前AI工具的一個(gè)清晰邊界。

讓AI做局部的“code golf”（代碼精簡(jiǎn)），它能勝任，可以把證明的體積壓縮一些。

但全局性的重構(gòu)決策，完全超出了現(xiàn)有AI工具的能力范圍。

比如發(fā)現(xiàn)某個(gè)論證在文檔中多處重復(fù)出現(xiàn)，可以抽象為一個(gè)獨(dú)立引理，而這個(gè)引理可能在當(dāng)前文件之外還有更廣泛的用途。

陶哲軒指出，他可以向AI解釋這樣一個(gè)重構(gòu)方案，AI隨后能執(zhí)行它，但AI無法自發(fā)地發(fā)現(xiàn)這類重構(gòu)機(jī)會(huì)。

AI擅長(zhǎng)處理局部的、原子化的任務(wù)，但對(duì)項(xiàng)目的全局結(jié)構(gòu)缺乏理解。在IEANTN項(xiàng)目的語境下，這意味著AI能快速生成單個(gè)引理的證明，卻無法判斷這個(gè)引理應(yīng)該如何嵌入整個(gè)數(shù)論估計(jì)網(wǎng)絡(luò)的架構(gòu)中。

項(xiàng)目推進(jìn)速度確實(shí)比預(yù)期快了很多。

但陶哲軒表示，他現(xiàn)在需要花更多時(shí)間來提前規(guī)劃形式化任務(wù)的scope，預(yù)判AI會(huì)迅速交回一個(gè)證明，因此在發(fā)布任務(wù)時(shí)就要考慮好如何讓結(jié)果更易審查、更兼容項(xiàng)目的全局結(jié)構(gòu)。

換句話說，瓶頸從“等人來做證明”轉(zhuǎn)移到了“設(shè)計(jì)好任務(wù)讓AI的產(chǎn)出能被有效整合”。數(shù)學(xué)家的角色正在從親自執(zhí)行證明，轉(zhuǎn)向成為證明工程的架構(gòu)師。

要實(shí)現(xiàn)這個(gè)愿景，每一塊拼圖都必須在正確的抽象層次、以正確的接口標(biāo)準(zhǔn)存在于系統(tǒng)中。AI能以驚人速度生產(chǎn)拼圖塊，但拼圖塊的形狀是否與整體藍(lán)圖匹配，目前仍然只有人類能判斷。

參考鏈接：
[1]https://mathstodon.xyz/@tao/116789374373843141
[2]https://www.ipam.ucla.edu/news-research/special-projects/integrated-explicit-analytic-number-theory-network/

閱讀最新前沿科技趨勢(shì)報(bào)告，請(qǐng)?jiān)L問21世紀(jì)關(guān)鍵技術(shù)研究院的“未來知識(shí)庫(kù)”

未來知識(shí)庫(kù)是 “21世紀(jì)關(guān)鍵技術(shù)研究院”建 立的在線知識(shí)庫(kù)平臺(tái)，收藏的資料范圍包括人工智能、腦科學(xué)、互聯(lián)網(wǎng)、超級(jí)智能，數(shù)智大腦、能源、軍事、經(jīng)濟(jì)、人類風(fēng)險(xiǎn)等等領(lǐng)域的前沿進(jìn)展與未來趨勢(shì)。目前擁有超過8000篇重要資料。每周更新不少于100篇世界范圍最新研究資料。 歡迎掃描二維碼或訪問https://wx.zsxq.com/group/454854145828進(jìn)入。

截止到2月28日 ”未來知識(shí)庫(kù)”精選的百部前沿科技趨勢(shì)報(bào)告

（加入未來知識(shí)庫(kù)，全部資料免費(fèi)閱讀和下載）