💻 computer science

Determination of the fifth Busy Beaver value

この論文は、Coq 証明支援系を用いて 5 状態のチューリングマシンを網羅的に解析し、約 40 年ぶりにビジー・ビーバー値 $S(5)$ が 47,176,870 であることを初めて数学的に証明・検証したことを報告しています。

原著者： The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev, Matthew L. House, Rachel Hunter, Iijil, Maja Kądziołka, Pavel Kropitz, Sha

公開日 2026-03-24

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev, Matthew L. House, Rachel Hunter, Iijil, Maja Kądziołka, Pavel Kropitz, Shawn Ligocki, mxdys, Mateusz Naściszewski, savask, Tristan Stérin, Chris Xu, Jason Yuen, Théo Zimmermann

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

🐻 忙しいカバとは？（ゲームのルール）

まず、この研究の対象である「忙しいカバ」ゲームを理解しましょう。

想像してください。**「ルールがシンプルで、紙（テープ）とペン（ヘッド）しかない小さなロボット」**がいます。
このロボットは、最初、真っ白な紙（すべて 0 が書かれている状態）に立ちます。
ロボットには「状態（A, B, C...）」というスイッチがあり、紙の数字を見て「書き換える」「右へ動く」「左へ動く」「次の状態へ移る」という命令に従って動き続けます。

「忙しいカバ」のゴールは：
「5 つのスイッチ（状態）しか持っていないロボットの中で、最も長く動き回り、最後に止まる（ハルティングする）ロボットを見つけること」です。

止まらずに永遠に動き続けるロボットは「負け」。
止まった瞬間、紙に書かれた「1」の数が多ければ多いほど、そのロボットは「カバ（熊）」として優秀とされます。
止まるまでの「ステップ数（動きの数）」も記録されます。

これまで、スイッチが 1 つ、2 つ、3 つ、4 つのロボットについては、どれが最強かが分かっていました。しかし、「スイッチが 5 つ」のロボットについては、どれが最強か、そしてその最強ロボットが何歩で止まるかが、40 年以上も謎でした。

🕵️‍♂️ 解決への挑戦：なぜこんなに大変だったのか？

スイッチが 5 つのロボットは、組み合わせの数が約 16 兆通りもあります。
これを一つずつ試すのは、人類の歴史が始まってからずっと計算し続けても終わらないほど膨大です。

さらに、難しいのは**「止まらないロボット」**の判定です。
「このロボットは永遠に動き続けるのか？」と判断するには、無限の時間を待つ必要があります。しかし、数学的には「止まらないこと」を証明するのは、ゴールドバッハの予想（未解決の数学問題）やリーマン予想のような難問と同じレベルの難しさを持つことがあります。

つまり、「止まるロボット」を見つけるのは簡単だが、「止まらないロボット」を証明するのは、数学の限界に挑むような難しさだったのです。

🤝 解決の鍵：「bbchallenge」という巨大な協力プロジェクト

この難問を解決したのが、**「bbchallenge（ビービーチャレンジャー）」**という、世界中のボランティアが集まったオンラインコミュニティです。

どんな人たちが？ 大学教授もいれば、学生、エンジニア、趣味のプログラマーまで。年齢も国籍もバラバラで、ほとんどがリアルでは会ったことがない人々です。
どうやって？ 彼らは「デシダー（判定機）」という、ロボットが止まるかどうかを判定するアルゴリズム（プログラム）を次々と開発しました。
- 例えば、「あるパターンを繰り返しているなら、それは永遠に止まらない」と見抜く「ループ検知」。
- 「特定の文字の並びが繰り返されるなら、止まらない」と見抜く「n-gram 解析」。
- 「有限オートマトン（簡単な機械）を使って、複雑な動きを簡略化して判定する」という高度な技術など。

彼らは 2 年間、Discord というチャットで日夜議論し合い、何百万ものロボットを判定するプログラムを共有・改良し続けました。

🛡️ 決定打：Coq（コック）という「完璧な証明者」

ここが今回の最大の驚きです。
コミュニティが作ったプログラムで「止まらない」と判定されたロボットたちを、**「Coq（コック）」という「証明を厳密にチェックする AI 助手（証明支援ツール）」**にすべて入力しました。

Coq の役割： 人間が書いたプログラムや証明には、必ずミスや勘違いが含まれる可能性があります。しかし、Coq は「この証明は数学的に 100% 正しいか？」を、一つ一つの論理ステップを厳密にチェックします。
今回の成果： Coq は、1 億 8,100 万個以上のロボットを、一つ一つチェックし、「止まる」「止まらない」をすべて証明しました。
- 止まるロボット：4,800 万個以上（その中で最も長く動いたのが優勝者）。
- 止まらないロボット：1 億 3,300 万個以上（それぞれが「止まらない」ことを数学的に証明）。

