ハクソク

世界を動かす技術を、日本語で。

第五のビジービーバー値の決定

2025年9月17日原文(arxiv.org)

概要

  • Busy Beaver問題 の5状態版に対する新しい値$S(5)$の厳密な決定
  • Coq証明支援系 を用いた形式的検証の実施
  • 181,385,789台 のTuring machineの網羅的な解析
  • 40年以上ぶり の新Busy Beaver値の確定
  • 大規模オンライン共同研究 の有効性の証明

Busy Beaver問題 $S(5)$ の厳密決定と形式的検証

  • Busy Beaver関数$S(n)$ は、n状態2記号Turing machineが全0テープから停止するまでに実行できる最大ステップ数
  • Tibor Radó (1962年) により、計算不能関数の代表例として提案
  • 今回、 5状態の場合の値 $S(5)=47,176,870$ を厳密に決定
  • Coq proof assistant を用い、証明過程を形式的に検証
  • 181,385,789台 の5状態Turing machineを全て列挙し、各機械の停止性を判定
  • 結果として、 $S(5)$の値が40年以上ぶりに更新 され、かつ 形式的検証 も世界初
  • 本研究は、 bbchallenge.org による大規模なオンライン共同研究の成果

技術的詳細と意義

  • 形式的検証 により、証明の完全性と再現性を担保

  • Enumerative approach による全探索と停止性判定の組み合わせ

  • Coq を用いた証明により、ヒューマンエラーや見落としの排除

  • Logic in Computer Science ・ Automata Theory ・ 数学的論理 分野への貢献

  • Busy Beaver問題の新たなマイルストーン確立

    • 03D10, 03B35 （数学的分類）
    • F.1.1, F.4.1, I.2.3, D.2.4, F.4.3 （ACM分類）

今後の展望と共同研究の意義

  • bbchallenge Collaboration による大規模分散型研究の成功例
  • 形式的証明 の普及と計算理論分野への波及効果
  • より高状態数 へのBusy Beaver探索および自動証明技術の発展期待
  • 論文・証明データ はarXivおよびbbchallenge.orgで公開

Hackerたちの意見

よくわからないなぁ - 彼らは力技を使ったの？

└

これらの数を計算するのに力技だけでは無理だよ。計算不可能なんだから。

└

5状態のチューリングマシンを徹底的にチェックする必要があると思うけど、その後は力技がちょっとだけ役立つだけだよね。力技じゃ、チューリングマシンが永遠に止まらないってことはわからないんじゃない？

└

ちょっと違うと思うけど、論文のこの部分が関係してると思うよ：

証明の構造。私たちの主な結果である定理1.1の証明は第6章にあります。証明の構造は次の通りです：マシンは木の正規形（TNF）で列挙され、検索空間のサイズが劇的に減少します：16,679,880,978,201の5状態マシンから「たった」181,385,789に。詳しくは第3章を見てね。各列挙されたマシンは、主に停止するかどうかを判断しようとするアルゴリズムである決定器を通して処理されます。停止問題の計算不可能性のため、普遍的な決定器は存在せず、すべての技術は合理的な時間内に大規模なマシン群を判断できる決定器を作ることにあります。私たちの決定器のほとんどは、チューリングマシンが訪れる構成のセットをより便利な上位集合で近似する抽象解釈フレームワークのインスタンスで、これを「閉じたテープ言語（CTL）」と呼んでいます。これは停止構成を含まず、チューリングマシンの遷移に対して閉じています（第4.2章を参照）。S(5)パイプラインは表3に示されています - S(2,4)については表4を見てください。この研究のすべての決定器はbbchallengeコラボレーションによって作成されました；第4章を参照してください。5状態マシンの場合、13のスパラディックマシンは決定器では解決できず、個別の非停止証明が必要でした（第5章を参照）。だから、彼らは検索空間を大幅に減らす方法を見つけ、残りの検索空間の大部分が停止するかどうかを証明できる一般的な決定器を書いたけど、一般的な決定器が推論できなかった残りの13台のマシンは手動で解決する必要があったんだ。

└

ここにはいくつかの概念が関わってるね。まず、特定の数学理論（おそらく一貫性があって再帰的に公理化できるもの）に基づいて、何が証明できるかを考えなきゃいけない。そんな理論に対して、BB(N)の正確な値を証明できない有限のNが存在するんだ。だから「無限の時間」があれば、理論が力尽きるところまで、すべての証明を列挙して、次々とビジービーバーの値を確認できるかもしれない。これはゴーデル/チャイティンの不完全性のビジービーバー版だね。BB(5)の場合、ペアノ算術が十分で、RCA₀も多分いける。もっと強力な理論はどこから来るのか？それはちょっと謎だけど、確かにその研究はたくさんあるよ（フェファーマンやフリードマンの研究を見てみて）。次に、有限の時間で何が実現可能かを考えなきゃ。機械を列挙することも、証明を列挙することもできるけど、具体的な戦略には限界がある。BB(5)の場合、著者たちは単純な力技は使わなかった。5状態の機械を徹底的に列挙して（対称性の削減後）、ほとんどすべての機械の停止/非停止の挙動を証明するために認定された決定器を使って、いくつかの残った機械については手動で証明（形式化もされた）を提供したんだ。

