5番目のBusy Beaverで研究者らが計算の限界に迫る
(quantamagazine.org)- 世界中から20人以上が参加した Busy Beaver Challenge が、5規則チューリングマシンの Busy Beaver 数 BB(5)=47,176,870 を検証した
- 1989年にMarxenとBuntrockが見つけた、47,176,870ステップ後に停止するマシンが、実際に最も長く動作する 5規則停止マシン であることが確定した
- チームは、重複候補を減らす 系譜方式、非停止判定プログラム、Coq proof assistant を組み合わせて、数千万件の候補を処理した
- 最終結果は、mxdysがコミュニティの手法を統合した 40,000行のCoq証明 として完成し、InriaのCoq専門家Yannick Forsterがレビューした
- BB(6)では、Collatz conjecture に似た6規則マシン Antihydra が障壁として立ちはだかっており、BB(5)が人類が正確に知る最後のBusy Beaver数になる可能性もある
BB(5)が確定
- Busy Beaver Challenge チームが、BB(5)の正確な値 47,176,870 を検証した
- この値は、5個の規則を持つチューリングマシンのうち、停止するマシンが実行できる最大ステップ数を意味する
- 検証には Coq proof assistant が使われ、Coqは数学的証明が誤りなく構成されていることを認証した
- Santa Fe Institute の Cristopher Moore は、この作業の社会的・数学的エンジニアリングが印象的だと評価した
- Maynooth University の Damien Woods は、結果が出るまでの速さを「Usain Bolt territory」にたとえた
- BB(5)の具体的な値そのものより重要なのは、これが他の計算機科学分野への応用ではなく、計算不能性の境界 で得られた成果だという点にある
Busy Beaver問題と停止問題
- Busy Beaver問題は、一般的なプログラミング言語ではなく チューリングマシン を対象とする
- チューリングマシンは、無限のテープ上の0と1を読み書きし、headが1マスずつ移動しながら規則表に従って動作する
- 各規則は、現在読んでいる値が0か1かに応じて次の動作を指定する
- 値を書き換える、またはそのままにする
- 左または右に移動する
- 次に参照する規則を指定する
- 特殊な規則は、マシンがいつ停止するかを定める
- あるチューリングマシンが最終的に停止するか、永遠に動作し続けるかを一般的に判定する問題が 停止問題 である
- Alan Turing は、停止問題に一般解が存在しないことを証明した
- Busy Beaver探索は、すべてのマシンの停止性を一般的に解く代わりに、規則数が固定された有限集合の中で各マシンを分類する作業である
RadóのBusy Beaver game
- Tibor Radó は1962年の論文で、チューリングマシンを規則数ごとにまとめた Busy Beaver game を定義した
- 規則数がn個のすべてのチューリングマシンの集合では:
- いくつかのマシンは永遠に動作する
- いくつかのマシンは停止する
- 停止するマシンのうち最も長く動作するマシンが busy beaver である
- その実行ステップ数が BB(n) である
- BB(n)を確定するには、停止するすべてのマシンの実行時間を確認し、残るすべてのマシンが停止しないことを証明しなければならない
- 実行時間の測定は通常コンピュータシミュレーションで可能だが、非停止の証明は特定のマシンに対する停止問題を解くことに近い
- Busy Beaver Challenge の貢献者 Shawn Ligocki は、この作業を「未知の境界」で進めるものだと捉えている
BB(1)からBB(4)まで
- BB(1)=1 は容易に確認できる
- 最初の規則が0を読んだときに停止するようにすれば、最初のステップで止まる
- それ以外では、0で埋められたテープに沿って移動し続ける
- 規則が2個になるだけで6,000を超える異なるチューリングマシンが生まれ、規則3個では数百万個、規則4個では数十億個へと増える
- Allen Brady は、初期動作が同じマシンをまとめて重複を減らす 系譜方式 をコンピュータプログラムに統合した
- Shen Lin は Radó とともに BB(3)=21 を証明し、その結果は1965年に発表された
- Brady は1966年に107ステップ後に停止する4規則マシンを発見し、1974年にそれがBB(4)であることを証明した
- BB(4)はその後40年以上にわたり、人類が知っていた最後のBusy Beaver数だった
5番目のBusy Beaver探索
- 1984年のDortmund競争は、BB(5) を目指した最初の大規模な探索だった
- 5規則チューリングマシンはほぼ 17兆個 に達し、1ミリ秒に1個ずつ列挙しても500年以上かかる
- Dortmundの参加者たちが見つけた最も忙しいマシンは、100,000ステップ以上動作した後に停止した
- その後、ある研究者が200万ステップ以上動作するマシンを見つけた
- Heiner Marxen と Jürgen Buntrock は、チューリングマシンのシミュレーションを高速化する数学的手法を開発した
- Marxen は1989年、会社の強力な新型コンピュータで週末のあいだプログラムを走らせ、47,176,870ステップ 後に停止するマシンを発見した
- Buntrock が結果を再現し、2人は1990年初めに 論文 を発表した
- 実際にこのマシンは5番目のBusy Beaverだったが、残るすべてのマシンが停止しないことを証明するには、さらに30年以上を要した
Skeletと未解決マシン
- 2000年代初頭、ブルガリアの計算機科学者 Georgi Ivanov Georgiev は BB(5) に非常に近いところまで迫った
- Georgiev は2年間、毎日何時間もかけて非停止マシンを識別するプログラムを改良した
- 最終プログラムはコメントなしの高密度な 6,000行 のコードで、実行には1週間以上かかった
- このプログラムは約100台のチューリングマシンを未解決のまま残し、Georgiev は手作業の解析でそれを 43台 まで減らした
- Georgiev は2003年、その結果を Skelet というペンネームで オンライン に公開した
- この43台の難解なマシンは、彼のペンネームにちなんで Skelet machines と呼ばれるようになった
- Georgiev は、2年にわたる集中的な作業の末、新しいアイデアをもう生み出せないほど疲れ切っていたと語っている
Busy Beaver Challengeの協業構造
- Tristan Stérin は2022年に Busy Beaver Challenge を開始した
- プロジェクトはオンライン協業方式で進められ、伝統的な学術資格を持たない貢献者も多く含む、20人以上の国際コミュニティへと成長した
- Stérin は、BB(5)を確定するには文書化され再現可能な証明が必要だと考えた
- Georgiev のプログラムは高度だったが、他の研究者がレビューするのは難しかった
- Stérin は既存のアプローチをもとに作業を分担した
- Brady の系譜方式で重複マシンを除去する
- 47,176,870ステップ以内に停止するマシンを特定する
- 永遠に動作するマシンは、それぞれの証明手法を含む独立したプログラムで処理する
- 2021年末に作られた第1段階のプログラムは、BB(5)を決定するのに十分な約 1億2,000万台 のチューリングマシンのリストを生成した
- そのうち約4分の1は Marxen と Buntrock のマシンより先に停止し、8,800万台 が引き続き検討対象として残った
- Stérin は、マシンの動作を0と1の2次元グリッドで示す 時空間ダイアグラム のオンラインインターフェースも構築した
閉テープ言語と協業の加速
- Shawn Ligocki は2022年に Busy Beaver Challenge に加わり、Marxen が作った 閉テープ言語法 を復活させた
- この方法は、チューリングマシンのテープ上のパターンを使って、マシンが停止しないことを示す統一的な数学的枠組みを提供する
- Ligocki はこの手法を紹介する ブログ記事 を書いたが、あらゆるケースを網羅するプログラムの作り方は分かっていなかった
- Justin Blanchard がプロジェクト参加後にこれを実装し、さらに別の2人の貢献者が実行速度を大きく引き上げた
- 数カ月のうちに、閉テープ言語法はチームで最も強力な道具の1つになった
- この手法は、Georgiev が残した43台の Skelet machine のうち 10台 も処理できた
- Ligocki は、この成果は1人だけの貢献では生まれなかっただろうと見ている
Skelet #1、Skelet #17、そしてCoq
- Skelet #1 は、予測可能な段階とカオス的な段階を交互に示すマシンだった
- 2023年3月、Ligocki と Pavel Kropitz は、Marxen と Buntrock の30年前の高速化シミュレーション手法を強化して Skelet #1 を解析した
- Skelet #1 は、1兆×1兆ステップを超えて初めて反復周期に入り、その反復周期は 80億ステップ超 と長大だった
- 21歳の独学プログラマ mei は Coq を学んだ後、Busy Beaver Challenge のいくつかの証明を Coqに翻訳 した
- mei は Ligocki と Kropitz による Skelet #1 の非停止証明も Coq に移し、その結果をさらに確かなものにした
- Skelet #17 は、Chris Xu が突破口を開いたもう1つの難解なマシンだった
- Xu の 証明 は見事だったが、Coq が要求する厳密な形式へ移すのが難しい数学的直観を含んでいた
- チームは、「6カ月間プログラムを走らせればよい」という類いの証明ではなく、合理的に再現可能な証明を求めていた
40,000行のCoq証明
- 2024年4月、mxdys というペンネームだけで知られる新たな貢献者が、Coq証明の完成作業に加わった
- mxdys の所在地や個人的背景は、チームにも分かっていない
- 5月10日、mxdys はDiscordに「The Coq proof of BB(5) is finished.」と投稿した
- mxdys は数週間のうちに、コミュニティの手法と成果を統合して単一の 40,000行のCoq証明 を完成させた
- この証明は Coq-BB5 リポジトリで公開されている
- Inria の Coq 専門家 Yannick Forster はこの証明をレビューし、形式化は容易な作業ではなかったと評価した
- その結果、Marxen と Buntrock が30年以上前に見つけた 47,176,870ステップのマシン が、実際に5番目の Busy Beaver であることが確定した
- Georgiev は、この問題が自分の生きているうちに解かれるとは思っていなかったと語った
- Allen Brady は、証明完成の1カ月前にあたる2024年4月21日、90歳で死去した
BB(6)と次の境界
- Busy Beaver Challenge の貢献者たちは、この結果を説明する正式な学術論文の準備を始めた
- 論文は、mxdys の Coq 証明を人間が読める証明で補う形になる予定だ
- 一部のチームメンバーは、次のBusy Beaverへと移った
- mxdys と Racheline は、BB(6)で乗り越えるのが難しそうな障壁を発見した
- この障壁は、Collatz conjecture に似た停止問題を持つ6規則マシンである
- このマシンは Antihydra と呼ばれている
- チューリングマシンと Collatz conjecture のつながりは Pascal Michel の1993年の論文までさかのぼるが、Antihydra は数学における概念的突破なしには解けそうにない最小のマシンに見える
- Scott Aaronson は、BB(5)が人類が知る最後の Busy Beaver 数になる可能性があると見ている
- 一部の貢献者たちは Busy Beaver の変種問題を引き続き扱う予定だが、参加者全員が同じ方向に残るわけではない
- Stérin は Busy Beaver Challenge を通じてオンライン協業研究の有効性を確信し、数学の他分野の協業プロジェクトを支援するソフトウェアツールを開発したいと考えている
1件のコメント
Hacker News の意見
Scott Aaronson がこの結果について書いたコメントがある: https://scottaaronson.blog/?p=8088
それから「leisure-class beavers」に関しては、今年初めの大きなスレッドもある:
https://news.ycombinator.com/item?id=40453221
https://news.ycombinator.com/item?id=38113792
https://news.ycombinator.com/item?id=37910297
もともと ビジービーバー問題 には多くの変種があり、その一つがラムダ計算で定義した関数型ビジービーバーである [1]
状態数ではなくビット単位のプログラムサイズを測るため、より多くの値を決定でき、これまでチューリングマシンでは 6 個だけなのに対し、こちらは 37 個まで出ている。既知の最大値と Graham's Number を超える値との間隔も、プログラム 13 ビットにすぎない。近い変種 [2] は Kolmogorov 複雑性で直接表現でき、Mikhail Andreev は [3] 情報理論への応用においてこれが重要だと見ている
[1] https://oeis.org/A333479
[2] https://oeis.org/A361211
[3] https://arxiv.org/pdf/1703.05170
https://oeis.org/A141475 は見つけたが、ここでは 5 に対して 27 兆と出ている
その定義を説明した動画を見た記憶がある
エリートテック企業で、私が見た誰よりも速く IC の職位を駆け上がった、ものすごく、理解しがたいほど賢いエンジニアと数年一緒に働いた
彼は数年前に退職し、今後の計画を聞いたところ ビジービーバー問題 を研究すると言っていた。記事で BB(5) の形式証明を仕上げた匿名貢献者 mxdys がその人なのか気になるが、おそらく永遠に分からないだろう
見返りが何なのか分からないし、それほど優れた知性なら、世界を改善することにもっと関係のある問題を解いてほしいと思う
Tibor Radó の元のビジービーバー論文「On Non-Computable Functions」は、実際かなり読みやすくて面白い
追加注釈付きの現代版はここにある: https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
ここで目立つ点は、証明が Coq 証明 であることだ
既知の証明を定理証明支援系に移したのではなく、最初から定理証明支援系で実装された重要な証明としては初めてなのか気になる。以前にもコンピュータ支援証明はあったが、四色定理や Kepler 予想は後になって形式検証環境へ移された
主な問題は、判定器と手作業の証明が整理されておらず、やや疑わしかった点だ。特に Skelet #1 は最終パターンまで加速するために専用プログラムが必要で [0]、Skelet #17 では Xu が非停止を証明するのに密度の高い 7 ページの推論を書く必要があった [1]。Coq による全体証明は、これらの結果に必要だった信頼性を与えてくれる
[0] https://www.sligocki.com/2023/03/13/skelet-1-infinite.html
[1] https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/18...
https://github.com/ccz181078/Coq-BB5/blob/main/BB52Theorem.v
https://en.m.wikipedia.org/wiki/Four_color_theorem
「形式検証環境」が正確に何を意味するのか理解できていないのかもしれないが、四色定理は最初からコンピュータで証明されたものだと理解している。Kempe の元の証明の試みには欠陥があったが、その後の証明で使われた基本的な道具の一部を提供し、最終的に定理はコンピュータで証明されたようだ
このビジービーバーは 1990 年に発見され、サイズ 5 のすべてのマシンもその直後に列挙された可能性が高い
チームに祝意を表します。これで空テープ基準の 5状態2記号チューリングマシン プログラムの停止問題が解決されたことになります。
同じ手法を2状態4記号の場合に適用してみた人がいるのか気になります。一般に記号のほうが状態より強力ではありますが、その程度ならおそらく扱えそうで、意外な結果もあるかもしれません。6状態2記号と2状態5記号はいずれも扱いが難しそうで、ひょっとすると証明可能なほど難しいのかもしれません。ついでに、人間は心の目や脳内の量子力学のようなもので停止問題の答えを直観できる、という荒唐無稽ながら奇妙に広く流布している考えがありますが、当然ながら今回の証明にはそうしたものは関わっていません。
現在使っている判定器だけでも、2×4の残りのケースがすべて非停止であることを証明するには十分だと理解しています。したがって、判定器の設計に大きな誤りがなければ、現在のチャンピオンから Σ(2,4) = 2,050、S(2,4) = 3,932,964 が得られます。結果が一か所に整理されていないだけです。
2×5にはHydraがあり、6×2にはAntihydraがありますが、両者は開始点と停止条件が違うだけで同じ反復を計算します。標準的な予想は、Mahlerの3/2問題に関連して、この反復が mod 2 で一様分布するというもので、その予想を証明できれば、0と1の累積比率に対する上限と下限が得られ、2つのマシンが非停止であることをほぼ確実に証明できます。もちろん、既知の証明方法はありません。
Alephという論理理論ベースの証明生成器を使い、その時点ではすでに1,500年前から、ZFCではBB(18)を確立できないことが知られていました。2024年と比べると、Alephが使われるずっと前のどんなプログラムも、理論上でさえBB(18)を解くための総当たり証明検査には使えませんでした。これは、今日の私たちがZFC証明を列挙して検査することで、理論上はBB(??)を解けることと対照的です。
「人間が停止問題の答えを直観する」という立場は、こういう意味です。私の知る限り、このような未来史が不可能だという強い理論的理由はありません。そしてビジービーバーは計算不可能なので、必要なプログラムを作るには人間が新しい理論を開発しなければなりませんでした。結果の功績は何かに帰されるべきであり、当時そのプログラムは存在しなかったので、計算に帰すことはできません。
長さ5のすべての非停止プログラムが、たまたま全て 非停止であることを証明可能 だったのか気になります。
「Σ(5) = 1,915 および S(5) = 2,358,064 という事実は決して証明されないだろう。あるいは、より大きな下限が見つかったなら、その新しい値をこの予測に代入してもよい。」
理由は、自然が5状態の保留マシンの中に、Goldbach予想と同じくらい捉えにくい問題を少なくとも一つ仕込んでいる可能性が高い、というものでした。別の言い方をすれば、私たちが認識できる能力を超えた非停止の再帰パターンが存在する可能性が高いということです。幸いこの予測は現実にはなりませんでしたが、余分な状態が一つ違うだけでした。
[0] Allen Brady, "The Busy Beaver Game and the Meaning of Life", in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey, Oxford University Press, 1988, pp. 259–277. This chapter can also be found in the 2nd ed., Springer, 1995, pp. 237–254.
実用的な意味なら、他の人たちがすでに答えています。数学的な意味なら、BB(5)が決定不能だったとしたらかなり驚きだったと思います。5状態2記号は、決定不能な振る舞いをエンコードするには小さすぎるからです。
ただし不完全性定理の結果として、標準的な数学ではBB(n)の値を証明できないような n は必ず存在します。ここ数年、複数の人がそうした n を探し、どこまで低くできるかを研究しており、現在の記録[0]は745です。この記録はおそらくさらに下げられると思いますが、それでも私たちが知っている最大値5と、分からないと分かっている最小値745との間には大きな隔たりがあります。
[0] 「標準的な数学」とは何か気になるかもしれないので付け加えると、これはZFCとPAの両方についての現在の記録です。ですから、少なくともPAについてはさらに下げることが可能なはずに思えます。これまでのところ、PAでZFCよりよい方法は見つかっていないようですが、当然可能なはずではないでしょうか。
「わずか4日前、mxdysとRachelineという別の貢献者は、BB(6)について越えがたいと思われる壁を発見した。停止問題が、扱いにくいことで有名な数学問題であるCollatz予想に似ている6規則マシンである。チューリングマシンとCollatz予想のつながりは、数学者Pascal Michelの1993年の論文にまでさかのぼるが、新たに発見された『Antihydra』というマシンは、数学上の概念的ブレークスルーなしには解けそうにない最小のマシンである。」
個人プロジェクトで 切断在庫問題（https://en.wikipedia.org/wiki/Cutting_stock_problem）を解くプログラムを書いたことがあります。
在庫には /---/、/---|、|---| という形の部材の切断が含まれており、45度カットで材料を無駄にしたくなかったため、既存のプログラムを使えなかった、あるいは使いたくありませんでした。BradyがBB(4)探索を最適化するために、差が重要でない探索部分木を刈り込んだという説明は、私が自分のプログラムを高速化したときにやったこととかなり似ていて興味深いです。
Scott Aaronsonのブログ記事によると、5状態チューリングマシン は16,679,880,978,201個あるそうです。
このうち何パーセントが停止するのか分かっているのか気になります。追記: n状態チューリングマシンの数は (4n + 1)^(2n) です。気になっていた分析に近い、小さい n 向けの資料を見つけました: https://github.com/LukasKalbertodt/beaver
bbchallenge.org のサイトでは見つけられませんでしたが、すべてのマシンは分類されています。
総合すると、証明はかなり短い部類です。空白とコメントを含めて Coq 19,000行です
私の経験では、従来型の論文にコンパイルすれば Coq 版よりずっと短くなると思います。もちろん証明の長さが難易度や複雑さの尺度になるわけではありませんが、非常に大まかな目安としては使えます
人間の知識の限界を語るとき、証明可能ではあるものの複雑すぎてどんな人間にも理解できない定理をよく思い浮かべます。おそらく私たちが持つ最も複雑な証明は 有限単純群の分類でしょう。数千〜数万ページに及び、地球上でその全体を完全に理解している人はほとんどいないか、まったくいない可能性があります
記事で述べられているように、BB(6) は決定不能かもしれません。しかし、数百万ページに及ぶ証明があり、人類の手の届かないところにある可能性もあります