盡管許多人并不愿意承認(rèn)，但是很可能，AI 會在十年內(nèi)趕超人類數(shù)學(xué)家。
前幾天，一篇加州理工和 MIT 研究者用 ChatGPT 證明數(shù)學(xué)定理的論文爆火，在數(shù)學(xué)圈引發(fā)了極大關(guān)注。
英偉達首席科學(xué)家 Jim Fan 激動轉(zhuǎn)發(fā)，稱 AI 數(shù)學(xué) Copilot 已經(jīng)到來，下一個發(fā)現(xiàn)新定理的，就是全自動 AI 數(shù)學(xué)家了！
紐約時報近日也發(fā)文，稱數(shù)學(xué)家們做好準(zhǔn)備，AI 將在十年內(nèi)趕上甚至超過最優(yōu)秀的人類數(shù)學(xué)家。
而陶哲軒本人，也轉(zhuǎn)發(fā)了此文。
AI 也來顛覆數(shù)學(xué)界了！
如今，數(shù)學(xué)家們不得不正視一股最新的革命性力量 ——AI。
2019 年，谷歌前雇員、現(xiàn)任灣區(qū)初創(chuàng)公司員工的計算機科學(xué)家 Christian Szegedy 預(yù)測，計算機系統(tǒng)將在十年內(nèi)趕上或超過最優(yōu)秀的人類數(shù)學(xué)家解決問題的能力。而去年，他把目標(biāo)日期修改為 2026 年。
2018 年菲爾茲獎得主、普林斯頓高等研究院的數(shù)學(xué)家 Akshay Venkatesh 目前還對使用 AI 不感興趣，但他十分熱衷于討論 AI 相關(guān)的話題。
去年的采訪中，Venkatesh 表示，「我希望我的學(xué)生意識到，這個領(lǐng)域會發(fā)生非常大的變化?！?/p>
而最近他的態(tài)度是：「我不反對通過深思熟慮、甚至刻意地使用 AI，來輔助人類的理解。但我堅信，對于我們使用它的方式，我們需要保持正念，慎之又慎?！?/p>
在今年二月，加州大學(xué)洛杉磯分校理論與應(yīng)用數(shù)學(xué)研究所，曾舉行了一場關(guān)于「機器輔助證明」的研討會。
研討會的主要組織者，就是 2006 年的菲爾茲獎得主、在 UCLA 任職的數(shù)學(xué)家陶哲軒。
他指出，用 AI 輔助數(shù)學(xué)證明，其實是非常值得關(guān)注的現(xiàn)象。
直到最近幾年，數(shù)學(xué)家才開始擔(dān)心 AI 的潛在威脅，無論是 AI 對于數(shù)學(xué)美學(xué)的破壞，還是對于數(shù)學(xué)家本身的威脅。
而杰出的社區(qū)成員們，正在把這些問題擺上臺面，開始探索如何「打破禁忌」。
從歐幾里得幾何原本到計算機代碼
幾千年來，數(shù)學(xué)家已經(jīng)早已適應(yīng)了邏輯和推理的最新進展。不過，他們準(zhǔn)備好迎接人工智能了嗎？
2000 多年來，歐幾里得的文本一直是數(shù)學(xué)論證和推理的范式。
卡內(nèi)基梅隆大學(xué)邏輯學(xué)家 Jeremy Avigad 說，歐幾里得以近乎詩意的「定義」開始，在此基礎(chǔ)上建立了當(dāng)時的數(shù)學(xué) —— 使用基本概念、定義和先前的定理，每個連續(xù)的步驟都「清楚地遵循」以前的步驟，以這樣一種方式證明事物。
有人抱怨說，歐幾里得的一些「明顯」的步驟，其實不太明顯，但 Avigad 博士說，但這個系統(tǒng)奏效了。
但是到 20 世紀(jì)以后，數(shù)學(xué)家們不愿意再將數(shù)學(xué)建立在這種直觀的幾何基礎(chǔ)上了。
相反，他們開發(fā)了正式的系統(tǒng)，這個系統(tǒng)中有著精確的符號表示和機械的規(guī)則。
最終，在這種系統(tǒng)下，數(shù)學(xué)可以被翻譯為計算機代碼。
1976 年，四色定理成為第一個在暴力計算的幫助下被證明的主要定理。
會抱怨的 AI：抱歉，我看不懂你們的定理
有這樣一個數(shù)學(xué)小工具，被稱為證明助手，或交互式定理證明器。
數(shù)學(xué)家會一步一步地將證明轉(zhuǎn)換為代碼，然后用軟件程序檢查推理是否正確。
驗證過程會累積在一個動態(tài)規(guī)范參考庫中，其他人都可以查閱。
霍斯金森形式數(shù)學(xué)中心主任 Avigad 博士說，這種類型的形式化為今天的數(shù)學(xué)奠定了基礎(chǔ)，就像歐幾里得試圖將那個時代的數(shù)學(xué)轉(zhuǎn)碼，從而為其提供基礎(chǔ)一樣。
最近，開源證明助手系統(tǒng) Lean 再次引發(fā)了大量關(guān)注。
Lean 是現(xiàn)在的亞馬遜計算機科學(xué)家 Leonardo de Moura 在微軟時開發(fā)的。
Lean 使用的是自動推理，由老式的 AI GOFAI 提供支持，這是一個受邏輯啟發(fā)的象征式 AI。
截至目前，Lean 已經(jīng)驗證了一個將球體從內(nèi)到外轉(zhuǎn)動的有趣定理，以及一個統(tǒng)一數(shù)學(xué)領(lǐng)域方案的關(guān)鍵定理。
但是，證明助手也有缺點：它會時常抱怨自己不理解數(shù)學(xué)家輸入的定義、公理或推理步驟，因此它也被賜名「證明抱怨器」。
這些抱怨會讓研究變得繁瑣，但 Fordham 大學(xué)的數(shù)學(xué)家 Heather Macbeth 表示，這類提供逐行反饋的功能，也會讓系統(tǒng)對教學(xué)很有用。
今年春天，Macbeth 博士曾設(shè)計了一門「雙語」課程，她將黑板上的每個問題都翻譯成講義中的 Lean 代碼，學(xué)生們需要用 Lean 和自然語言提交解決方案。
「這給了他們信心，」Macbeth 博士說，因為他們會收到即時反饋，關(guān)于證明何時完成，以及沿途的每一步是對還是錯。
而在參加研討會后，約翰霍普金斯大學(xué)的數(shù)學(xué)家 Emily Riehl 也嘗試了一把。
她用了一個證明助手小程序，來證明自己此前發(fā)表過的文章中的定理。
使用完后，她大為震驚?！肝椰F(xiàn)在很深入得了解了證明的過程，比我之前的理解要深刻得多。我的思路如此清晰，以至于我可以向最蠢的計算機解釋清楚?！?/p>
暴力推理 —— 這很不「數(shù)學(xué)」
另一個計算機科學(xué)家們經(jīng)常會用來解決一些數(shù)學(xué)問題的工具叫做「暴力推理」，但是數(shù)學(xué)界對于這種方法卻常常嗤之以鼻。
然而，AI 科學(xué)家們好像并不太在意數(shù)學(xué)家們的想法，不斷地用他們自己熟悉的辦法，去攻占數(shù)學(xué)「高地」。
卡耐基梅隆大學(xué)的計算機科學(xué)家 Heule 曾經(jīng)在 2016 年用一個 200T 的「SAT 求解器」文件去解決「布爾畢達哥拉斯三元組問題」。
《自然》雜志在文章中卻說到：200T 的證明是史上最大的證明過程，用這些工具解決問題是否真的算數(shù)學(xué)？
但是在解決問題的論文作者本人，計算機科學(xué)家 Heule 看來，「這種方法是解決超過人類能力范圍的問題所必須的。」
同樣的，在國際象棋比賽中戰(zhàn)勝了人類（AlphaZero）之后，DeepMind 又設(shè)計了機器學(xué)習(xí)算法來解決蛋白質(zhì)折疊（AlphaFold）。
DeepMind 發(fā)表了一篇論文，認(rèn)為他們?nèi)〉眠@些成果的方式，是通過 AI 來引導(dǎo)人類的直覺，從而推進數(shù)學(xué)發(fā)展。
而一位前谷歌計算機科學(xué)家，現(xiàn)在正在灣區(qū)創(chuàng)業(yè)的 Yuhuai Wu 也表示，自己的創(chuàng)業(yè)的方向就是利用機器學(xué)習(xí)來解決數(shù)學(xué)問題。
他目前的項目，Minerva，就是一個用來解決數(shù)學(xué)模型的微調(diào)大語言模型。
未來，他希望這個項目能成長為一個「自動化數(shù)學(xué)家」，可以作為一個通用研究助理來「獨立解決數(shù)學(xué)問題」。
數(shù)學(xué)是一個試金石
另一方面，很多深度接觸過 AI 技術(shù)的數(shù)學(xué)家也對 AI 在數(shù)學(xué)研究中不被重視提出了擔(dān)心。
他們認(rèn)為，人工智能技術(shù)經(jīng)常能夠「直接地」幫助數(shù)學(xué)家們「找到」自己想要的答案。
雖然數(shù)學(xué)家或者 AI 專家們都搞不清楚 AI 是如何找到這個答案的。
與 DeepMind 合作過的數(shù)學(xué)家 Geordie Williamson 曾經(jīng)分享了一段與 DeepMind 合作的經(jīng)歷。
他在和 DeepMind 合作的過程中，DeepMind 發(fā)現(xiàn)的一個神經(jīng)網(wǎng)絡(luò)可以預(yù)測他認(rèn)為很重要的數(shù)據(jù)值，而且異常準(zhǔn)確。
他就很努力地去試圖理解 AI 是如何做到的，因為這可能成為一個定理的基礎(chǔ)。
但他最后還是沒辦法搞懂 AI 的邏輯，而且 DeepMind 的人也沒法做到。
就像歐幾里得一樣，神經(jīng)網(wǎng)絡(luò)以某種方式找到了真理，但是邏輯原因卻很難被理解。
另一方面，從這位數(shù)學(xué)家的角度看來，推理是數(shù)學(xué)的精髓，但卻是機器學(xué)習(xí)中一直缺少的一塊拼圖。
在科技圈中，如果有一個黑箱在大部分情況下都能提供解決問題的方法，科技圈就會非常滿足了。
AI 就是這樣一個黑箱。
但是數(shù)學(xué)家們卻不會滿足于這種狀況。
這位數(shù)學(xué)家看來，嘗試?yán)斫馍窠?jīng)網(wǎng)絡(luò)的原理會引發(fā)出令人著迷的數(shù)學(xué)問題。
而解決這些問題，會讓數(shù)學(xué)家「為世界做出有意義的貢獻」。
假如 AI 能證明數(shù)學(xué)定理
如果 AI 生成的假設(shè)定理充斥整個世界，我們該怎么做？
網(wǎng)友對此發(fā)出靈魂拷問，我對 AI 系統(tǒng)提出新的假設(shè) / 公式是第一步有所懷疑，因為 DeepMind 早已在紐結(jié)理論中做到了。
我想知道，社區(qū)將如何應(yīng)對 AI 輸出的大量新假設(shè)。check 人工智能創(chuàng)建的邏輯論點是一回事；被數(shù)百萬個「哦，這可能是真的」建議淹沒是另一回事。我不認(rèn)為我們現(xiàn)有的評論和出版系統(tǒng)為此做好了準(zhǔn)備。
這會對人們對數(shù)學(xué)的信任產(chǎn)生什么影響？
有人認(rèn)為，機器并不能很快就能完成數(shù)學(xué)研究，但可以看到它改變了研究方式，就像機器學(xué)習(xí)模型和計算能力如何改變了生物學(xué)領(lǐng)域一樣。
還有網(wǎng)友表示，從 AlphaDev 開始，我就一直在思考這個問題，但是同樣的程序可以構(gòu)建排序算法，也可以使用自動證明檢查器來證明數(shù)學(xué)定理。真正的問題是它是否可以用來證明一些重要的東西，而不僅僅是微不足道的發(fā)現(xiàn)。
不過還是有網(wǎng)友依然對 GPT 類的工具能否真的發(fā)現(xiàn)有價值的真理持懷疑態(tài)度。
也有網(wǎng)友指出，可能人類和 AI 對于數(shù)學(xué)理解和關(guān)注本就有區(qū)別，AI 證明了什么是真的，而人類總是關(guān)注為什么它是真的。
參考資料：
https://www.nytimes.com/2023/07/02/science/ai-mathematics-machine-learning.html
本文來自微信公眾號：新智元 （ID：AI_era）
廣告聲明：文內(nèi)含有的對外跳轉(zhuǎn)鏈接（包括不限于超鏈接、二維碼、口令等形式），用于傳遞更多信息，節(jié)省甄選時間，結(jié)果僅供參考，IT之家所有文章均包含本聲明。