前幾天，一篇加州理工和MIT研究者用ChatGPT證明數(shù)學(xué)定理的論文爆火，在數(shù)學(xué)圈引發(fā)了極大關(guān)注。

(資料圖)

圖片

英偉達(dá)首席科學(xué)家Jim Fan激動(dòng)轉(zhuǎn)發(fā)，稱AI數(shù)學(xué)Copilot已經(jīng)到來(lái)，下一個(gè)發(fā)現(xiàn)新定理的，就是全自動(dòng)AI數(shù)學(xué)家了！

紐約時(shí)報(bào)近日也發(fā)文，稱數(shù)學(xué)家們做好準(zhǔn)備，AI將在十年內(nèi)趕上甚至超過(guò)最優(yōu)秀的人類數(shù)學(xué)家。

圖片

而陶哲軒本人，也轉(zhuǎn)發(fā)了此文。

圖片

Siobhan Roberts參加了今年Machine Assisted Proofs舉辦的IPAM研討會(huì)，隨后她根據(jù)自己的經(jīng)歷和采訪，寫下了這篇關(guān)于AI和數(shù)學(xué)的文章

AI也來(lái)顛覆數(shù)學(xué)界了！

如今，數(shù)學(xué)家們不得不正視一股最新的革命性力量——AI。

2019年，谷歌前雇員、現(xiàn)任灣區(qū)初創(chuàng)公司員工的計(jì)算機(jī)科學(xué)家Christian Szegedy預(yù)測(cè)，計(jì)算機(jī)系統(tǒng)將在十年內(nèi)趕上或超過(guò)最優(yōu)秀的人類數(shù)學(xué)家解決問(wèn)題的能力。而去年，他把目標(biāo)日期修改為2026年。

卡內(nèi)基梅隆大學(xué)的邏輯學(xué)家Jeremy Avigad（藍(lán)衣服），與學(xué)生在形式化數(shù)學(xué)暑期學(xué)校中

2018年菲爾茲獎(jiǎng)得主、普林斯頓高等研究院的數(shù)學(xué)家Akshay Venkatesh目前還對(duì)使用AI不感興趣，但他十分熱衷于討論AI相關(guān)的話題。

去年的采訪中，Venkatesh表示，「我希望我的學(xué)生意識(shí)到，這個(gè)領(lǐng)域會(huì)發(fā)生非常大的變化?！?/p>

而最近他的態(tài)度是：「我不反對(duì)通過(guò)深思熟慮、甚至刻意地使用AI，來(lái)輔助人類的理解。但我堅(jiān)信，對(duì)于我們使用它的方式，我們需要保持正念，慎之又慎?！?/p>

在今年二月，加州大學(xué)洛杉磯分校理論與應(yīng)用數(shù)學(xué)研究所，曾舉行了一場(chǎng)關(guān)于「機(jī)器輔助證明」的研討會(huì)。

圖片

研討會(huì)的主要組織者，就是2006年的菲爾茲獎(jiǎng)得主、在UCLA任職的數(shù)學(xué)家陶哲軒。

他指出，用AI輔助數(shù)學(xué)證明，其實(shí)是非常值得關(guān)注的現(xiàn)象。

直到最近幾年，數(shù)學(xué)家才開(kāi)始擔(dān)心AI的潛在威脅，無(wú)論是AI對(duì)于數(shù)學(xué)美學(xué)的破壞，還是對(duì)于數(shù)學(xué)家本身的威脅。

而杰出的社區(qū)成員們，正在把這些問(wèn)題擺上臺(tái)面，開(kāi)始探索如何「打破禁忌」。

暑期學(xué)校的組織者，自左至右：Avigad，Patrick Massot和Heather Macbeth

從歐幾里得幾何原本到計(jì)算機(jī)代碼

幾千年來(lái)，數(shù)學(xué)家已經(jīng)早已適應(yīng)了邏輯和推理的最新進(jìn)展。不過(guò)，他們準(zhǔn)備好迎接人工智能了嗎？

圖片

洛杉磯蓋蒂博物館中17世紀(jì)古希臘數(shù)學(xué)家歐幾里得的肖像：他衣衫襤褸，舉著自己的幾何論文《元素》

