40 年以上もの間解かれていなかったコンピュータ パズル「ビジー ビーバー問題」が、アマチュア愛好家のグループによって解決されました。

数学の権威であるテレンス・タオ氏はこのニュースを共有し、満足感を表した。

これは、数学研究における共同作業において証明支援機能がいかに有用であるかを改めて証明しています。

コンピューター科学者のスコット・アーロンソン氏も、これを高く評価するブログ記事を書いています。

この発見は、1983 年以来のビーバーの多忙機能の研究における最も重要な進歩です。

具体的には、数十年にわたる努力の末、ついに5 番目の「ビジー ビーバー」チューリング マシンが発見されました。

BB(5) = 47,176,870 (5状態チューリングマシンは停止するまでに47,176,870個の「1」を書き込むことができる)

チューリング マシンは、0 と 1 を読み書きすることで無限の磁気テープ上で計算を実行する抽象的な計算モデルです。

40 年以上前、コンピューター科学者のグループがドイツのドルトムントで「ビジービーバー」チューリングマシンを見つけるコンテストを開催しました。

停止する前に最も多くの 1 を書き込むことができる特定のチューリング マシンを見つけます (これをビジー ビーバー数と呼びます)。

特定の状態で停止する前に最大 1 を書き込むことができるチューリング マシンを特定することで、計算理論の限界をより深く理解することができます。

4番目の忙しいビーバーの数は1974年に決定されて以来、5番目の忙しいビーバーの数の探索は未解決の問題のままです。

現在、世界中から集まった 20 人以上の協力者 (そのほとんどは伝統的な学歴を持たない) が、 Coq Proof Assistantと呼ばれるソフトウェアを使用して、47,176,870 という結果を得て、数学的証明に誤りがないことを確認しています。

この成果はコミュニティでたちまち話題となり、アイルランドのメイヌース大学のコンピューター科学者であるダミアン・ウッズ氏は驚きを表明した。

ボルトと同じように、彼らの速さに驚きました！

さて、半世紀ってそんなに早いのでしょうか？この問題はとてつもなく難しいとしか言​​いようがありません。

急がず、この集団が揚子江の波のように「5番目のビーバー」を捕まえる様子を見てください〜

「Busy Beaver」という用語がなぜ使われているのでしょうか?

この質問に答えるには、まずバイナリチューリングマシンの基本を理解する必要があります。

1936年、コンピュータサイエンスの父アラン・チューリングはチューリングマシンを提案しました。

これは、無限に長い紙テープ、読み取り/書き込みヘッド（紙テープ上の情報を読み書きできる）、一連の内部状態などの基本コンポーネントで構成されています。

チューリングマシンの動作は、表として表される一連の規則によって定義されます。表の各行は規則を表し、各列は読み取り/書き込みヘッドによって読み取られるシンボル（0または1）に対応します。

各ルールは、特定の状態で読み取り/書き込みヘッドが0または1を検出した場合に実行されるアクションを指定します。通常、アクションには以下が含まれます。

• 記号の書き込み: 現在のセルに書き込む記号を決定します (例: 0 を 1 に置き換えます)。
• 移動方向: 読み取り/書き込みヘッドが左に移動する、右に移動する、または静止したままになるかを決定します。
• 状態遷移: チューリング マシンの次の状態を決定します。

0と1の扱いに関するルールに加えて、チューリングマシンに実行を停止するタイミングを指示する特別なルールがあります。チューリングマシンがこの状態に入ると、すべての演算を停止します。これは「ゲームオーバー」と同等です（この状態は通常、状態集合にはカウントされません）。

ダウンタイムの問題に関しては、すでに調査で次のようなことが観察されています。

一部のチューリング マシンは比較的早く停止します (たとえば、この 3 つのルールを持つチューリング マシンは 11 ステップ後に停止します)。

しかし、他のものは簡単に検出できる無限ループに陥りました。

これはまた、チューリングが有名な「停止問題」を提唱するきっかけにもなりました。

チューリング マシンは、有限数のステップの後に動作を停止しますか、それとも無期限に実行されますか?

さらに彼は、あるマシンで機能する方法が別のマシンでも機能するかどうかは確実ではないため、ダウンタイムの問題に対する普遍的な解決策は存在しないと述べました。

数学者ティボール・ラドはこの結論に満足せず、結果として「ビジービーバーゲーム」を発明しました。

シャットダウン問題の本質をより単純な形にするために、ラドは次のような方法を提案した。

チューリング マシンを、それらが持つルールの数に応じてグループ化します。

