【原】小樂(lè)數(shù)學(xué)科普：人機(jī)合作加速數(shù)學(xué)研究

zzllrr小樂(lè) 2023-10-25 發(fā)布于江蘇

展開(kāi)全文

本文作者是蘇珊·達(dá)戈斯蒂諾（Susan D'Agostino）,，哥倫比亞大學(xué)數(shù)學(xué)家和科普作家[21]（撰稿日期：2023-9）

有人可能會(huì)認(rèn)為,，獲得菲爾茲獎(jiǎng)以后,，可以平息任何數(shù)學(xué)家對(duì)他們繼續(xù)往前寫(xiě)證明的能力的嘮叨懷疑。但在彼得·舒爾茨（Peter Scholze）獲得2018年獎(jiǎng)項(xiàng)后不久,，[1] 他質(zhì)疑他與達(dá)斯汀·克勞森（Dustin Clausen）合著的液體向量空間定理（liquid vector space theorem）證明的一部分,。于是舒爾茨謙虛地向數(shù)學(xué)界求助。

“我在2019年的大部分時(shí)間里都沉迷于這個(gè)定理的證明,，幾乎為之瘋狂,，”舒爾茨在2020年12月Xena Project博客上寫(xiě)道關(guān)于證明中包含的泛函分析（functional analysis）黑匣子。[2] “我認(rèn)為沒(méi)有人敢看這個(gè)細(xì)節(jié),，所以我仍然有一些揮之不去的小疑問(wèn),。...這可能是我迄今為止最重要的定理......最好確定它是正確的?！?/p>

事實(shí)上,，阿爾伯塔大學(xué)數(shù)學(xué)助理教授亞當(dāng)·托帕茲（Adam Topaz）緊張地笑著承認(rèn)，他和他的研究小組在2020年閱讀該定理時(shí)跳過(guò)了該定理的證明,。

“他是一個(gè)非常有說(shuō)服力的人,，”Topaz在2023年2月加州大學(xué)洛杉磯分校（UCLA）的純數(shù)學(xué)與應(yīng)用數(shù)學(xué)研究所舉行的機(jī)器輔助證明會(huì)議中的一次演講中說(shuō)[3]?！叭绻f(shuō)什么是正確的,，人們往往會(huì)傾向于相信他?！?/p>

這就是為什么舒爾茨和由德國(guó)弗萊堡大學(xué)的Johan Commelin領(lǐng)導(dǎo)的團(tuán)隊(duì)啟動(dòng)了一個(gè)大型合作項(xiàng)目,，使用免費(fèi)開(kāi)源的Lean證明助手來(lái)驗(yàn)證證明。這個(gè)由社區(qū)驅(qū)動(dòng)的軟件主要由萊昂納多·德·莫拉（Leonardo de Moura）在微軟研究院工作時(shí)提供的[4],，并得到Lean社區(qū)建立的數(shù)學(xué)庫(kù)的支持,。托帕茲和其他數(shù)學(xué)家以及計(jì)算機(jī)科學(xué)家加入Commelin的費(fèi)力嘗試。根據(jù)Topaz的說(shuō)法,，到 2021年5月,，他們達(dá)到了第一個(gè)目標(biāo),，而到2022年7月，他們完成了需要98000行代碼的項(xiàng)目,。

“我覺(jué)得交互式證明助手,，現(xiàn)在處于可以在非常合理的時(shí)間跨度內(nèi)正式驗(yàn)證困難的原創(chuàng)研究的水平，這絕對(duì)是瘋狂的,，”舒爾茨在他的博客上寫(xiě)道,。

Topaz說(shuō)，如果沒(méi)有機(jī)器的幫助,，仔細(xì)檢查證明將是“不可能開(kāi)始的”（nonstarter）,。作為發(fā)現(xiàn)和修復(fù)一些不準(zhǔn)確之處并驗(yàn)證主定理證明的獎(jiǎng)勵(lì)，Topaz說(shuō)該小組還證明了一些輔助陳述,，回答了舒爾茨注記中的一些問(wèn)題,，并填補(bǔ)了Lean數(shù)學(xué)庫(kù)中的一些空白，特別是在同調(diào)代數(shù)（homological algebra）,，拓?fù)?/strong>（topology）和范疇論（category theory）方面,。