これにより、**「スイッチ 5 つのロボットの中で、最も長く動いたのは、47,176,870 歩で止まるこのロボットだ！」という事実が、「数学的に疑いのない形」**で証明されたのです。

🏆 結果と意味

新しい記録の確定：
5 つのスイッチを持つロボットの最大ステップ数は、47,176,870 歩であることが確定しました。
また、紙に書かれた「1」の数の最大値も4,098であることが分かりました。
40 年ぶりの新発見：
1980 年代から 40 年以上、この値は「おそらくこれだろう」という予想だけで、証明されていませんでした。これが、40 年ぶりに新しい「Busy Beaver」の値が確定した瞬間です。
「Cryptid（クリプトイド）」の存在：
5 つのスイッチでは、すべてを解明できましたが、6 つのスイッチになると、また新しい難問が現れます。
「Antihydra（アンチハイドラ）」というロボットは、止まるかどうかを証明するには、コラッツ予想のような未解決の数学問題そのものを解く必要があるかもしれません。彼らは「数学の怪物（Cryptid）」と呼ばれています。

💡 まとめ：なぜこれがすごいのか？

協力力の勝利： 一人の天才が解決したのではなく、世界中の何百人もの「見知らぬ人」が、オンラインで協力し、オープンに知識を共有することで成し遂げました。
AI と数学の融合： 膨大な計算を人間が手作業で行うのではなく、プログラムで判定し、それを「証明支援ツール（Coq）」が厳密に検証するという、新しい研究の形を示しました。
人間の限界の可視化： 「5 つのスイッチなら解けるが、6 つになると数学の壁にぶつかるかもしれない」という、人類の知識の境界線が、はっきりと見えたのです。

この論文は、**「複雑な問題を、みんなで力を合わせ、そして最新のツールを使って、一つずつ解き明かしていく」**という、現代の科学のあり方を象徴する素晴らしい成果です。

この論文は、bbchallenge Collaboration（bbchallenge.org）による大規模な共同研究の成果であり、5 状態 2 記号チューリング機械のビジービーバー値 $S(5)$ が 47,176,870 であることを Coq 証明支援系を用いて厳密に証明したことを報告しています。また、2 状態 4 記号の値 $S(2, 4) = 3,932,964$ も同様に証明しました。

以下に、問題設定、手法、主要な貢献、結果、および意義について詳細な技術的サマリーを記述します。

1. 問題設定 (Problem)

ビジービーバー問題: $n$ 状態 2 記号のチューリング機械のうち、全 0 のテープから開始して停止するまでに実行できる最大ステップ数を $S(n)$ と定義します。この関数は計算不可能であり、 $n$ が増加するにつれてその値の決定は極めて困難になります。
歴史的経緯: $S(1)$ から $S(4)$ は以前に証明されていましたが、 $S(5)$ は 1989 年に Heiner Marxen と Jürgen Buntrock によって 47,176,870 ステップを達成する機械が発見されて以来、それが最大値であるかどうか（すなわち、それより長いステップ数で停止する機械が存在しないか）が 40 年以上未解決でした。
課題: 5 状態機械の総数は約 16.7 兆個に達しますが、その多くは停止しないか、非常に短いステップで停止します。問題は、停止しないことを証明する難易度と、膨大な数の機械を網羅的に検証する計算コストにあります。特に、停止しないことを証明することは、ゴールドバッハ予想やリーマン予想などの未解決数学問題の停止性問題に帰着できるため、極めて困難です。

2. 手法とアプローチ (Methodology)

証明は、Coq 証明支援系を用いて構築された「Coq-BB5」と呼ばれる形式証明に基づいています。主な技術的要素は以下の通りです。

2.1 探索空間の削減：ツリー正規形 (TNF)

無効な遷移や状態・記号の置換による重複を排除するため、Tree Normal Form (TNF) による再帰的な列挙手法を採用しました。
これにより、探索対象となる 5 状態 2 記号の機械の数は、約 16.7 兆個から 181,385,789 個 に劇的に削減されました。
Coq-BB5 はこの TNF 列挙プロセス自体を Coq 内で実装・実行しており、外部の信頼されたリストに依存しない完全な形式検証を実現しています。

2.2 決定器 (Deciders) のパイプライン

各機械に対して、停止するか否かを決定するための複数のアルゴリズム（決定器）を順次適用するパイプラインを構築しました。これらは「閉じたテープ言語 (Closed Tape Language: CTL)」という抽象解釈フレームワークに基づいています。