たとえば、1 つのセットは 1 つのルールのみを持つすべてのチューリング マシンを表し、別のセットは 2 つのルールを持つすべてのチューリング マシンを表す、というようになります。

1962年、ラドーはこれらの限定的なチューリングマシンを用いて「ビジービーバーゲーム」を定義しました。ゲームプレイは以下の通りです。

1.グループを選択します。これにより、チューリング マシンのルールの数が決まります。

2.グループ内の各マシンに、初期状態がすべて 0 のテープを用意します。

3.これらの機械がどのように動作するか観察してください。機械によっては永久に動き続けるものもあれば、ある時点で停止するものもあるでしょう。

4.最終的に停止する機械の中には、すぐに停止するものもあれば、より多くの手順を必要とするものもあります。各グループには、最も長く稼働する機械が1台あります。この機械は「ビジービーバー」と呼ばれます。

5. n 個のルールを持つグループでは、「ビジービーバー」が停止するまでに実行するステップ数は、「ビジービーバー数」BB(n) と呼ばれます。

6.ゲームの目的は、これらのBB(n)の正確な値を決定することです。

ラドーはこの「極めて非効率的な」チューリング マシンに、興味深く説明的な名前「ビジービーバー」 (英語のことわざ「ビーバーのように忙しい」に由来) を付けました。

このゲームは最終的に、多数のプログラマーや数学愛好家を惹きつけ、試してみることになりました。

初期のカニ食者

当時オレゴン州立大学の数学大学院生だったアレン・ブレイディ（以下、ブレイディと略す）が初期の挑戦者の一人となった。

ゲームがリリースされる前に、人々はすでにBB(1) = 1、BB(2) = 6と判定しており、その時点で人々はBB(3)を克服しようとしていました。

ブレイディはBB(3)にも参加し、チューリングマシンの挙動をシミュレートするコンピュータプログラムを作成した。このプログラムは、初期挙動の類似性に基づいて、同じ数のルールを持つマシンを分類する「家系図」を構築した。

プログラムは、マシン間の動作の違いが顕著になった場合にのみ、系統樹を分岐させます。シミュレーションによって、ある分岐にあるマシンが停止するか無限ループに入ることが示された場合、プログラムはその分岐を刈り込み、無限に動作しないチューリングマシンを排除します。

プログラムを書くことは最初のステップに過ぎませんでした。ブレイディは、プログラムを実行するために十分に強力なコンピュータを見つける必要がありました。

1964年当時、これは決して容易な仕事ではありませんでした。最終的に彼は、90マイル離れた霊長類研究施設でSDS 920コンピュータを見つけました。

残念ながら、BB(3)の途中で、ラルドの大学院生であるシェン・リンがBB(3) = 21を証明したと発表したが、ブレイディはリンの結果を確認し続けた。

卒業後、ブレイディは新しいタイプのノンストップチューリングマシンを発見し、それらに説明的な名前を付けました。

1966年、彼は4つのルールを持つチューリングマシンを発見しました。このマシンは107ステップで停止し、 4番目のビジービーバーではないかと推測しました。そして1974年、彼は最終的に、停止したマシンの中でこれ以上長く動作できないマシンは他にないことを証明しました。

これは過去 40 年間で、最も活発に活動しているビーバーの個体数として知られている最後の個体です。

1982年に、BB(5)を探す最初の大規模なドルトムント競技会が公式に開催され、最も長く稼働していたマシンは10万ステップ以上を走った後に停止した。

1984年、サイエンティフィック・アメリカン誌がこの競技を報じたことで、新世代の研究者たちの関心が高まりました。ある研究者は、200万歩以上歩いた後に停止する機械を発見し、従来の記録を破りました。

この新しい記録は大学院生のハイナー・マルクセンとユルゲン・ブントロックの注目も集め、2人は空き時間にこの問題に協力し、チューリングマシンのシミュレーションを加速する数学的手法を開発した。

200万歩の記録を破ることはできなかったが、1989年、会社で働いていたマルクセン氏は、高性能な新型コンピュータで検索プログラムを再起動したところ、 4700万歩で停止したチューリングマシンを思いがけず発見した。

2000年代初頭、ブルガリアのコンピューター科学者、ゲオルギ・イワノフ・ゲオルギエフ（ペンネーム：Skelet）氏が、この目標達成にかなり近づきました。

2年間の精力的な努力の末、彼は新しいタイプのノンストップマシンを識別できるコンピュータプログラムを開発しました。彼のプログラムは1週間動作し、未解決のチューリングマシンが約100個残りましたが、彼はそれらを手作業で分析し、リストを43個にまで絞り込みました。