“這真的是一個(gè)人類項(xiàng)目，而不是一個(gè)機(jī)器人項(xiàng)目,，”Topaz說(shuō),。

自2022年底以來(lái)，學(xué)術(shù)界一直在談?wù)揅hatGPT,、GPT-4 和其他可能改變研究和大學(xué)寫(xiě)作的人工智能AI寫(xiě)作工具,。但數(shù)學(xué)界也在努力應(yīng)對(duì)顛覆，正如人機(jī)合作在數(shù)學(xué)研究的最前沿編寫(xiě)困難定理的證明所輔助所做,。機(jī)器不僅驗(yàn)證人類發(fā)現(xiàn)的數(shù)學(xué)結(jié)果,，還幫助數(shù)學(xué)家推理，探索新想法,，甚至學(xué)習(xí)新的數(shù)學(xué),。

自動(dòng)化和交互式方法

形式方法是計(jì)算機(jī)科學(xué)的一個(gè)子領(lǐng)域，它使用基于計(jì)算邏輯的技術(shù)來(lái)協(xié)助數(shù)學(xué)推理,，卡內(nèi)基梅隆大學(xué)哲學(xué)和數(shù)學(xué)科學(xué)教授杰里米·阿維加德（Jeremy Avigad）表示,。在子領(lǐng)域中，有自動(dòng)化方法和交互式方法,。廣義上講,，使用前者，一個(gè)人問(wèn)一個(gè)問(wèn)題,，按下一個(gè)按鈕,，然后得到一個(gè)答案——或者得到一個(gè)“我不知道”，這可能會(huì)讓數(shù)學(xué)家陷入困境。使用后者,，用戶與計(jì)算機(jī)一起探索或檢查推理,。這為可能性留下了空間。

“現(xiàn)在還為時(shí)過(guò)早,，我們?nèi)栽谂宄@項(xiàng)技術(shù)可以做什么,，”Avigad說(shuō)?！暗泻芏嘞Ｍ团d奮點(diǎn),。”

當(dāng)數(shù)學(xué)家與交互式證明助手一起工作時(shí),，他們可能會(huì)通過(guò)輸入基本定義和定理來(lái)“教”會(huì)計(jì)算機(jī)數(shù)學(xué)的新領(lǐng)域。他們以后可能會(huì)“詢問(wèn)”機(jī)器對(duì)這些對(duì)象的了解,。在形式化證明時(shí),，他們將嘗試讓計(jì)算機(jī)確定是否遵循先前的陳述，并在必要時(shí)提供更多信息,。通過(guò)這種方式,，人機(jī)合作填充細(xì)節(jié)并推進(jìn)嘗試走向嚴(yán)格化。

但是根據(jù)Avigad的說(shuō)法,，區(qū)分自動(dòng)化和交互式方法是一種錯(cuò)誤的二分法（dichotomy）,。

“即使你正在交互式地做數(shù)學(xué)，你也希望盡可能自動(dòng)化繁瑣的部分,，”Avigad說(shuō),。“即使你正在使用自動(dòng)化,，每當(dāng)你嘗試一些不起作用的東西時(shí),，你也會(huì)做出改變并重試。所以,，這個(gè)領(lǐng)域的兩方面共同成長(zhǎng),。

丹佛大學(xué)數(shù)學(xué)教授邁克爾·金尼恩（Michael Kinyon）在使用工具時(shí)也模糊了這一界限。也就是說(shuō),，他使用自動(dòng)定理證明器,，但他將它們用作證明助手。這項(xiàng)工作改變了他對(duì)研究問(wèn)題的方法,。

“我們可能會(huì)更快一些,，例如，先使用該軟件嘗試一些東西,，然后再坐下來(lái)凝視空白并試圖自己弄清楚,，”Kinyon說(shuō)。“在這些事情的早期階段,，人們更愿意進(jìn)行實(shí)驗(yàn),。”

一些人認(rèn)為,，計(jì)算機(jī)的“思考”方式與人類不同,，促進(jìn)了人類的發(fā)現(xiàn)過(guò)程。