2000多年來(lái)，歐幾里得的文本一直是數(shù)學(xué)論證和推理的范式。

卡內(nèi)基梅隆大學(xué)邏輯學(xué)家Jeremy Avigad說(shuō)，歐幾里得以近乎詩(shī)意的「定義」開(kāi)始，在此基礎(chǔ)上建立了當(dāng)時(shí)的數(shù)學(xué)——使用基本概念、定義和先前的定理，每個(gè)連續(xù)的步驟都「清楚地遵循」以前的步驟，以這樣一種方式證明事物。

圖片

有人抱怨說(shuō)，歐幾里得的一些「明顯」的步驟，其實(shí)不太明顯，但Avigad博士說(shuō)，但這個(gè)系統(tǒng)奏效了。

但是到20世紀(jì)以后，數(shù)學(xué)家們不愿意再將數(shù)學(xué)建立在這種直觀的幾何基礎(chǔ)上了。

相反，他們開(kāi)發(fā)了正式的系統(tǒng)，這個(gè)系統(tǒng)中有著精確的符號(hào)表示和機(jī)械的規(guī)則。

圖片

https://kilthub.cmu.edu/articles/journal_contribution/A_Formal_System_for_Euclid_s_Elements/6490703

最終，在這種系統(tǒng)下，數(shù)學(xué)可以被翻譯為計(jì)算機(jī)代碼。

圖片

1976年，四色定理成為第一個(gè)在暴力計(jì)算的幫助下被證明的主要定理。

四色定理：四種顏色足以填充地圖，使得沒(méi)有兩個(gè)相鄰區(qū)域顏色相同

會(huì)抱怨的AI：抱歉，我看不懂你們的定理

有這樣一個(gè)數(shù)學(xué)小工具，被稱為證明助手，或交互式定理證明器。

數(shù)學(xué)家會(huì)一步一步地將證明轉(zhuǎn)換為代碼，然后用軟件程序檢查推理是否正確。

驗(yàn)證過(guò)程會(huì)累積在一個(gè)動(dòng)態(tài)規(guī)范參考庫(kù)中，其他人都可以查閱。

圖片

https://www.andrew.cmu.edu/user/avigad/Papers/formal_turn.pdf

霍斯金森形式數(shù)學(xué)中心主任Avigad博士說(shuō)，這種類型的形式化為今天的數(shù)學(xué)奠定了基礎(chǔ)，就像歐幾里得試圖將那個(gè)時(shí)代的數(shù)學(xué)轉(zhuǎn)碼，從而為其提供基礎(chǔ)一樣。

最近，開(kāi)源證明助手系統(tǒng)Lean再次引發(fā)了大量關(guān)注。

圖片

Lean是現(xiàn)在的亞馬遜計(jì)算機(jī)科學(xué)家Leonardo de Moura在微軟時(shí)開(kāi)發(fā)的。

Lean使用的是自動(dòng)推理，由老式的AI GOFAI提供支持，這是一個(gè)受邏輯啟發(fā)的象征式AI。

圖片

截至目前，Lean已經(jīng)驗(yàn)證了一個(gè)將球體從內(nèi)到外轉(zhuǎn)動(dòng)的有趣定理，以及一個(gè)統(tǒng)一數(shù)學(xué)領(lǐng)域方案的關(guān)鍵定理。

圖片

圖片

圖片

圖片

但是，證明助手也有缺點(diǎn)：它會(huì)時(shí)常抱怨自己不理解數(shù)學(xué)家輸入的定義、公理或推理步驟，因此它也被賜名「證明抱怨器」。

這些抱怨會(huì)讓研究變得繁瑣，但Fordham大學(xué)的數(shù)學(xué)家Heather Macbeth表示，這類提供逐行反饋的功能，也會(huì)讓系統(tǒng)對(duì)教學(xué)很有用。

圖片

https://leanprover-community.github.io/courses.html

今年春天，Macbeth博士曾設(shè)計(jì)了一門「雙語(yǔ)」課程，她將黑板上的每個(gè)問(wèn)題都翻譯成講義中的Lean代碼，學(xué)生們需要用Lean和自然語(yǔ)言提交解決方案。