Loops (ループ検出): 機械が有限ステップ内で同じ構成（Cycler）または空間的に変位した同じ構成（Translated Cycler）に到達することを検出します。これにより、非停止機械の約 95% を判定しました。
NGramCPS (n-gram 閉じた位置集合): テープ上の局所的な配置（n-gram）の集合が閉じているかを確認する手法です。固定長履歴や LRU（Least Recently Used）履歴などの拡張を行い、ループを除く非停止機械の 99.89% を判定しました。
RepWL (Repeated Word List): テープ上の特定の単語ブロックが繰り返し現れるパターンを正規表現としてモデル化し、無限ループを判定します。
FAR (Finite Automata Reduction): 停止する可能性のある構成を含む正規言語（非決定性有限オートマトン: NFA）を構成し、初期状態がその言語に含まれないことを示す「co-CTL」アプローチです。
WFAR (Weighted FAR): FAR の拡張であり、遷移に重み付けを行い、到達不可能な重み付き構成を排除することで、より複雑な非停止性を証明します。

2.3 個別証明 (Sporadic Machines)

上記の決定器で判定されなかった 13 台の「Sporadic Machines（散在機械）」 に対しては、個別に非停止性の証明を行いました。

これらの機械は、巨大なステップ数（例： $5.41 \times 10^{51}$ ステップ）の後にループに入るものや、フィボナッチ数に基づくカウンター、グレーコードの操作など、非常に複雑で人間には設計されていないような振る舞いを見せます。
これらの証明も Coq 内で形式化され、Coq-BB5 に統合されました。

3. 主要な貢献と結果 (Key Contributions & Results)

3.1 主要な定理

Theorem 1.1: $S(5) = 47,176,870$ $S (5) = 47, 176, 870$ 。
- 181,385,789 個の機械すべてについて、停止する場合は 47,176,870 ステップ以下で停止すること、停止しない場合は無限ループに陥ることを証明しました。
Theorem 1.2: $S(2, 4) = 3,932,964$ $S (2, 4) = 3, 932, 964$ 。
- 2 状態 4 記号のビジービーバー値も同様に証明しました。
Theorem 6.1: $\Sigma(5) = 4,098$ $Σ (5) = 4, 098$ 。
- 停止時にテープ上に残る 1 の最大数も導出しました。
Theorem 6.3: $S(4) = 107$ $S (4) = 107$ の再確認。
- 既存の結果を Coq によって再検証し、確実性を高めました。

3.2 計算リソースと形式検証

Coq-BB5: 証明全体は 27,274 行の Coq コードと 638 個の補題から構成され、さらに busycoq からの 10,553 行のコードを含みます。
実行時間: 標準的なラップトップで 13 コア並列化により、約 45 分でコンパイル（証明実行）が完了しました。
信頼性: 証明は Coq の標準ライブラリにある functional_extensionality_dep という公理のみを使用しており、Coq の実装の信頼性を前提とすれば、結果は数学的に確実です。

3.3 共同研究のモデルケース

bbchallenge.org: 2022 年に設立されたこのオンラインプラットフォームは、数百人の研究者（多くはアカデミアに所属しないソフトウェアエンジニアや学生）が、Discord や GitHub を介して非停止性の証明（決定器）を開発・共有する「大規模共同研究」の成功例となりました。
2 年間の共同作業で生み出されたアルゴリズムや知見が、最終的に Coq による形式証明に統合されました。

4. 意義と今後の展望 (Significance & Future Work)

数学的意義: 40 年以上ぶりに新しいビジービーバー値が決定され、かつそれが初めて形式検証された結果となりました。これは、計算不可能性の境界を具体的に示す重要なマイルストーンです。
形式検証の限界への挑戦: 従来の証明支援系は数式や定理の証明に用いられることが多かったですが、本論文では「チューリング機械の列挙とシミュレーション」という計算プロセス自体を証明の一部として組み込みました（リフレクションによる証明）。これは、大規模な計算を伴う数学的証明の信頼性を高める新しいパラダイムを示しています。
Cryptids（未解決機械）: 6 状態以上の機械には、停止性の証明が極めて困難、あるいは数学的に不可能（PA や ZF 公理系内では証明できない）とされる「Cryptids（未確認生物）」が存在することが示唆されています（例：Antihydra）。本研究は、5 状態ではそのような難問が存在しないことを示しましたが、6 状態以降の解決には AI や新しい数学的アプローチが必要となるでしょう。
AI への応用: 本研究で生成された証明データや未解決問題は、AI 推論システムのベンチマークとして利用され始めています。

総じて、この論文は、計算理論、形式検証、そして大規模なオープンソース共同研究が融合して、数学の未解決問題の一端を解き明かした画期的な成果です。