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