- 新しい 3-state 4-symbol Busy Beaver チャンピオンTMが発見され、停止時に ((2 \uparrow^{15} 5) + 14) 個の非ゼロ記号を残すことが計算された
- この数は Knuth の up-arrow 記法でも非常に大きく、(Ack(n)=n \uparrow^n n) と定義される 14番目の Ackermann number を上回る (BB(3,4) > Ack(14)) という下限として整理できる
- TMの中核動作は (B(k,n,m) \to B(k,0,g_{k-1}^n(m))) に近い形で圧縮できるが、これを示すには 二重帰納法 が必要となる
- Matthew House の 閉形式評価式 (g_k^n(0)=\frac{2 \uparrow^k (n+2)}{2}-2) により、最終スコア (\sigma=(2 \uparrow^{15}5)+14) を正確に書けるようになった
- このTMは Collatz 型の剰余分岐なしでも Ackermann レベルの関数をシミュレートし、開発中の Inductive Proof Validator の検証事例としても使われている
新しい Busy Beaver チャンピオンの規模
- Pavel Kropitz が新しい 3-state 4-symbol Busy Beaver チャンピオンを発見した
- このTMは「Ackermann-level」の関数を計算でき、停止時にはテープ上に次の個数の非ゼロ記号を残す
- ((2 \uparrow^{15} 5) + 14)
- Knuth の up-arrow 記法でも非常に大きな値であり、下限は次のように要約される
- ここで (Ack(14)) は (Ack(n)=n \uparrow^n n) と定義される 14 番目の Ackermann number である
- 知られている範囲では、実際の探索で見つかったTMの中で Ackermann-level 関数 をシミュレートできる最初の事例である
TMの定義と最終構成
- TMの遷移文字列は次のとおり
1RB3LB1RZ2RA_2LC3RB1LC2RA_3RB1LB3LC2RC
- 遷移表は状態
A, B, C と記号 0, 1, 2, 3 に対して定義される
A: 1RB, 3LB, 1RZ, 2RAB: 2LC, 3RB, 1LC, 2RAC: 3RB, 1LB, 3LC, 2RC
- 最終構成は次のとおり
- (0^\infty ;; 3^{2 g_{15}^{3}(0) + 1} ;; 2^{16} ;; 1 ;; \text{ Z> } ;; 0^\infty)
- この構成からスコア (\sigma) が正確に計算される
- (\sigma = 2 g_{15}^{3}(0) + 18 = (2 \uparrow^{15} 5) + 14)
発見と検証の過程
- Pavel Kropitz はこのTMを 2024年4月25日 に Discord で共有した
- 当時のコードは人間が読めるスコア下限を指定できず、結果を
Halt(SuperPowers(13)) と表示していた
- これは証明に 13層の帰納規則 が必要であることを意味する
- その後、新しい Inductive Proof Validator を使った検証が始まった
- 2024年5月20日 に検証が完了し、(g_k^n(m)) の正確な定義が抽出され、これにより (\sigma > 2 \uparrow^{15} 3) という下限が得られた
- Matthew House は 2024年5月22日 に次の単純な閉形式評価式を発見した
- (g_k^n(0) = \frac{ 2 \uparrow^k (n+2) }{2} - 2)
- この評価式によって (\sigma) の 正確な値 を表現できるようになった
動作解析と二重帰納による証明
- 次の構成を定義する
- (B(k, n, m) = 0^\infty ;; 3^{2m+1} ;; 2^k ;; \text{ A> } ;; 1^n)
- 初期構成は 241 ステップ後に次の状態へ到達する
- (0^\infty ;; \text{A>} ;; 0^\infty \xrightarrow{241} B(16,3,0);;2;;0^\infty)
- 中核規則は次のとおり
- (B(k,n,m) \to B(k,0,g_{k-1}^n(m))), ただし (k \ge 1)
- (g_k) は次の再帰式で定義される
- (g_0(m)=m+1)
- (g_{k+1}(m)=g_k^{2m+2}(0))
- 全体の動作はほぼ1つの規則に圧縮できるほど単純だが、その規則自体は 二重帰納法 で証明しなければならない
- 補題と系は、
B 状態が 3 と 2^k のブロックを処理して 1 を生成する過程を扱う
- (3;;2^k;;\text{<B} \xrightarrow{2k+1} 2^k;;\text{<B};;1)
- (3^m;;2^k;;\text{<B} \xrightarrow{(2k+1)m} 2^k;;\text{<B};;1^m)
- 定理3は、すべての (k \ge 1, n \ge 0, m \ge 0) について中核規則が成り立つことを示す
- (k=1) の基本ケースは (n) に関する帰納法で処理される
- 帰納段階では (k) に関する仮定と (n) に関する帰納仮定をあわせて用いる
正確な値の計算
- (g_k) には、Knuth の up-arrow と算術だけを使う比較的単純な 閉形式評価 がある
- すべての (k \ge 0, m \ge 0) について次が成り立つ
- (2 g_{k+1}(m) + 4 = 2 \uparrow^k (2m+4))
- ここで (a \uparrow^0 b = ab) と定義する
- この結果は (k) に関する帰納法で証明される
- 基本ケース (k=0) では (g_1(m)=2m+2) となる
- 帰納段階では ((2 \uparrow^k)^n) の反復適用を用いる
- 閉形式は、(2 \uparrow^k 2 = 4) がすべての (k) で成り立つという偶然に依存している
- パラメータが少し異なり、((2 \uparrow^k)^{2m+2}5) の形になっていたなら、閉形式表現を得るのは難しかったと考えられる
- 系として、すべての (k \ge 0, n \ge 0) について次が成り立つ
- (2 g_k^n(0) + 4 = 2 \uparrow^k (n+2))
- 最終スコアはそのまま次のように導かれる
- (\sigma = 2 g_{15}^{3}(0) + 18 = (2 \uparrow^{15} 5) + 14)
開始状態を変えた順列の結果
- 開始状態を
B や C に変えると、より小さい関連結果が得られる
- (0^\infty ;; \text{B>} ;; 0^\infty \xrightarrow{86} B(7,3,0);;2;;0^\infty)
- (0^\infty ;; \text{C>} ;; 0^\infty \xrightarrow{20} B(1,3,0);;2;;0^\infty)
- 開始状態が
B のときのスコアは次のとおり
- (\sigma_B = 2 g_6^3(0) + 9 = (2 \uparrow^6 5) + 5)
- 開始状態が
C のときは 72 ステップで停止し、スコアは次のとおり
- (\sigma_C = 2 g_0^3(0) + 3 = (2 \uparrow^0 5) - 1 = 9)
B から始める最初の順列も、別の上位 BB(3,4) TM である- これを TNF に変換すると、次の遷移文字列になる
1RB3RB1LC2LA_2LA2RB1LB3RA_3LA1RZ1LC2RA
Collatz 型規則のない単純さ
- このTMの興味深い点の1つは、予想より 単純である ことにある
- 値の剰余に応じて異なる動作をする Collatz-like 規則 がない
- Collatz-like TM の支配が終わったかどうかを判断するには、まだ早すぎる
- Ackermann-level の Collatz-like TM がまだ残っている可能性はあるが、選択バイアスのためすぐには見えていないのではないかという推測がある
- このTMが最初の Ackermann-level TM として発見された理由は、Ackermann-level 関数上で modular arithmetic を実装しなくても停止証明が可能なほど単純だったからかもしれない
Inductive Proof Validator
- このTMは開発中の Inductive Proof Validator のテスト事例として適していた
- プロジェクトの目標は、「帰納証明」のための標準化された証明書形式を作ることにある
- ここでいう「帰納証明」は、前向き推論と規則ベース解析全般を指す包括的な用語として使われている
- 誰でも「inductive decider」を持っていれば、その規則をこの形式で記述し、validator がその証明を検査できるようにするという方式である
- システムはまだ非常に粗削りで実用準備はできていないが、多少の手作業を経て このTM を含む複数のTMの動作証明に使われている
1件のコメント
Hacker News の意見
非常に長時間実行されるチューリングマシンのプログラムは、深く複雑だったりスパゲッティコードだったりすると考えがちだが、今回の新チャンピオンは反例に近い。
状態は A、B、C の3つだけで、B は A と C に制御を渡すが、A と C は互いを「知らず」、B にだけ戻す。
本当のスパゲッティコードなら各状態がほかのすべての状態へ遷移できたはずだが、これは一種のモジュール構成になっている。
また空白マスを決して出力せず、すべての命令が状態か色のどちらかは変えるため、
B1 -> 1LBのように位置だけを動かす「怠惰な命令」もない。探索空間全体を、確定的であれヒューリスティックであれ除外するまでは分からない。
BB(5, 2) を超えるすべてのサイズには、永遠に実行されると予想されるものの、数論の大きな進展なしには証明できない、混沌的・疑似乱数的なマシンが含まれている。
ただし、長時間実行されるマシンが完全に混沌としていることはできないと見ている。
テープに乱数のように記号を吐き出すなら、すぐに停止構成、循環構成、または単純化されたパターンに到達するはずだからだ。
それでも、より高いレベルで混沌とした何かをシミュレートし、各高レベル段階の間に途方もない時間を費やしてから停止するマシンはあり得る。
n状態s記号のチューリングマシンは、最大でもn個の異なる状態にしか遷移できない。そのため
s=4やs=2なら、ごく小さなチューリングマシンだけがスパゲッティコードのようになれる。新しい BB(3,4) 記録保持者は次のとおり。
0 1 2 3A 1RB 3LB 1RZ 2RAB 2LC 3RB 1LC 2RAC 3RB 1LB 3LC 2RC行
s、列tの(t', d, s')は、状態sでテープヘッド下の記号がtのときの遷移を意味する。記号
tをt'で上書きし、方向dに従って左/右へ移動した後、状態をs'に変え、s' == Zなら停止する。これは
3*4*log2(4*2*log2(4+1))、つまり約64ビットの情報量である。一方、わずか49ビットの
BBλ(49)は Graham 数をはるかに上回る https://oeis.org/A333479上の計算は、各マスが任意の
(記号, 方向, 状態)の組み合わせを持てると見る最も広い方式なので、任意のチューリングマシンを記述するのに必要なビット数をかなり過大に見積もっている。BB(3, 4) の場合、Tree Normal Form、つまり Brady アルゴリズム(https://nickdrozd.github.io/2022/01/14/bradys-algorithm.html)を使うと、異なるチューリングマシンは約6000億個しかなく、40ビット未満になる。
1RZの1Rは任意に選んだ値のように見える。そこで停止するので、テープに何が残ろうと、ヘッドがどこへ動こうと関係ないからだ。
実際、
1を書くことも重要ではないが、0を書いていたら最適ではなかったように思う。すでにその位置には
2が書かれており、1に変わるものの、テープ上の記号数の基準では2も同じように数えられたはずだ。log2(4+1)の項がどう出てくるのかよく分からない。3*4*log2(4*2*log2(4+1))を計算すると約51になり、非専門家の視点では3*4*log2(4*2*4) = 60になりそうに思えた。もしかして
3*4*log2(4*2*log2(3*3*4-1)) ≈ 64なのか気になる。動作が気になったので、ここに実装してみた:
turingmachine.io/?import-gist=c862f28918f3d889f964797694d28fcc少し実行してみると、何が起きているのかが見える。
状態 B は
0を2に、1を1に変えて C へ遷移し、状態 C は3を2に変えて A へ遷移する。そのため
2 -> 1を直すにはすべての3を一度通過しなければならず、3の連続区間を反復的に指数的に伸ばすことになる。本当に理解しがたいのは、想像もできないほど多くのステップの後に、なぜ最終的に停止するのかだ。
全部が極端なコードゴルフのように聞こえる。
別の方向としては BitGrid というものを調べてみるとよい。
BitGrid はセルごとの状態が4ビットしかないので、4x4 セルの格子は何があっても
2^64以上を数えることはできない。実際にどこまで数えられるのかを探すのは興味深そうで、小さな格子では端の接続が結果を支配するだろう。
https://esolangs.org/wiki/Bitgrid
https://github.com/mikewarot/Bitgrid
この表はおそらくチューリングマシンの説明だと思うが、どう解釈すればよいのか参考になる資料があるとよさそう
状態A、B、C はgotoの行き先に相当し、色0、1、2、3 は実行中のデータである各状態で現在の色を読み、その色に応じて「どの色を出力するか、左/右に動くか、どの状態へ行くか」という命令を実行する
C に移すと
switch (SCAN)とWRITE、RIGHT/LEFT、gotoでそのまま表現できるこのロジックをさらに構造化されたスタイルで書き直したり、別の最適化をしたりする余地があるのか気になる
たとえば最初の行の最初の列は「記号
0を読み、現在の状態がA」という意味である表のセルは実行する動作を表し、
1RBは「テープ上の記号を1に変え、右へ1マス移動したあと、状態Bに遷移せよ」という意味である状態
Zは停止状態に相当するL()、R()関数を用意し、(状態, 現在の記号)を(書き込む記号, 移動関数, 次の状態)に対応付ける表を作って、state != 'Z'の間ループすればよい1RZは状態Zに規則がないため、停止遷移と理解すればよいWikipedia にもより詳しいチューリングマシンの状態表の例があり https://en.wikipedia.org/wiki/Turing_machine#Formal_definition、この特定のチューリングマシンの実行トレースは https://bbchallenge.org/1RB3LB1RZ2RA_2LC3RB1LC2RA_3RB1LB3LC2RC で見られる
これも更新する必要がありそうだ
基礎計算機科学の主要な結果の引用がDiscord リンクだなんて
科学的結果を発表する唯一有効な方法が、いわゆる査読付きジャーナルだという考えは、科学コミュニティがダンバー数に収まるほど小さかった200年前の遺物である
今もそれにしがみついているのは、有力な一部の研究者と出版社が利益を得ているからであって、科学の進歩という面で実際の利点があるからではない
むしろ現代の再現性危機にかなり大きな責任を負っている可能性もある
科学的方法は強く支持するが、伝統的な査読はすでにとっくに賞味期限切れだと思う
https://en.wikipedia.org/wiki/Dunbar%27s_number
これらは引用というより出典表記に近いと思う
結果を支える主要な論証はブログ記事の中でより厳密な形で再現されているので独立に成り立ち、Discord リンクは関心のある人向けに歴史的文脈を提供しているだけである
適切な時点で文献によって補強できるなら、前向きな変化である
たとえば Zhang の素数間隔の上限を改善したプロジェクトがそうであり、こうした面では他のコミュニケーションツールが Discord を簡単に代替できない可能性がある
実際に人が集まっている場所へ行く必要がある
本当に基礎的なものなら、ブログに載せるのではなく、ジャーナル論文として査読を受けていただろう
1RB3LB1RZ2RA_2LC3RB1LC2RA_3RB1LB3LC2RCのように、それほど大きくない記号量で説明できるチューリングマシンは、可能な数が限られているところが、その一部が停止するまでにこれほど途方もない数のステップを実行できるという事実は本当に驚きである
2^60個ある出力、つまり正規形がグラハム数を超える49ビットのラムダ項のほうがもっと驚くべきだ
正直100%理解しているわけではなく、おそらくほとんど役にも立たない結果だが、信じられないほど有用な LLM の進歩よりもこういうもののほうに惹かれる
おそらく「複雑な」工学的成果よりも、単純な数学的真実に自然と惹かれるからだと思う
BB(5) > BB(3,4)ではないのか？https://bbchallenge.org では、BB(5) が約4700万だという推測を証明または反証しようとしていると書かれているが、BB(3,4) はそれよりはるかに大きいように見える
BB(3, 4) >>> BB(5, 2)に見えるBB(5) = BB(5, 2)であり、BB(3, 4)は表に遷移が12個（3*4）ある一方、BB(5, 2)は10個しかないので、それほど驚くことではないただし
BB(3, 4) >> BB(6, 2)でもあるように見える両者は遷移数が同じなので、このような小さなチューリングマシンでは、記号数が多いことにかなり価値があるようだ