“這打破了我們的模式,，加深了我們的理解,，”威斯康星大學(xué)數(shù)學(xué)教授喬丹·艾倫伯格（ Jordan Ellenberg）說(shuō)?！澳憧梢园研问交醋魇窍驒C(jī)器傳授數(shù)學(xué)思想,，而機(jī)器的'思維’與我們的非常不同?！?016年,，Ellenberg和荷蘭代爾夫特理工大學(xué)數(shù)學(xué)教授迪恩·吉斯韋特（Dion Gijswijt）解決了杯蓋集猜想（cap set conjecture，cap set為仿射幾何中的術(shù)語(yǔ)[19] [20],，這里cap暫譯為杯蓋∩,，與英語(yǔ)中的cup杯子∪相對(duì)，zzllrr小樂(lè)譯注）,，這一結(jié)果后來(lái)發(fā)表在[5]《數(shù)學(xué)年鑒》中,。

后來(lái)，在2019年,，數(shù)學(xué)家Sander Dahmen和來(lái)自阿姆斯特丹自由大學(xué)的計(jì)算機(jī)科學(xué)家Johannes H?lzl和Robert Lewis使用Lean定理證明器來(lái)形式化Ellenberg和Gijswijt定理的證明[6],。作者認(rèn)為，與其他數(shù)學(xué)子領(lǐng)域的證明相比,，形式化證明所必需的組合背景“不那么令人生畏”,。這種形式化工作提供了一些保證，即在有利的情況下,，人們可以通過(guò)計(jì)算機(jī)檢查《數(shù)學(xué)年鑒》最近的一篇論文,。但是，在這本受人尊敬的期刊中,，只有極少數(shù)論文包含具有“不那么令人生畏”的先決條件的簡(jiǎn)短證明,。熱心者可以希望該軟件會(huì)隨著時(shí)間的推移而改進(jìn)。

事關(guān)優(yōu)雅

有些人可能想知道機(jī)器是否將證明簡(jiǎn)化為計(jì)算,。但福特漢姆大學(xué)數(shù)學(xué)助理教授希瑟·麥克白（Heather Macbeth）認(rèn)為,，這種還原主義并不是這項(xiàng)工作的核心。這是因?yàn)槿祟悶榱死斫饩帉?xiě)證明,，而計(jì)算可能無(wú)法提供這一點(diǎn),。

“你可能會(huì)認(rèn)為,，當(dāng)你從紙張轉(zhuǎn)向計(jì)算機(jī)時(shí)，我們把[美]扔出窗外,，我們已經(jīng)決定我們將擁抱功能而不是形式,，我們真的要走向一個(gè)完成證明很重要的世界，”麥克白說(shuō),?！澳堑共皇恰,！保溈税自诩償?shù)學(xué)與應(yīng)用數(shù)學(xué)研究所會(huì)議上的發(fā)言）,。

麥克白花了三年時(shí)間編寫(xiě)了數(shù)千行Lean代碼，以努力使證明形式化,。兩年來(lái),，她還與其他人合作維護(hù)Lean數(shù)學(xué)庫(kù)。在這個(gè)角色中,，她審查了其他人編寫(xiě)的數(shù)千行代碼,，以評(píng)估代碼是否可以改進(jìn)，并確保它適合庫(kù)的其余部分,。

“我覺(jué)得其中一些真的很美，有些我不覺(jué)得,，”麥克白說(shuō),。“幾乎所有在紙上寫(xiě)的好數(shù)學(xué)的原則都延伸到形式數(shù)學(xué)中的相應(yīng)原則,?！?/p>

根據(jù)麥克白的說(shuō)法，自動(dòng)證明中包含的論證并不總是模仿人類思維模式,。

“盡管如此,，有一個(gè)很好的證明，并不完全是人類會(huì)想到的,，”麥克白說(shuō),。她觀察到，為了提高效率,，人類可能會(huì)在尋找證明的不同步驟中修剪搜索空間,。然而，機(jī)器可能會(huì)檢查更多的情況,，包括那些最初看起來(lái)不太有希望的情況,。

“這實(shí)際上是一個(gè)關(guān)于存在差異以及為什么這些差異很有趣的問(wèn)題，”麥克白說(shuō),。