この研究で一番興味深いのは、オンラインでの共同作業だってこと。こういうプロジェクトが他にどれくらいあるのか、もっと広がる可能性があるのか気になるなぁ、プラットフォームとして。

└

BBチャレンジのサイトはすごくよく構成されてるね： https://bbchallenge.org/13650583

└

最近、Lean言語での数学的証明をブループリント（依存グラフ）を使って共同作業する動きがあるみたいで、関連してるっぽい。例えば： https://teorth.github.io/equational_theories/ https://teorth.github.io/pfr/

└

このコメントを見て、https://www.distributed.net/ がまだ存在しているか確認したくなった。おそらく20年近くこのサイトのことを考えてなかったけど、1990年代後半にRC5-64を解読していた頃にクライアントを動かしてたんだ。でも、今でもこの種のことに使えるプラットフォームとして続いているみたいだね。

└

論文では、似たような構造と規模を持つ2つのコミュニティについて言及しているよ： - https://conwaylife.com/、コナウェイのライフゲームや他のセルオートマトンについて - Googology、https://googology.fandom.com/wiki/Googology_Wiki と https://googology.miraheze.org/wiki/Main_Page、大きな数について

プログラマー向けの高レベルな概要を紹介するね（著者として名前が載ってるけど、貢献はかなり小さいよ）： [リンクされた論文の表3でパイプラインの詳細を見てね]

  • 5状態のチューリングマシンは約1億8100万台あって、まずこれを徹底的に列挙した。
  • その後、各マシンを約1億ステップ実行した。その中の約25%がこのステップ内で停止することがわかって、チャンピオンは47,176,870ステップ実行してから停止した。
  • これで140百万台のマシンが長時間実行されることになった。だから、質問はこうだ：これらのチューリングマシンは永遠に動き続けるのか、それとも単に実行時間が足りなかったのか？BBチャレンジプロジェクトの目的はこの質問に答えることだった。すべてのチューリングマシンに適用できる普遍的なアルゴリズムはないから、代わりに一連の（準）決定器が作られた。各決定器はチューリングマシンを受け取り、（いくつかの証明されたヒューリスティックに基づいて）「確実に永遠に動く」か「もしかしたら停止する」と分類する。最終的に4つの決定器が使われた：
  • ループ：チューリングマシンをしばらく実行して、以前に見た構成に再び入ったら、永遠にループすることが確定する。約90%のマシンがこれをするか停止するから、ほとんどをカバーしてる。残りは6.01百万台。
  • NGram CPS：各チューリングマシンを抽象的にシミュレートし、各側に出現することが許可されているバイナリの「n-gram」のセットを追跡する。到達可能な状態の過大評価を計算する。もしその抽象状態のどれも停止遷移に入らなければ、元のマシンも停止できない。6.005百万台のチューリングマシンをカバー。約7000台が残ってる。
  • RepWL：チューリングマシンの構成を説明するカウントルールを導き出そうとする。NGramモデルは「カウント」できないから、これはパリティに依存するパターンの多くをキャッチする。6557台のチューリングマシンをカバー。残りは数百台。
  • FAR：各チューリングマシンの状態を正規表現/FSMとして記述しようとする。
  • WFAR：FARのようなものだけど、重み付きエッジを追加して、いくつかの非正則言語（例えば、かっこの一致）を記述できるようにする。
  • スパラディック：約13台のマシンが複雑な動作をしていて、以前の決定器では対応できなかった。だから手書きの証明（後にRocqに翻訳された）がこれらのマシンのために書かれた。すべての決定器は最終的にRocqで書かれたから、実際に意図した通りに機能することが正式に確認された証明と結びついている（「この関数がTrueを返すなら、対応する数学的チューリングマシンは実際に停止しなければならない」）。したがって、すべての5状態のチューリングマシンは正式に停止するか非停止するかに分類された。最も長く実行された停止器はチャンピオンで、すでにチャンピオンだと疑われていたけど、これでそれ以上長く実行される5状態のチューリングマシンは存在しないことが証明された。
└

Coq-BB5では、機械は100Mステップ実行されるのではなく、直接決定器のパイプラインに投げ込まれるんだ。ほとんどの停止する機械は、ループを使って低いパラメータ（最大4,100ステップ）で検出されて、47Mステップまでシミュレーションされたのは183機械だけだよ。レガシーbbchallengeのシードデータベースでは、機械は正確に47,176,870ステップ実行されて、約80Mの非停止候補が残った。差異は、Coq-BB5が0RBや他の小さな要因を除外していないことから来ている。また、「5状態のチューリングマシンは約1億8100万種類ある」と言われているけど、この数字は証明が完了した後にしか得られないことに注意が必要だね。この数字を知るのはBB(5)を解くのと同じくらい難しいんだ。

Hacker Newsで議論の続きを見る