40多年的計算機(jī)難題——忙碌海貍難題，被一群業(yè)余愛好者攻破了！

數(shù)學(xué)大佬陶哲軒轉(zhuǎn)發(fā)了這一消息，并欣慰表示：

這再一次體現(xiàn)了證明助手對于數(shù)學(xué)研究的協(xié)作是多么有用。

計算機(jī)科學(xué)家Scott Aaronson為此還寫了一篇博文，并大肆贊賞：

這個發(fā)現(xiàn)是自1983年以來，忙碌海貍函數(shù)研究中最重要的進(jìn)展。

具體而言，人們歷經(jīng)數(shù)十年努力，終于找到了第五個“忙碌海貍”圖靈機(jī)：

BB(5) =47,176,870（5狀態(tài)圖靈機(jī)，能在停下來之前寫下47,176,870個“1”）

圖靈機(jī)是一種抽象的計算模型，通過讀取和寫入0和1在無限磁帶上進(jìn)行計算。

早在40多年前，一群計算機(jī)科學(xué)家在德國多特蒙德舉行競賽，尋找“忙碌海貍”圖靈機(jī)。

找出一個特定的圖靈機(jī)，在它停止之前能夠?qū)懴伦疃嗟?（我們稱之為忙碌海貍數(shù)）。

通過找出特定狀態(tài)下能在停止前寫下最多1的圖靈機(jī)，我們能更好地理解計算理論的邊界。

自從1974年確定了第四個忙碌海貍數(shù)后，尋找第五個成了懸而未決的問題。

而現(xiàn)在，來自世界各地的20多名貢獻(xiàn)者（其中大多數(shù)人沒有傳統(tǒng)的學(xué)術(shù)資格） ，使用一款名為Coq證明助手的軟件獲得了結(jié)果——47,176,870，該軟件證實數(shù)學(xué)證明沒有錯誤。

這一成就瞬間令社區(qū)沸騰，其中愛爾蘭梅努斯大學(xué)計算機(jī)科學(xué)家Damien Woods驚嘆：

就像博爾特一樣，我很驚訝他們的速度如此之快！

嗯，快半個世紀(jì)過去了還算快？只能說這個問題雀食有億點難。

別著急，且看這群人如何長江后浪推前浪抓住“第5只海貍”~

為什么提出“忙碌海貍”？

要回答這個問題，首先需要簡單了解一下二進(jìn)制圖靈機(jī)。

1936年，計算機(jī)科學(xué)之父艾倫·圖靈提出了圖靈機(jī)——

由一個無限長的紙帶，一個讀寫頭（可以讀取和寫入紙帶上的信息），以及一組內(nèi)部狀態(tài)等基本部分組成。

圖靈機(jī)的行為由一組規(guī)則定義，這些規(guī)則可以想象成一張表。表中的每行代表一個規(guī)則，每列對應(yīng)讀寫頭讀取到的符號（0或1）。

每條規(guī)則指定了在特定狀態(tài)下，讀寫頭遇到0或1時應(yīng)該執(zhí)行的操作。操作通常包括：

• 寫入符號：決定在當(dāng)前單元格寫入什么符號（例如，將0替換為1）。
• 移動方向：決定讀寫頭是向左移動、向右移動還是保持不動。
• 狀態(tài)轉(zhuǎn)換：決定圖靈機(jī)的下一個狀態(tài)是什么。

除了處理0和1的規(guī)則外，還有一條特殊規(guī)則告訴圖靈機(jī)何時停止運行。當(dāng)圖靈機(jī)進(jìn)入這個狀態(tài)時，它就不再執(zhí)行任何操作，相當(dāng)于“比賽結(jié)束”（這種狀態(tài)一般不計算在狀態(tài)集合里）。

而就在停機(jī)問題上，已經(jīng)有研究觀察到：

一些圖靈機(jī)會相對較快地停止（比如這臺three-rule圖靈機(jī)在11步后停止）

其他的則陷入了很容易發(fā)現(xiàn)的無限循環(huán)

這也啟發(fā)圖靈提出了著名的“停機(jī)問題”：

圖靈機(jī)是否會在有限的步驟后停止運行，或者它是否會無限期地運行下去？

他還進(jìn)一步提到，停機(jī)問題沒有通用的解決方案，因為人們永遠(yuǎn)無法確定適用于一臺機(jī)器的方法是否也適用于另一臺機(jī)器。

對于這個結(jié)論，數(shù)學(xué)家Tibor Radó（以下簡稱拉多）不太滿意，并由此發(fā)明了“忙碌的海貍游戲”。

為了將停機(jī)問題的本質(zhì)提煉成更簡單的形式，拉多提出了一種方法——