此外,，一些證明在形式化過(guò)程中變得優(yōu)雅。托馬斯·布朗寧（Thomas Browning）和帕特里克·盧茨（Patrick Lutz）都是加州大學(xué)伯克利分校（University of California，Berkeley——UCB）的數(shù)學(xué)研究生,，他們努力將伽羅瓦理論形式化——這是一個(gè)許多人已經(jīng)認(rèn)為很優(yōu)雅的子領(lǐng)域,。但是在他們工作的某個(gè)時(shí)刻，他們需要使用任意的有限序列,，根據(jù)Browning和Lutz的說(shuō)法,，這不是Lean的優(yōu)勢(shì)。因此,，他們找到了解決方法,。

“這種策略主要只是為了避免處理某些類型的論證，這些論證在Lean中不能很好地進(jìn)行,，”Browning和Lutz在他們的論文中寫(xiě)道,。“但它確實(shí)有一個(gè)額外的好處,，即當(dāng)使用這種新的歸納原理重寫(xiě)時(shí),，一些標(biāo)準(zhǔn)證明會(huì)變得更簡(jiǎn)單?！?/p>

加速的趨勢(shì)

幾十年前,，機(jī)器輔助證明被主流數(shù)學(xué)家視為邊緣項(xiàng)目，布拉格捷克信息學(xué),、機(jī)器人和控制論研究所的杰出研究員約瑟夫·厄本（Josef Urban）表示,。

“知名數(shù)學(xué)家說(shuō)，像湯姆·黑爾斯（Tom Hales）這樣的人通過(guò)正式證明開(kāi)普勒猜想來(lái)浪費(fèi)他們的才能,，”Urban談到這位數(shù)學(xué)家時(shí)說(shuō),，他在通常裁判過(guò)程的挫敗感反應(yīng)之后，提供了一個(gè)機(jī)器驗(yàn)證的證明,?！霸谶^(guò)去的15年里，這種情況真的發(fā)生了變化,，這尤其要?dú)w功于Hales,。”

可以肯定的是,，機(jī)器輔助證明仍然有反對(duì)者,，包括哥倫比亞大學(xué)數(shù)學(xué)教授邁克爾·哈里斯（Michael Harris）。使用定理證明器的數(shù)學(xué)家必須學(xué)會(huì)用計(jì)算機(jī)理解的術(shù)語(yǔ)編碼和表達(dá)問(wèn)題,，這減少了花在數(shù)學(xué)上的時(shí)間。

“在我將我的問(wèn)題重新構(gòu)建成一種可以適應(yīng)這項(xiàng)技術(shù)的形式前,，我會(huì)自己解決問(wèn)題,，”哈里斯告訴量子雜志[7],。

羅格斯大學(xué)（Rutgers University）數(shù)學(xué)教授多倫·澤爾伯格（Doron Zeilberger）也不是機(jī)器證明的粉絲，盡管他的厭惡始于人類編寫(xiě)的證明,，并延伸到機(jī)器輔助證明,。

“我們不需要人類生成的數(shù)學(xué)的更多'正式版本’，”去年當(dāng)注意到對(duì)Avigad 和其他人的開(kāi)創(chuàng)性工作的贊賞時(shí),，Zeilberger在他的博客上寫(xiě)道[8],。“形式化已知的證明與倒讀隱語(yǔ)（Pig-Latin）沒(méi)有什么不同,。一旦你做了幾次,，它就不再有趣了。雖然這在智力和技術(shù)上都具有挑戰(zhàn)性,，否則這些聰明的人不會(huì)參與其中,，但這些人正在浪費(fèi)他們的才能?！?/p>

“事實(shí)上,，我們的硅仆人，即將成為我們的主人,，可以更有成效地使用,，”Zeilberger繼續(xù)說(shuō)道?！癈oq（另一個(gè)交互式定理證明器）和Lean延續(xù)了有害的希臘傳統(tǒng),，它引入了公理化方法，使數(shù)學(xué)成為演繹的,、以邏輯為中心的科學(xué)?！?/p>

但這些觀點(diǎn)似乎與人工智能的頂頭風(fēng)背道而馳,，人工智能的頂頭風(fēng)似乎正在推動(dòng)當(dāng)前社會(huì)的發(fā)展，包括數(shù)學(xué)界,。

