陶哲軒：“這個(gè)領(lǐng)域發(fā)展太快了”
陶哲軒點(diǎn)贊轉(zhuǎn)發(fā)，《美國(guó)數(shù)學(xué)學(xué)會(huì)通報(bào)》用一整期特刊介紹了AI給數(shù)學(xué)帶來(lái)的改變。
作者陣容非常豪華，包括菲爾茲獎(jiǎng)得主Akshay Venkatesh、華裔數(shù)學(xué)家鄭樂雋、計(jì)算機(jī)科學(xué)家Ernest Davis等多位知名學(xué)者。
其中鄭樂雋表示，如果最終機(jī)器能做得比人類更好，那很好，她將樂意退出數(shù)學(xué)領(lǐng)域去彈鋼琴。
他們提出的觀點(diǎn)包括：
- AI的數(shù)學(xué)能力不完全反映人類的認(rèn)知過程，依賴于訓(xùn)練數(shù)據(jù)中的模式，而不是真正理解問題的本質(zhì)。
- 合成數(shù)學(xué)如合成拓?fù)鋵W(xué)和合成微分幾何學(xué)，提供了一種全新的數(shù)學(xué)實(shí)踐方式，允許數(shù)學(xué)家專注于更深層次的概念和問題。
- 交互式證明系統(tǒng)與軟件工程中的“規(guī)范驅(qū)動(dòng)開發(fā)”，可以降低數(shù)學(xué)家的認(rèn)知負(fù)荷、促進(jìn)數(shù)學(xué)家之間的合作。
- 形式化證明技術(shù)可能改變數(shù)學(xué)證明的本質(zhì)、顛覆數(shù)學(xué)家的工作方式。
- 數(shù)學(xué)屆不應(yīng)被科技公司主導(dǎo)的議程所綁架。
在開篇，編委會(huì)寫道：
現(xiàn)在，是數(shù)學(xué)家們了解并推動(dòng)這場(chǎng)辯論，并決定學(xué)科未來(lái)方向的時(shí)候了。
AI能自動(dòng)證明定理嗎？
計(jì)算機(jī)已經(jīng)在數(shù)學(xué)中發(fā)揮了重要作用，尤其是在計(jì)算效率方面的提升，但是否能夠幫助人類進(jìn)行數(shù)學(xué)推理？有一天它們是否會(huì)自主進(jìn)行推理？
數(shù)學(xué)家Kevin Buzzard概述了神經(jīng)網(wǎng)絡(luò)、計(jì)算機(jī)定理證明器和大型語(yǔ)言模型的最新發(fā)展。
Kevin Buzzard現(xiàn)任英國(guó)倫敦帝國(guó)理工學(xué)院數(shù)學(xué)教授，他專門研究算術(shù)幾何和朗蘭茲綱領(lǐng)。
回顧整個(gè)計(jì)算工具的歷史，最早Computer一詞還指人類作為“計(jì)算員”，他們的成就不應(yīng)被低估。
17世紀(jì)早期，蘇格蘭數(shù)學(xué)家John Napier構(gòu)造了第一個(gè)對(duì)數(shù)表，他提出如果有更多“計(jì)算員”來(lái)幫忙，就可以進(jìn)一步推進(jìn)這一工作。
另一個(gè)代表性成果是Felkel和Vega在18世紀(jì)70年代發(fā)表的整數(shù)因式分解表，這使研究素?cái)?shù)分布成為可能，最終導(dǎo)致了素?cái)?shù)定理的證明。
早期電子計(jì)算機(jī)出現(xiàn)后，機(jī)器在高速計(jì)算方面已經(jīng)遠(yuǎn)超人類，Computer一詞的含義也發(fā)生了變化。
如劍橋大學(xué)在1957年購(gòu)買了EDSAC II計(jì)算機(jī)，用于海洋學(xué)計(jì)算，為現(xiàn)代板塊構(gòu)造理論奠定基礎(chǔ)。
這個(gè)階段計(jì)算機(jī)還只是一個(gè)工具，即使目前的計(jì)算機(jī)也難以像人類一樣進(jìn)行數(shù)學(xué)推理和定理證明。
神經(jīng)網(wǎng)絡(luò)可以用于搜索定理、猜測(cè)新定理和尋找反例，如發(fā)現(xiàn)了拓?fù)鋵W(xué)中關(guān)于結(jié)點(diǎn)和邊的關(guān)系的新定理，以及在表示論中發(fā)現(xiàn)了關(guān)于Kazhdan-Lusztig多項(xiàng)式的新結(jié)果，但對(duì)于證明深?yuàn)W復(fù)雜的定理還有局限性。
自動(dòng)定理證明系統(tǒng)（ATP）可以自動(dòng)證明一些復(fù)雜的定理，如羅賓斯猜想。但ATP生成的證明往往過于冗長(zhǎng)，難以被人類理解。
交互式定理證明系統(tǒng)（ITP）可以用于驗(yàn)證定理的正確性，幫助發(fā)現(xiàn)和修正數(shù)學(xué)文獻(xiàn)中的錯(cuò)誤，如數(shù)學(xué)家Peter Scholze在液體張量實(shí)驗(yàn)（Liquid Tensor Experiment）中承認(rèn)自己無(wú)法掌握所有涉及的數(shù)學(xué)對(duì)象和概念，最終在Lean系統(tǒng)幫助下完成。
大模型如ChatGPT雖然可以生成相關(guān)數(shù)學(xué)內(nèi)容，但容易產(chǎn)生錯(cuò)誤。Buzzard建議大模型與ITP等系統(tǒng)結(jié)合使用，通過大模型生成初步證明，然后由ITP進(jìn)行驗(yàn)證，從而提高可靠性。
Buzzard認(rèn)為，這些新興技術(shù)可以幫助數(shù)學(xué)家突破認(rèn)知障礙，探索更加復(fù)雜和更加新穎的數(shù)學(xué)領(lǐng)域，并最終改變數(shù)學(xué)家的工作方式，使他們能夠?qū)⒏鄷r(shí)間和精力投入到數(shù)學(xué)思維和理解上。
另外三篇文章，從不同角度探討了這些新興技術(shù)如何幫助數(shù)學(xué)家應(yīng)對(duì)日益增長(zhǎng)的復(fù)雜性，并開拓新的數(shù)學(xué)領(lǐng)域。
數(shù)學(xué)的形式化轉(zhuǎn)向
邏輯學(xué)家Jeremy Avigad討論了自20世紀(jì)初以來(lái)，數(shù)學(xué)定義和證明可以在具有精確語(yǔ)法和使用規(guī)則的形式系統(tǒng)中表示。
Jeremy Avigad任卡內(nèi)基梅隆大學(xué)哲學(xué)和數(shù)學(xué)教授，在數(shù)理邏輯和基礎(chǔ)、形式驗(yàn)證和交互式定理證明以及數(shù)學(xué)哲學(xué)和歷史領(lǐng)域做出了貢獻(xiàn)。
他認(rèn)為這種轉(zhuǎn)向可能改變數(shù)學(xué)的本質(zhì)，依賴機(jī)器驗(yàn)證的證明可能減少了數(shù)學(xué)家對(duì)直觀理解和洞察的重視，從而可能影響數(shù)學(xué)發(fā)現(xiàn)的過程和數(shù)學(xué)思想的發(fā)展。
純數(shù)學(xué)中的抽象邊界和規(guī)范驅(qū)動(dòng)開發(fā)
數(shù)學(xué)家Johan Commelin和Adam Topaz探討了抽象邊界（Abstraction Boundaries）如何在交互式定理證明器的幫助下，幫助控制數(shù)學(xué)研究中的復(fù)雜性。
Johan Commelin任荷蘭烏得勒支大學(xué)助理教授，Adam Topaz阿爾伯塔大學(xué)助理教授，兩人研究興趣的交點(diǎn)是代數(shù)幾何，共同參與了液體張量試驗(yàn)。
△左：Johan Commelin，右：Adam Topaz
抽象邊界是指在數(shù)學(xué)研究和定理證明過程中，將數(shù)學(xué)對(duì)象的實(shí)現(xiàn)細(xì)節(jié)與其外在屬性和行為進(jìn)行形式化區(qū)分的界限。這種界限使得數(shù)學(xué)家可以在不依賴具體實(shí)現(xiàn)細(xì)節(jié)的情況下，使用和推理這些數(shù)學(xué)對(duì)象。
抽象邊界的概念在軟件工程中非常常見，例如通過C語(yǔ)言的頭文件、面向?qū)ο缶幊讨械墓卜椒ɑ蛘吆瘮?shù)式編程中的typeclass來(lái)實(shí)現(xiàn)。
基于抽象邊界的“規(guī)范驅(qū)動(dòng)開發(fā)”方法，不僅降低了認(rèn)知負(fù)荷，還促進(jìn)了數(shù)學(xué)家之間的合作，使得工作可以輕松地分配給具有不同專長(zhǎng)的合作者。
奇異新世界：定理證明助手和合成基礎(chǔ)
數(shù)學(xué)家Michael Shulman認(rèn)為，現(xiàn)有的計(jì)算機(jī)程序如Lean證明助手，能夠驗(yàn)證數(shù)學(xué)證明的正確性，但它們專門的證明語(yǔ)言對(duì)許多數(shù)學(xué)家來(lái)說(shuō)是一道門檻。
Michael Shulman任圣地亞哥大學(xué)副教授，研究領(lǐng)域是范疇論和代數(shù)拓?fù)洹?span style="display:none">kDO速刷資訊——每天刷點(diǎn)最新資訊，了解這個(gè)世界多一點(diǎn)SUSHUAPOS.COM
現(xiàn)有的計(jì)算機(jī)證明助手能夠驗(yàn)證數(shù)學(xué)證明的正確性，但它們專門的證明語(yǔ)言對(duì)許多數(shù)學(xué)家來(lái)說(shuō)是一道門檻。大模型有潛力降低這一門檻，使數(shù)學(xué)家能夠以更熟悉的語(yǔ)言與證明助手進(jìn)行交互。
這可能允許數(shù)學(xué)家使用由模型支持的證明助手探索根本上全新的數(shù)學(xué)領(lǐng)域，現(xiàn)有的證明助手已經(jīng)在同倫類型論（homotopy type theory）等領(lǐng)域發(fā)揮了這一作用。
當(dāng)前的人工智能可以做嚴(yán)肅的數(shù)學(xué)嗎？
紐約大學(xué)計(jì)算機(jī)科學(xué)家Ernest Davis指出，當(dāng)前AI在解決文字描述的數(shù)學(xué)問題上，無(wú)法可靠地結(jié)合基礎(chǔ)數(shù)學(xué)和常識(shí)推理。
AI通過三種主要方法嘗試解決數(shù)學(xué)問題，但每種方法都有其優(yōu)勢(shì)和局限。
- 直接生成答案，適用于簡(jiǎn)單數(shù)學(xué)問題。
- 生成可執(zhí)行代碼，已在實(shí)踐中取得成功。
- 翻譯成邏輯規(guī)范，對(duì)于復(fù)雜問題仍存在挑戰(zhàn)。
他認(rèn)為AI在解決數(shù)學(xué)奧林匹克問題時(shí)可能會(huì)依賴于訓(xùn)練數(shù)據(jù)中的模式，而不是真正理解問題的本質(zhì)，這與人類通過直觀和邏輯推理解決問題的方式有顯著差異。
AI真正解決數(shù)學(xué)問題需要三類知識(shí)：基礎(chǔ)數(shù)學(xué)、語(yǔ)言理解和世界常識(shí)。例如理解硬幣的價(jià)值和物理特性。常識(shí)在解決問題時(shí)經(jīng)常被忽視，但實(shí)際上是至關(guān)重要的。
基準(zhǔn)測(cè)試集是評(píng)估AI系統(tǒng)性能的重要工具，但它們可能無(wú)法全面覆蓋AI的所有能力。
但同時(shí)他也指出，盡管AI在處理基礎(chǔ)問題時(shí)存在局限，但這可能不會(huì)影響其進(jìn)行高級(jí)數(shù)學(xué)研究的能力。
一方面，高級(jí)數(shù)學(xué)研究可能不需要與解決基礎(chǔ)問題相同的常識(shí)推理能力。
另一方面，在棋類游戲上，即使AI無(wú)法理解棋局的基本概念，在棋局分析和策略制定上的能力能遠(yuǎn)超人類棋手。
數(shù)學(xué)家如何看待AI？
關(guān)于自動(dòng)化與數(shù)學(xué)研究的一些想法
菲爾茲獎(jiǎng)得主Akshay Venkatesh探討了數(shù)學(xué)自動(dòng)化對(duì)數(shù)學(xué)研究的影響。他指出，機(jī)器可能大大增強(qiáng)數(shù)學(xué)解決問題的能力，但也會(huì)徹底改變數(shù)學(xué)的核心問題和價(jià)值觀，使其難以被人類所認(rèn)知。
他分析了當(dāng)前數(shù)學(xué)界決定“什么是重要”的機(jī)制，如期刊、獎(jiǎng)項(xiàng)、數(shù)學(xué)理論在應(yīng)用領(lǐng)域得到認(rèn)可、教育體系、聘用和資助過程等，都不足以解釋數(shù)學(xué)界相對(duì)較高的共識(shí)水平。
他認(rèn)為“證明”這種特殊的學(xué)術(shù)交流方式能引發(fā)一致同意，類似于自由市場(chǎng)中信息傳播的機(jī)制。
AI會(huì)導(dǎo)致當(dāng)前數(shù)學(xué)界對(duì)“重要性”的判斷發(fā)生劇變。
機(jī)器如何使數(shù)學(xué)更包容
數(shù)學(xué)家鄭樂雋（Eugenia Cheng）認(rèn)為，技術(shù)已經(jīng)在改變?nèi)藗冄芯繑?shù)學(xué)的方式，可以利用這些技術(shù)使數(shù)學(xué)更加包容，而不是使數(shù)學(xué)家變得多余。
鄭樂雋在謝菲爾德大學(xué)任教，除了范疇論研究和本科教學(xué)之外，她的目標(biāo)是消除世界上的“數(shù)學(xué)恐懼癥”。
她分析了技術(shù)如何影響數(shù)學(xué)教學(xué)、提出問題、協(xié)作、傳播以及研究：
- 教學(xué)：標(biāo)準(zhǔn)的“粉筆和黑板”式講授變得沒有必要，她開始采用交互性更強(qiáng)的教學(xué)方式。同時(shí)對(duì)于學(xué)生來(lái)說(shuō)，記憶現(xiàn)在已經(jīng)無(wú)關(guān)緊要，應(yīng)當(dāng)將大腦留給更有趣的事情
- 提出問題：技術(shù)使得任何人都可以在網(wǎng)上提問并獲得答復(fù)，但繼承和放大了數(shù)學(xué)界的精英主義和競(jìng)爭(zhēng)性。
- 協(xié)作：技術(shù)大大便利了遠(yuǎn)程協(xié)作，使地理位置不再是障礙。電子白板等工具也大大增強(qiáng)了協(xié)作的便利性。
- 傳播：互聯(lián)網(wǎng)使論文傳播變得普及，不再局限于有限的紙質(zhì)期刊。這讓論文發(fā)表過程更加公開透明，論文質(zhì)量而非發(fā)表渠道成為關(guān)鍵。
- 研究：通過智能手機(jī)可以隨時(shí)隨地展開研究，不受地點(diǎn)限制。搜索引擎等也讓她不必記住所有事實(shí)，可以隨時(shí)查閱。
總的來(lái)說(shuō)，鄭樂雋認(rèn)為技術(shù)可以使數(shù)學(xué)變得更加包容，只要數(shù)學(xué)家善用這些技術(shù)，而不是固步自封。
同時(shí)她也提出，如果最終機(jī)器能做得比人類更好，那很好，她將樂意退出數(shù)學(xué)領(lǐng)域去彈鋼琴。
機(jī)器時(shí)代下的證明
數(shù)論學(xué)家Andrew Granville關(guān)注證明的本質(zhì)以及計(jì)算機(jī)證明與人類證明之間的關(guān)系。
他認(rèn)為，純數(shù)學(xué)中的“客觀性”并非如我們所想那樣牢不可破。
- 定義和概念的困難：現(xiàn)代數(shù)學(xué)中很多概念沒有單一明確的定義，存在多種可能的定義和闡釋。這就難以談“客觀”。
- 公理系統(tǒng)的局限性：根據(jù)哥德爾不完備性定理，即使采用一致的公理系統(tǒng)，也無(wú)法證明所有關(guān)于整數(shù)的正確語(yǔ)句。這說(shuō)明“客觀的”數(shù)學(xué)基礎(chǔ)是有局限性的。
- 歷史演變的影響：不同時(shí)代數(shù)學(xué)家對(duì)“數(shù)學(xué)證明”的理解和標(biāo)準(zhǔn)有所不同，這體現(xiàn)了客觀性標(biāo)準(zhǔn)的變遷。
他探討了計(jì)算機(jī)自動(dòng)證明可能同時(shí)帶來(lái)的挑戰(zhàn)和機(jī)遇。計(jì)算機(jī)證明可以幫助確認(rèn)人類直觀證明的正確性，提高可信度。但計(jì)算機(jī)證明可能會(huì)取代人類，成為“黑箱”證明。但這種證明可能缺乏人類應(yīng)有的可理解性和適應(yīng)性。
Granville希望未來(lái)的計(jì)算機(jī)證明能夠吸收人類證明的優(yōu)點(diǎn)，在形式化的基礎(chǔ)上保持足夠的靈活性和易理解性。
自動(dòng)化迫使數(shù)學(xué)家反思自己的價(jià)值觀
哥倫比亞大學(xué)數(shù)學(xué)家Michael Harris強(qiáng)調(diào)數(shù)學(xué)需要吸收其他學(xué)科、尤其是人文社科的經(jīng)驗(yàn)。
他建議經(jīng)常反思學(xué)科的價(jià)值追求和物質(zhì)基礎(chǔ)，有助于數(shù)學(xué)家在面對(duì)自動(dòng)化等挑戰(zhàn)時(shí)，更好地捍衛(wèi)數(shù)學(xué)的核心價(jià)值。
此外，他還警示數(shù)學(xué)界不應(yīng)被科技公司主導(dǎo)的議程所綁架，科技公司的價(jià)值取向與數(shù)學(xué)家的價(jià)值取向并不完全一致，數(shù)學(xué)家應(yīng)保持獨(dú)立思考的勇氣，而不是被動(dòng)接受來(lái)自產(chǎn)業(yè)的價(jià)值導(dǎo)向。
更多精彩內(nèi)容7月發(fā)布
特刊的第二部分將于2024年7月發(fā)布，內(nèi)容將包括：
- 自動(dòng)化與哲學(xué)：
形式化所引發(fā)的許多問題并不新鮮。McLarty的文章描述，龐加萊在一個(gè)多世紀(jì)前就在討論“推理機(jī)器”。龐加萊已經(jīng)關(guān)注到形式化證明與數(shù)學(xué)實(shí)踐之間的關(guān)系，這一主題在de Toffolli的文章中得到了進(jìn)一步的探討。
- 技術(shù)改變思維
DeDeo的文章檢驗(yàn)了自動(dòng)證明對(duì)數(shù)學(xué)家認(rèn)知過程的潛在影響。
- 深度學(xué)習(xí)與數(shù)學(xué)的互動(dòng)
Bengio和Malkin的文章考慮了進(jìn)行數(shù)學(xué)研究對(duì)機(jī)器學(xué)習(xí)帶來(lái)的特定挑戰(zhàn)。Fraser和Poggio的文章則提出了與深度學(xué)習(xí)數(shù)學(xué)基礎(chǔ)相關(guān)的問題。
敬請(qǐng)期待～
期刊地址：
https://www.ams.org/journals/bull/2024-61-02/
參考鏈接：
[1]https://mathstodon.xyz/@tao/112221953164171331
本文鏈接：陶哲軒轉(zhuǎn)發(fā)、菲爾茲獎(jiǎng)得主領(lǐng)銜：AI正在顛覆數(shù)學(xué)家的工作方式 | 美國(guó)數(shù)學(xué)學(xué)會(huì)特刊http://m.sq15.cn/show-2-4657-0.html
聲明：本網(wǎng)站為非營(yíng)利性網(wǎng)站，本網(wǎng)頁(yè)內(nèi)容由互聯(lián)網(wǎng)博主自發(fā)貢獻(xiàn)，不代表本站觀點(diǎn)，本站不承擔(dān)任何法律責(zé)任。天上不會(huì)到餡餅，請(qǐng)大家謹(jǐn)防詐騙！若有侵權(quán)等問題請(qǐng)及時(shí)與本網(wǎng)聯(lián)系，我們將在第一時(shí)間刪除處理。
上一篇： 北大&火山引擎奪冠！CLIC視頻壓縮挑戰(zhàn)賽結(jié)果公布，中國(guó)團(tuán)隊(duì)表現(xiàn)亮眼