將圖靈機(jī)根據(jù)它們擁有的規(guī)則數(shù)量進(jìn)行分組。

例如，一組代表所有只有一條規(guī)則的圖靈機(jī)，另一組代表所有有兩條規(guī)則的圖靈機(jī)，依此類推。

1962年，拉多利用這些有限的圖靈機(jī)組定義了“忙碌海貍游戲”。游戲的玩法是：

1.選擇一個組，即確定你的圖靈機(jī)將擁有的規(guī)則數(shù)量。

2.為組中的每臺機(jī)器提供一個初始狀態(tài)全是0的磁帶。

3.觀察這些機(jī)器的運行。一些機(jī)器可能會無限期地運行下去，而其他的則會在某個時刻停止。

4.在那些最終停止的機(jī)器中，有的會很快停止，有的則需要更多步驟。每個組中會有一個運行時間最長的機(jī)器，這臺機(jī)器被稱為“忙碌海貍”。

5.在有n條規(guī)則的組中，這臺“忙碌海貍”在停止之前所執(zhí)行的步數(shù)就是所謂的“忙碌海貍數(shù)”BB(n)。

6.游戲的目標(biāo)是確定這些BB(n)的確切值。

拉多給這樣“極度低效”的圖靈機(jī)取了一個有趣且形象的名字：忙碌海貍（Busy Beaver，取自英語中的諺語 as busy as a beaver）。

而這個游戲也最終引來一眾程序員和數(shù)學(xué)愛好者的瘋狂試玩。

早期吃螃蟹的人

Allen Brady（以下簡稱布雷迪），當(dāng)時的俄勒岡州立大學(xué)數(shù)學(xué)研究生，成了早期挑戰(zhàn)者之一。

在游戲推出前，人們已經(jīng)確定了BB(1) = 1，BB(2) = 6，當(dāng)時人們正嘗試攻克BB(3)。

布雷迪也投身BB(3)，他編寫了計算機(jī)程序來模擬圖靈機(jī)的行為，這個程序構(gòu)建了一種“家譜”，根據(jù)圖靈機(jī)初始行為的相似性，對具有相同規(guī)則數(shù)量的機(jī)器進(jìn)行分類。

程序只在機(jī)器之間行為差異變得重要時才將家譜樹分成多個分支。如果模擬顯示某條分支上的機(jī)器會停止或進(jìn)入無限循環(huán)，程序就會剪掉這個分支，排除那些不會無限運行下去的圖靈機(jī)。

編寫程序只是第一步，布雷迪需要找到足夠強(qiáng)大的計算機(jī)來運行它。

在1964年，這不是一件容易的事。最終，他在90英里外的靈長類動物研究實驗室找到了一臺SDS 920計算機(jī)。

只可惜BB(3)進(jìn)行到一半，拉多的研究生Shen Lin已宣布證明BB(3) = 21，不過布雷迪還是繼續(xù)證實了Lin的結(jié)果。

畢業(yè)后，布雷迪發(fā)現(xiàn)了新的非停止圖靈機(jī)種類，并給它們起了形象的名字。

1966年，他發(fā)現(xiàn)了一個在停止前運行了107步的四規(guī)則圖靈機(jī)，并推測這可能是第四個忙碌海貍，并最終于1974年證明了沒有其他停止的機(jī)器能運行更久。

這是四十多年來人類所知的最后一個忙碌的海貍號碼

1982年，第一次大規(guī)模尋找BB(5)）的Dortmund競賽正式舉辦，其中運行時間最長的一臺在超過10萬步后停止。

1984年，《科學(xué)美國人》對這項比賽的報道激發(fā)了新一代研究者的興趣，有一位研究者打破了舊紀(jì)錄，他發(fā)現(xiàn)的一臺機(jī)器在超過200萬步后停止。

這一新紀(jì)錄也引來當(dāng)時的研究生Heiner Marxen和 Jürgen Buntrock，他們在業(yè)余時間合作研究這個問題，開發(fā)了加速圖靈機(jī)模擬的數(shù)學(xué)技術(shù)。

盡管未能打破200萬步的紀(jì)錄，但后來在1989年，Marxen在一家公司工作時，使用一臺功能強(qiáng)大的新計算機(jī)重新啟動了他的搜索程序，并意外地發(fā)現(xiàn)了一個在4700萬步后停止的圖靈機(jī)。

2000年代初，一位名叫Georgi Ivanov Georgiev（化名Skelet）的保加利亞計算機(jī)科學(xué)家非常接近這一目標(biāo)。