倫敦帝國(guó)理工學(xué)院純數(shù)學(xué)教授凱文·巴扎德（Kevin Buzzard）在 2022年國(guó)際數(shù)學(xué)家大會(huì)上作了演講,，“數(shù)學(xué)中形式主義的興起”[9][23]。在那里,，他將情緒稱為不是“結(jié)束的開(kāi)始”,，而是“開(kāi)始的開(kāi)始”。在他看來(lái),，數(shù)學(xué)研究人員的工作沒(méi)有風(fēng)險(xiǎn),。然而，機(jī)器將越來(lái)越多地幫助人類證明數(shù)學(xué)定理,，不僅通過(guò)找出例子,，而且通過(guò)推理,。根據(jù)Buzzard的說(shuō)法，計(jì)算機(jī)還將幫助人類在數(shù)據(jù)庫(kù)中找到證明或反例,，構(gòu)建簡(jiǎn)單的證明,，并且通常使人類更容易學(xué)習(xí)數(shù)學(xué)。

巡回會(huì)議似乎支持這一說(shuō)法,。除了二月份在純粹與應(yīng)用數(shù)學(xué)研究所舉行的機(jī)器輔助證明會(huì)議外,，其他可敬的機(jī)構(gòu)今年也投入時(shí)間和空間讓數(shù)學(xué)家聚集在一起討論這一加速的趨勢(shì)。

5月,，班夫國(guó)際數(shù)學(xué)創(chuàng)新與發(fā)現(xiàn)研究站（Banff International Research Station for Mathematical Innovation and Discovery）舉辦了上同調(diào)理論形式化（Formalization of Cohomology Theories）研討會(huì)[10],，這匯集了形式化專家和學(xué)科專家，朝著前沿研究邁進(jìn),。6月,，西蒙斯·勞費(fèi)爾數(shù)學(xué)科學(xué)研究所（Simons Laufer Mathematical Sciences Institute）在數(shù)學(xué)形式化暑期研究生院課程中向研究生介紹了其背后的技術(shù)和思想[11]。7月,，麻省理工學(xué)院洛侖茲中心舉辦機(jī)器檢查數(shù)學(xué)研討會(huì)[12],，針對(duì)那些聽(tīng)說(shuō)過(guò)但尚未嘗試這項(xiàng)技術(shù)的數(shù)學(xué)家。

在美國(guó)以外,，哥本哈根大學(xué)在6月舉辦了一個(gè)大師班[13],，稱為數(shù)學(xué)的形式化，以建立舒爾茨的液體張量實(shí)驗(yàn),。7月,，荷蘭洛倫茲中心提供[14]機(jī)器檢查數(shù)學(xué)，為期一周的入門研討會(huì),，面向感興趣的數(shù)學(xué)家,，旨在促進(jìn)合作。同樣在夏天,，豪斯多夫數(shù)學(xué)研究所提供了一個(gè)計(jì)劃[15],，形式數(shù)學(xué)的前景，為專家和初級(jí)研究人員提供一個(gè)論壇,，讓他們聚集,、合作，并“更好地將他們與數(shù)學(xué)主流聯(lián)系起來(lái)”,。9月,，該機(jī)構(gòu)提供[16]為期一周的系列講座[17]，形式數(shù)學(xué)和計(jì)算機(jī)輔助證明,。更多內(nèi)容可以在Lean社區(qū)網(wǎng)站上找到[18],。此外，Lean并不是唯一的交互式定理證明器,。根據(jù)Buzzard的說(shuō)法,，其他系統(tǒng)包括Coq,，Isabelle / HOL，HOL Light,，Agda,，cubical Agda，Metamath和Mizar,。

“他們數(shù)字化了音樂(lè) - CD,，MP3 - 但當(dāng)時(shí)沒(méi)有人預(yù)見(jiàn)到后果是 - Napster，Spotify,，”Buzzard在演講中說(shuō),。“我們正在將數(shù)學(xué)數(shù)字化,，我相信這將不可避免地改變數(shù)學(xué),。歡迎您加入我們?！?/p>

參考資料

https://www./science/Fields-Medal

https://xenaproject./2020/12/05/liquid-tensor-experiment/

https://www.ipam./programs/workshops/machine-assisted-proofs/?tab=schedule

https://leanprover-community./

https://annals.math./2017/185-1/p08

https://drops./opus/volltexte/2019/11070/

https://www./how-close-are-computers-to-automating-mathematical-reasoning-20200827/

https://sites.math./~zeilberg/Opinion184.html

https://www./watch?v=SEID4XYFN7o

https://www./events/2023/5-day-workshops/23w5124

https://www./summer_schools/1021