それ以来、人々は常に新しいことに挑戦してきました。

最終的にBB(5)が決定した。

2022年、大学院生のトリスタン・ステリンは、 BB(5)を完成させることを目的としたオンラインコラボレーションであるBusy Beaver Challengeを立ち上げました。

これに先立ち、ステリンはブレイディの系図的方法を使用して従来のアプローチに調整を加え、永続的に稼働するマシンを処理するために別のプログラムを使用することを計画しました。

2021年末までに、ステリンはコンピュータ プログラムの最初のステップを書き、約1億2000万通りのチューリング マシンのリストを生成しました。

これらのマシンの分析を支援するために、ステリンは「時空グラフ」を使用してチューリングマシンの動作を視覚化するオンライン インターフェイスを構築しました。

これらの任務を終えた後、彼は限られた個人的なエネルギーを考慮して、偶然ショーン・リゴッキを招き入れました。

リゴッキ氏は、30 年前の技術であるクローズド テープ言語アプローチをチームに導入し、それを現在の Busy Beaver 問題に適用しました。

彼はこの技術を紹介するブログ記事を書いたが、当初はあらゆる状況をカバーできるプログラムの書き方がわからなかった。

その後、別のジャスティン・ブランチャードがプロジェクトに参加し、やり方を理解しましたが、彼のプログラムは比較的遅いものでした。

その後、他の 2 人の貢献者が、さらに高速に実行する方法を発見しました。この手法は、前述の43 個の未解決チューリング マシンのうち 10 個を処理できるものでした。

初期の成功を収めた後、BB(5)は最終的に2つの重要なブレークスルーを達成しました。

1 つ目はSkelet #1です。これは予測可能な動作と混沌とした動作が絶えず切り替わるため、分析と理解が非常に困難です。

2023年3月、リゴツキ氏とスロバキアの貢献者パベル・クロピッツ氏（英語が話せず、チームの他のメンバーとのコミュニケーションにはGoogle翻訳を使用）は、マルクセン氏とバントロック氏（2人の学生、この2人は以前に200万歩の記録に挑戦していた）による30年前の高速化シミュレーション手法の強化版を使用して、ついにスケルトン1を解読した。

彼らは、スケルトン #1 が1 兆ステップ以上を経た後に異常に長い繰り返しサイクルに入り、 1,000 ステップ以内に繰り返しが始まる通常の無限ループをはるかに超えていることを発見しました。

スケルトン #1 の極めて奇妙な動作のため、リゴッキ氏は約 5 か月間、自分たちの証明が正しいかどうか確信が持てませんでした。

その後、独学でプログラミングを学んだ21歳のメイ（通称「メイ」）がチームに加わりました。彼女はCoq Proof Assistantを習得し、チームの証明の一部をCoq言語に翻訳することで、証明の厳密さと信頼性を向上させました。

2つ目のブレークスルーはスケルトン17でした。研究者たちは、この機械が決して止まらないことを証明するために、まるで4層に暗号化された秘密メッセージを解読するかのように、その動作を層ごとに分析する必要がありました。

大学院生の Chris Xu 氏と他のコミュニティ貢献者による広範な作業にもかかわらず、証明のほとんどはまだ Coq に翻訳されていません。

2023年4月には、 mxdysという謎の新しい貢献者が参加し、わずか数週間で4万行のCoq証明を完成させ、BB(5)の価値を確認しました。

mxdys は、5 番目のビジービーバーが4,700 万歩歩いた後に停止したことを証明し、Marxen と Buntrock の調査結果を裏付けました。

コックの専門家ヤニック・フォースターは証拠を検討し、興奮してこう語った。

まだとてもショックを受けています。

物語はまだ終わっていない。

BB(5)は最終的に確認され、研究者は現在、mxdysのCoq証明の人間が読めるバージョンとなる学術論文を執筆中です。

しかし、BB(5)は確認されているので、BB(6)はどれくらい離れているのでしょうか？

mxdys ともう一人の貢献者である Racheline は、有名な数学の問題であるコラッツ予想に類似した停止問題を持つ6 ルールのチューリング マシンを発見しました。

皆さんの頭を悩ませるのを避けるため、この推測についてはここでは詳しく説明しません。ただ、非常に難しいということだけは知っておいていただければと思います。

著名な理論計算機科学者スコット・アーロンソンは次のように述べています。

BB(5)は、私たちが知る限り、忙しいビーバー番号としては最後のものかもしれません。

ん？聞き覚えがあるような。BB(4)も同じことを言っていたような。