經(jīng)過兩年的不懈努力，他開發(fā)了一個能夠識別非停止機(jī)器新種類的計算機(jī)程序。盡管他的程序運行了一周并留下了約100個未解決的圖靈機(jī)，但他手工分析后將名單減少到43個。

此后人們一直陷入不斷嘗試中。

最終確定BB(5)

2022年，研究生Tristan Stérin發(fā)起了“忙碌海貍挑戰(zhàn)”，這是一項在線合作，旨在最終確定BB(5)。

在這之前，Stérin決定在傳統(tǒng)方法的基礎(chǔ)上進(jìn)行調(diào)整，使用布雷迪的家譜方法，并計劃用獨立程序處理永遠(yuǎn)運行的機(jī)器。

到2021年底，Stérin編寫了第一步的計算機(jī)程序，生成了大約1.2億臺可能的圖靈機(jī)列表。

為了幫助分析這些機(jī)器，Stérin構(gòu)建了一個在線界面，使用“時空圖”來可視化圖靈機(jī)的行為。

完成這些后，鑒于個人精力有限，他在偶然的情況下拉來了Shawn Ligocki。

Ligocki向團(tuán)隊介紹了封閉磁帶語言方法，這是一種30年前的技術(shù)，他將其應(yīng)用于當(dāng)前的忙碌海貍問題。

他寫了一篇博客文章介紹這項技術(shù)，但最初并不知道如何編寫一個能涵蓋所有情況的程序。

然后，又一位Justin Blanchard加入了項目，他想出了如何做到這一點，但他的程序相對緩慢。

于是另外兩個貢獻(xiàn)者找到了讓它運行得更快的方法，這一技術(shù)甚至可以處理前文提到的43個未解決圖靈機(jī)中的10個。

取得階段性成果后，BB(5)終于迎來兩個關(guān)鍵突破。

第一個是Skelet #1，它在可預(yù)測行為和混亂行為之間不斷交替，這種特性使得它非常難以分析和理解。

2023年3月，Ligocki和斯洛伐克貢獻(xiàn)者Pavel Kropitz（不會說英語，使用谷歌翻譯與團(tuán)隊其他成員交流），使用Marxen和Buntrock（之前挑戰(zhàn)200萬步記錄的兩位學(xué)生）30年前的加速模擬技術(shù)的一個增強(qiáng)版，最終破解了Skelet #1。

他們發(fā)現(xiàn)Skelet #1在超過一萬億步之后才進(jìn)入一個異常長的重復(fù)周期，遠(yuǎn)超過一般無限循環(huán)在1,000步內(nèi)開始重復(fù)的常規(guī)。

由于Skelet #1的行為極其奇怪，Ligocki在將近五個月的時間里都不確定他們的證明結(jié)果是否正確。

后來，一位21歲自學(xué)成才的程序員（以“mei”為名）加入了團(tuán)隊，她通過學(xué)習(xí)Coq證明助手，將團(tuán)隊的一些證明翻譯成Coq語言，提高了證明的嚴(yán)格性和可靠性。

第二個突破是Skelet #17，研究者必須像破譯四層加密的秘密消息一樣，逐層解析其行為模式，才能證明該機(jī)器永遠(yuǎn)不會停止。

盡管研究生Chris Xu和其他社區(qū)貢獻(xiàn)者做了大量工作，但大多數(shù)證明尚未翻譯成Coq。

直到2023年4月，一位名為mxdys的神秘新貢獻(xiàn)者加入，并在短短幾周內(nèi)完成了一個40,000行的Coq證明，證實了BB(5) 的值。

mxdys證明第五臺忙碌海貍在4700萬步后停止，確認(rèn)了Marxen和Buntrock的發(fā)現(xiàn)。

Coq專家Yannick Forster審查了證明，他激動表示：

我仍然感到非常震驚。

故事仍未結(jié)束

BB(5)終于確認(rèn)了，目前相關(guān)研究者正在起草一份學(xué)術(shù)論文，這將是一個補(bǔ)充mxdys的Coq證明的人類可讀版本。

但是，BB(5)已確認(rèn)，BB(6)還會遠(yuǎn)嗎？

mxdys和另一位貢獻(xiàn)者Racheline發(fā)現(xiàn)了一個六規(guī)則的圖靈機(jī)，其停機(jī)問題與著名的數(shù)學(xué)難題“科拉茨猜想”相似。

為了避免讓大家頭疼，此處不再展開這個猜想，各位看官只需要知道它非常難就行。

以至于著名理論計算機(jī)科學(xué)家Scott Aaronson發(fā)出感慨：

BB(5)也許是我們所知道的最后一個忙碌的海貍號碼

嗯？這話有點耳熟，BB(4)好像也是這樣說的。