40 多年的計(jì)算機(jī)難題 —— 忙碌海貍難題，被一群業(yè)余愛(ài)好者攻破了！
數(shù)學(xué)大佬陶哲軒轉(zhuǎn)發(fā)了這一消息，并欣慰表示：
這再一次體現(xiàn)了證明助手對(duì)于數(shù)學(xué)研究的協(xié)作是多么有用。
計(jì)算機(jī)科學(xué)家 Scott Aaronson 為此還寫(xiě)了一篇博文，并大肆贊賞：
這個(gè)發(fā)現(xiàn)是自 1983 年以來(lái)，忙碌海貍函數(shù)研究中最重要的進(jìn)展。
具體而言，人們歷經(jīng)數(shù)十年努力，終于找到了第五個(gè)“忙碌海貍”圖靈機(jī)：
BB (5) =47,176,870（5 狀態(tài)圖靈機(jī)，能在停下來(lái)之前寫(xiě)下 47,176,870 個(gè)“1”）
圖靈機(jī)是一種抽象的計(jì)算模型，通過(guò)讀取和寫(xiě)入 0 和 1 在無(wú)限磁帶上進(jìn)行計(jì)算。
早在 40 多年前，一群計(jì)算機(jī)科學(xué)家在德國(guó)多特蒙德舉行競(jìng)賽，尋找“忙碌海貍”圖靈機(jī)。
找出一個(gè)特定的圖靈機(jī)，在它停止之前能夠?qū)懴伦疃嗟?1（我們稱(chēng)之為忙碌海貍數(shù)）。
通過(guò)找出特定狀態(tài)下能在停止前寫(xiě)下最多 1 的圖靈機(jī)，我們能更好地理解計(jì)算理論的邊界。
自從 1974 年確定了第四個(gè)忙碌海貍數(shù)后，尋找第五個(gè)成了懸而未決的問(wèn)題。
而現(xiàn)在，來(lái)自世界各地的 20 多名貢獻(xiàn)者（其中大多數(shù)人沒(méi)有傳統(tǒng)的學(xué)術(shù)資格），使用一款名為 Coq 證明助手的軟件獲得了結(jié)果 ——47,176,870，該軟件證實(shí)數(shù)學(xué)證明沒(méi)有錯(cuò)誤。
這一成就瞬間令社區(qū)沸騰，其中愛(ài)爾蘭梅努斯大學(xué)計(jì)算機(jī)科學(xué)家 Damien Woods 驚嘆：
就像博爾特一樣，我很驚訝他們的速度如此之快！
嗯，快半個(gè)世紀(jì)過(guò)去了還算快？只能說(shuō)這個(gè)問(wèn)題雀食有億點(diǎn)難。
別著急，且看這群人如何長(zhǎng)江后浪推前浪抓住“第 5 只海貍”~
為什么提出“忙碌海貍”？
要回答這個(gè)問(wèn)題，首先需要簡(jiǎn)單了解一下二進(jìn)制圖靈機(jī)。
1936 年，計(jì)算機(jī)科學(xué)之父艾倫?圖靈提出了圖靈機(jī) ——
由一個(gè)無(wú)限長(zhǎng)的紙帶，一個(gè)讀寫(xiě)頭（可以讀取和寫(xiě)入紙帶上的信息），以及一組內(nèi)部狀態(tài)等基本部分組成。
圖靈機(jī)的行為由一組規(guī)則定義，這些規(guī)則可以想象成一張表。表中的每行代表一個(gè)規(guī)則，每列對(duì)應(yīng)讀寫(xiě)頭讀取到的符號(hào)（0 或 1）。
每條規(guī)則指定了在特定狀態(tài)下，讀寫(xiě)頭遇到 0 或 1 時(shí)應(yīng)該執(zhí)行的操作。操作通常包括：
寫(xiě)入符號(hào)：決定在當(dāng)前單元格寫(xiě)入什么符號(hào)（例如，將 0 替換為 1）。
移動(dòng)方向：決定讀寫(xiě)頭是向左移動(dòng)、向右移動(dòng)還是保持不動(dòng)。
狀態(tài)轉(zhuǎn)換：決定圖靈機(jī)的下一個(gè)狀態(tài)是什么。
除了處理 0 和 1 的規(guī)則外，還有一條特殊規(guī)則告訴圖靈機(jī)何時(shí)停止運(yùn)行。當(dāng)圖靈機(jī)進(jìn)入這個(gè)狀態(tài)時(shí)，它就不再執(zhí)行任何操作，相當(dāng)于“比賽結(jié)束”（這種狀態(tài)一般不計(jì)算在狀態(tài)集合里）。
而就在停機(jī)問(wèn)題上，已經(jīng)有研究觀(guān)察到：
一些圖靈機(jī)會(huì)相對(duì)較快地停止（比如這臺(tái) three-rule 圖靈機(jī)在 11 步后停止）
其他的則陷入了很容易發(fā)現(xiàn)的無(wú)限循環(huán)
這也啟發(fā)圖靈提出了著名的“停機(jī)問(wèn)題”：
圖靈機(jī)是否會(huì)在有限的步驟后停止運(yùn)行，或者它是否會(huì)無(wú)限期地運(yùn)行下去？
他還進(jìn)一步提到，停機(jī)問(wèn)題沒(méi)有通用的解決方案，因?yàn)槿藗冇肋h(yuǎn)無(wú)法確定適用于一臺(tái)機(jī)器的方法是否也適用于另一臺(tái)機(jī)器。
對(duì)于這個(gè)結(jié)論，數(shù)學(xué)家 Tibor Radó（以下簡(jiǎn)稱(chēng)拉多）不太滿(mǎn)意，并由此發(fā)明了“忙碌的海貍游戲”。
為了將停機(jī)問(wèn)題的本質(zhì)提煉成更簡(jiǎn)單的形式，拉多提出了一種方法 —— 將圖靈機(jī)根據(jù)它們擁有的規(guī)則數(shù)量進(jìn)行分組。
例如，一組代表所有只有一條規(guī)則的圖靈機(jī)，另一組代表所有有兩條規(guī)則的圖靈機(jī)，依此類(lèi)推。
1962 年，拉多利用這些有限的圖靈機(jī)組定義了“忙碌海貍游戲”。游戲的玩法是：
1.選擇一個(gè)組，即確定你的圖靈機(jī)將擁有的規(guī)則數(shù)量。
2.為組中的每臺(tái)機(jī)器提供一個(gè)初始狀態(tài)全是 0 的磁帶。
3.觀(guān)察這些機(jī)器的運(yùn)行。一些機(jī)器可能會(huì)無(wú)限期地運(yùn)行下去，而其他的則會(huì)在某個(gè)時(shí)刻停止。
4.在那些最終停止的機(jī)器中，有的會(huì)很快停止，有的則需要更多步驟。每個(gè)組中會(huì)有一個(gè)運(yùn)行時(shí)間最長(zhǎng)的機(jī)器，這臺(tái)機(jī)器被稱(chēng)為“忙碌海貍”。
5.在有 n 條規(guī)則的組中，這臺(tái)“忙碌海貍”在停止之前所執(zhí)行的步數(shù)就是所謂的“忙碌海貍數(shù)”BB (n)。
6.游戲的目標(biāo)是確定這些 BB (n) 的確切值。
拉多給這樣“極度低效”的圖靈機(jī)取了一個(gè)有趣且形象的名字：忙碌海貍（Busy Beaver，取自英語(yǔ)中的諺語(yǔ) as busy as a beaver）。
而這個(gè)游戲也最終引來(lái)一眾程序員和數(shù)學(xué)愛(ài)好者的瘋狂試玩。
早期吃螃蟹的人
Allen Brady（以下簡(jiǎn)稱(chēng)布雷迪），當(dāng)時(shí)的俄勒岡州立大學(xué)數(shù)學(xué)研究生，成了早期挑戰(zhàn)者之一。
在游戲推出前，人們已經(jīng)確定了 BB (1) = 1，BB (2) = 6，當(dāng)時(shí)人們正嘗試攻克 BB (3)。
布雷迪也投身 BB (3)，他編寫(xiě)了計(jì)算機(jī)程序來(lái)模擬圖靈機(jī)的行為，這個(gè)程序構(gòu)建了一種“家譜”，根據(jù)圖靈機(jī)初始行為的相似性，對(duì)具有相同規(guī)則數(shù)量的機(jī)器進(jìn)行分類(lèi)。
程序只在機(jī)器之間行為差異變得重要時(shí)才將家譜樹(shù)分成多個(gè)分支。如果模擬顯示某條分支上的機(jī)器會(huì)停止或進(jìn)入無(wú)限循環(huán)，程序就會(huì)剪掉這個(gè)分支，排除那些不會(huì)無(wú)限運(yùn)行下去的圖靈機(jī)。
編寫(xiě)程序只是第一步，布雷迪需要找到足夠強(qiáng)大的計(jì)算機(jī)來(lái)運(yùn)行它。
在 1964 年，這不是一件容易的事。最終，他在 90 英里外的靈長(zhǎng)類(lèi)動(dòng)物研究實(shí)驗(yàn)室找到了一臺(tái) SDS 920 計(jì)算機(jī)。
只可惜 BB (3) 進(jìn)行到一半，拉多的研究生 Shen Lin 已宣布證明 BB (3) = 21，不過(guò)布雷迪還是繼續(xù)證實(shí)了 Lin 的結(jié)果。
畢業(yè)后，布雷迪發(fā)現(xiàn)了新的非停止圖靈機(jī)種類(lèi)，并給它們起了形象的名字。
1966 年，他發(fā)現(xiàn)了一個(gè)在停止前運(yùn)行了 107 步的四規(guī)則圖靈機(jī)，并推測(cè)這可能是第四個(gè)忙碌海貍，并最終于 1974 年證明了沒(méi)有其他停止的機(jī)器能運(yùn)行更久。
這是四十多年來(lái)人類(lèi)所知的最后一個(gè)忙碌的海貍號(hào)碼
1982 年，第一次大規(guī)模尋找 BB (5)）的 Dortmund 競(jìng)賽正式舉辦，其中運(yùn)行時(shí)間最長(zhǎng)的一臺(tái)在超過(guò) 10 萬(wàn)步后停止。
1984 年，《科學(xué)美國(guó)人》對(duì)這項(xiàng)比賽的報(bào)道激發(fā)了新一代研究者的興趣，有一位研究者打破了舊紀(jì)錄，他發(fā)現(xiàn)的一臺(tái)機(jī)器在超過(guò) 200 萬(wàn)步后停止。
這一新紀(jì)錄也引來(lái)當(dāng)時(shí)的研究生 Heiner Marxen 和 Jürgen Buntrock，他們?cè)跇I(yè)余時(shí)間合作研究這個(gè)問(wèn)題，開(kāi)發(fā)了加速圖靈機(jī)模擬的數(shù)學(xué)技術(shù)。
盡管未能打破 200 萬(wàn)步的紀(jì)錄，但后來(lái)在 1989 年，Marxen 在一家公司工作時(shí)，使用一臺(tái)功能強(qiáng)大的新計(jì)算機(jī)重新啟動(dòng)了他的搜索程序，并意外地發(fā)現(xiàn)了一個(gè)在 4700 萬(wàn)步后停止的圖靈機(jī)。
2000 年代初，一位名叫 Georgi Ivanov Georgiev（化名 Skelet）的保加利亞計(jì)算機(jī)科學(xué)家非常接近這一目標(biāo)。
經(jīng)過(guò)兩年的不懈努力，他開(kāi)發(fā)了一個(gè)能夠識(shí)別非停止機(jī)器新種類(lèi)的計(jì)算機(jī)程序。盡管他的程序運(yùn)行了一周并留下了約 100 個(gè)未解決的圖靈機(jī)，但他手工分析后將名單減少到 43 個(gè)。
此后人們一直陷入不斷嘗試中。
最終確定 BB (5)
2022 年，研究生 Tristan Stérin 發(fā)起了“忙碌海貍挑戰(zhàn)”，這是一項(xiàng)在線(xiàn)合作，旨在最終確定 BB (5)。
在這之前，Stérin 決定在傳統(tǒng)方法的基礎(chǔ)上進(jìn)行調(diào)整，使用布雷迪的家譜方法，并計(jì)劃用獨(dú)立程序處理永遠(yuǎn)運(yùn)行的機(jī)器。
到 2021 年底，Stérin 編寫(xiě)了第一步的計(jì)算機(jī)程序，生成了大約 1.2 億臺(tái)可能的圖靈機(jī)列表。
為了幫助分析這些機(jī)器，Stérin 構(gòu)建了一個(gè)在線(xiàn)界面，使用“時(shí)空?qǐng)D”來(lái)可視化圖靈機(jī)的行為。
完成這些后，鑒于個(gè)人精力有限，他在偶然的情況下拉來(lái)了 Shawn Ligocki。
Ligocki 向團(tuán)隊(duì)介紹了封閉磁帶語(yǔ)言方法，這是一種 30 年前的技術(shù)，他將其應(yīng)用于當(dāng)前的忙碌海貍問(wèn)題。
他寫(xiě)了一篇博客文章介紹這項(xiàng)技術(shù)，但最初并不知道如何編寫(xiě)一個(gè)能涵蓋所有情況的程序。
然后，又一位 Justin Blanchard 加入了項(xiàng)目，他想出了如何做到這一點(diǎn)，但他的程序相對(duì)緩慢。
于是另外兩個(gè)貢獻(xiàn)者找到了讓它運(yùn)行得更快的方法，這一技術(shù)甚至可以處理前文提到的 43 個(gè)未解決圖靈機(jī)中的 10 個(gè)。
取得階段性成果后，BB (5) 終于迎來(lái)兩個(gè)關(guān)鍵突破。
第一個(gè)是 Skelet #1，它在可預(yù)測(cè)行為和混亂行為之間不斷交替，這種特性使得它非常難以分析和理解。
2023 年 3 月，Ligocki 和斯洛伐克貢獻(xiàn)者 Pavel Kropitz（不會(huì)說(shuō)英語(yǔ)，使用谷歌翻譯與團(tuán)隊(duì)其他成員交流），使用 Marxen 和 Buntrock（之前挑戰(zhàn) 200 萬(wàn)步記錄的兩位學(xué)生）30 年前的加速模擬技術(shù)的一個(gè)增強(qiáng)版，最終破解了 Skelet #1。
他們發(fā)現(xiàn) Skelet #1 在超過(guò)一萬(wàn)億步之后才進(jìn)入一個(gè)異常長(zhǎng)的重復(fù)周期，遠(yuǎn)超過(guò)一般無(wú)限循環(huán)在 1,000 步內(nèi)開(kāi)始重復(fù)的常規(guī)。
由于 Skelet #1 的行為極其奇怪，Ligocki 在將近五個(gè)月的時(shí)間里都不確定他們的證明結(jié)果是否正確。
后來(lái)，一位 21 歲自學(xué)成才的程序員（以“mei”為名）加入了團(tuán)隊(duì)，她通過(guò)學(xué)習(xí) Coq 證明助手，將團(tuán)隊(duì)的一些證明翻譯成 Coq 語(yǔ)言，提高了證明的嚴(yán)格性和可靠性。
第二個(gè)突破是 Skelet #17，研究者必須像破譯四層加密的秘密消息一樣，逐層解析其行為模式，才能證明該機(jī)器永遠(yuǎn)不會(huì)停止。
盡管研究生 Chris Xu 和其他社區(qū)貢獻(xiàn)者做了大量工作，但大多數(shù)證明尚未翻譯成 Coq。
直到 2023 年 4 月，一位名為 mxdys 的神秘新貢獻(xiàn)者加入，并在短短幾周內(nèi)完成了一個(gè) 40,000 行的 Coq 證明，證實(shí)了 BB (5) 的值。
mxdys 證明第五臺(tái)忙碌海貍在 4700 萬(wàn)步后停止，確認(rèn)了 Marxen 和 Buntrock 的發(fā)現(xiàn)。
Coq 專(zhuān)家 Yannick Forster 審查了證明，他激動(dòng)表示：
我仍然感到非常震驚。
故事仍未結(jié)束
BB (5) 終于確認(rèn)了，目前相關(guān)研究者正在起草一份學(xué)術(shù)論文，這將是一個(gè)補(bǔ)充 mxdys 的 Coq 證明的人類(lèi)可讀版本。
但是，BB (5) 已確認(rèn)，BB (6) 還會(huì)遠(yuǎn)嗎？
mxdys 和另一位貢獻(xiàn)者 Racheline 發(fā)現(xiàn)了一個(gè)六規(guī)則的圖靈機(jī)，其停機(jī)問(wèn)題與著名的數(shù)學(xué)難題“科拉茨猜想”相似。
為了避免讓大家頭疼，此處不再展開(kāi)這個(gè)猜想，各位看官只需要知道它非常難就行。
以至于著名理論計(jì)算機(jī)科學(xué)家 Scott Aaronson 發(fā)出感慨：
BB (5) 也許是我們所知道的最后一個(gè)忙碌的海貍號(hào)碼
嗯？這話(huà)有點(diǎn)耳熟，BB (4) 好像也是這樣說(shuō)的。
參考鏈接：
[1]https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/
[2]https://news.ycombinator.com/item?id=40857041
[3]https://scottaaronson.blog/?p=8088
本文來(lái)自微信公眾號(hào)：微信公眾號(hào)（ID：QbitAI），作者：一水，原標(biāo)題《40 年圖靈機(jī)難題被業(yè)余玩家攻破，陶哲軒：軟件輔助證明改變數(shù)學(xué)研究規(guī)則》
廣告聲明：文內(nèi)含有的對(duì)外跳轉(zhuǎn)鏈接（包括不限于超鏈接、二維碼、口令等形式），用于傳遞更多信息，節(jié)省甄選時(shí)間，結(jié)果僅供參考，IT之家所有文章均包含本聲明。