圖片

https://hrmacbeth.github.io/math2001/

「這給了他們信心，」Macbeth博士說(shuō)，因?yàn)樗麄儠?huì)收到即時(shí)反饋，關(guān)于證明何時(shí)完成，以及沿途的每一步是對(duì)還是錯(cuò)。

而在參加研討會(huì)后，約翰霍普金斯大學(xué)的數(shù)學(xué)家Emily Riehl也嘗試了一把。

圖片

約翰霍普金斯大學(xué)的數(shù)學(xué)家Emily Riehl一直在使用實(shí)驗(yàn)證明輔助程序

她用了一個(gè)證明助手小程序，來(lái)證明自己此前發(fā)表過(guò)的文章中的定理。

使用完后，她大為震驚?！肝椰F(xiàn)在很深入得了解了證明的過(guò)程，比我之前的理解要深刻得多。我的思路如此清晰，以至于我可以向最蠢的計(jì)算機(jī)解釋清楚?！?/p>

圖片

學(xué)生們?cè)跀?shù)學(xué)形式化暑期學(xué)校期間參加的一個(gè)小組項(xiàng)目

暴力推理——這很不「數(shù)學(xué)」

另一個(gè)計(jì)算機(jī)科學(xué)家們經(jīng)常會(huì)用來(lái)解決一些數(shù)學(xué)問(wèn)題的工具叫做「暴力推理」，但是數(shù)學(xué)界對(duì)于這種方法卻常常嗤之以鼻。

然而，AI科學(xué)家們好像并不太在意數(shù)學(xué)家們的想法，不斷地用他們自己熟悉的辦法，去攻占數(shù)學(xué)「高地」。

卡耐基梅隆大學(xué)的計(jì)算機(jī)科學(xué)家Heule曾經(jīng)在2016年用一個(gè)200T的「SAT 求解器」文件去解決「布爾畢達(dá)哥拉斯三元組問(wèn)題」。

圖片

https://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-force/fulltext

《自然》雜志在文章中卻說(shuō)到：200T的證明是史上最大的證明過(guò)程，用這些工具解決問(wèn)題是否真的算數(shù)學(xué)？

圖片

但是在解決問(wèn)題的論文作者本人，計(jì)算機(jī)科學(xué)家Heule看來(lái)，「這種方法是解決超過(guò)人類能力范圍的問(wèn)題所必須的。」

圖片

同樣的，在國(guó)際象棋比賽中戰(zhàn)勝了人類（AlphaZero）之后，DeepMind又設(shè)計(jì)了機(jī)器學(xué)習(xí)算法來(lái)解決蛋白質(zhì)折疊（AlphaFold）。

DeepMind發(fā)表了一篇論文，認(rèn)為他們?nèi)〉眠@些成果的方式，是通過(guò)AI來(lái)引導(dǎo)人類的直覺(jué)，從而推進(jìn)數(shù)學(xué)發(fā)展。

圖片

https://www.nature.com/articles/s41586-021-04086-x

而一位前谷歌計(jì)算機(jī)科學(xué)家，現(xiàn)在正在灣區(qū)創(chuàng)業(yè)的Yuhuai Wu也表示，自己的創(chuàng)業(yè)的方向就是利用機(jī)器學(xué)習(xí)來(lái)解決數(shù)學(xué)問(wèn)題。

圖片

他目前的項(xiàng)目，Minerva，就是一個(gè)用來(lái)解決數(shù)學(xué)模型的微調(diào)大語(yǔ)言模型。

未來(lái)，他希望這個(gè)項(xiàng)目能成長(zhǎng)為一個(gè)「自動(dòng)化數(shù)學(xué)家」，可以作為一個(gè)通用研究助理來(lái)「獨(dú)立解決數(shù)學(xué)問(wèn)題」。

圖片

數(shù)學(xué)是一個(gè)試金石

另一方面，很多深度接觸過(guò)AI技術(shù)的數(shù)學(xué)家也對(duì)AI在數(shù)學(xué)研究中不被重視提出了擔(dān)心。

他們認(rèn)為，人工智能技術(shù)經(jīng)常能夠「直接地」幫助數(shù)學(xué)家們「找到」自己想要的答案。

雖然數(shù)學(xué)家或者AI專家們都搞不清楚AI是如何找到這個(gè)答案的。

與DeepMind合作過(guò)的數(shù)學(xué)家Geordie Williamson曾經(jīng)分享了一段與DeepMind合作的經(jīng)歷。

他在和DeepMind合作的過(guò)程中，DeepMind發(fā)現(xiàn)的一個(gè)神經(jīng)網(wǎng)絡(luò)可以預(yù)測(cè)他認(rèn)為很重要的數(shù)據(jù)值，而且異常準(zhǔn)確。

圖片

他就很努力地去試圖理解AI是如何做到的，因?yàn)檫@可能成為一個(gè)定理的基礎(chǔ)。

但他最后還是沒(méi)辦法搞懂AI的邏輯，而且DeepMind的人也沒(méi)法做到。

就像歐幾里得一樣，神經(jīng)網(wǎng)絡(luò)以某種方式找到了真理，但是邏輯原因卻很難被理解。

另一方面，從這位數(shù)學(xué)家的角度看來(lái)，推理是數(shù)學(xué)的精髓，但卻是機(jī)器學(xué)習(xí)中一直缺少的一塊拼圖。

在科技圈中，如果有一個(gè)黑箱在大部分情況下都能提供解決問(wèn)題的方法，科技圈就會(huì)非常滿足了。

AI就是這樣一個(gè)黑箱。

但是數(shù)學(xué)家們卻不會(huì)滿足于這種狀況。

這位數(shù)學(xué)家看來(lái)，嘗試?yán)斫馍窠?jīng)網(wǎng)絡(luò)的原理會(huì)引發(fā)出令人著迷的數(shù)學(xué)問(wèn)題。

而解決這些問(wèn)題，會(huì)讓數(shù)學(xué)家「為世界做出有意義的貢獻(xiàn)」。

假如AI能證明數(shù)學(xué)定理

如果AI生成的假設(shè)定理充斥整個(gè)世界，我們?cè)撛趺醋觯?/p>

網(wǎng)友對(duì)此發(fā)出靈魂拷問(wèn)，我對(duì)AI系統(tǒng)提出新的假設(shè)/公式是第一步有所懷疑，因?yàn)镈eepMind早已在紐結(jié)理論中做到了。

我想知道，社區(qū)將如何應(yīng)對(duì)AI輸出的大量新假設(shè)。check人工智能創(chuàng)建的邏輯論點(diǎn)是一回事；被數(shù)百萬(wàn)個(gè)「哦，這可能是真的」建議淹沒(méi)是另一回事。我不認(rèn)為我們現(xiàn)有的評(píng)論和出版系統(tǒng)為此做好了準(zhǔn)備。

這會(huì)對(duì)人們對(duì)數(shù)學(xué)的信任產(chǎn)生什么影響？

圖片

有人認(rèn)為，機(jī)器并不能很快就能完成數(shù)學(xué)研究，但可以看到它改變了研究方式，就像機(jī)器學(xué)習(xí)模型和計(jì)算能力如何改變了生物學(xué)領(lǐng)域一樣。

圖片

還有網(wǎng)友表示，從AlphaDev開(kāi)始，我就一直在思考這個(gè)問(wèn)題，但是同樣的程序可以構(gòu)建排序算法，也可以使用自動(dòng)證明檢查器來(lái)證明數(shù)學(xué)定理。真正的問(wèn)題是它是否可以用來(lái)證明一些重要的東西，而不僅僅是微不足道的發(fā)現(xiàn)。

圖片

圖片

不過(guò)還是有網(wǎng)友依然對(duì)GPT類的工具能否真的發(fā)現(xiàn)有價(jià)值的真理持懷疑態(tài)度。

圖片

也有網(wǎng)友指出，可能人類和AI對(duì)于數(shù)學(xué)理解和關(guān)注本就有區(qū)別，AI證明了什么是真的，而人類總是關(guān)注為什么它是真的。

關(guān)鍵詞：