コンピュータサイエンスの謎めいた分野において、40年間も未解決だった「ビジービーバー問題」が、アマチュア愛好家グループによって最近解明されました。この功績は学術界に衝撃を与えただけでなく、著名な数学者テレンス・タオ氏もソーシャルメディアでこのニュースを拡散し、定理証明支援ツールの数学研究における重要性を強調しました。
コンピュータ科学者のスコット・アーロンソン氏もこの発見を高く評価し、1983年以来、ビジービーバー関数研究における最も重要な進歩であると述べています。この成果は計算理論の限界への深い理解を示すとともに、複雑な数学問題解決におけるソフトウェア支援証明の可能性を示しました。
ビジービーバー問題は40年以上前にドイツのドルトムントで生まれました。当時、コンピュータ科学者たちは、停止する前に最も多くの「1」を書き込む特定のチューリングマシンを探していました。チューリングマシンはアラン・チューリングが1936年に提案した抽象的な計算モデルで、無限長のテープに0と1を読み書きすることで計算を行います。
1974年に4番目のビジービーバー数が決定された後、5番目のビジービーバーを見つけることは未解決の問題となっていました。今回、世界中から20名以上の貢献者で構成されるオンラインコミュニティが、Coqという定理証明支援ソフトウェアを使用して、5番目のビジービーバー数BB(5)の値が47,176,870であることを検証することに成功しました。
この成果はコミュニティを沸騰させるだけでなく、コンピュータ科学者のダミアン・ウッズ氏も驚嘆し、この進歩をボルトの速さに例えました。この問題の解決がコンピュータサイエンスの他の分野に直接応用されることは少ないかもしれませんが、参加者にとって、数学的不可能性との闘いそのものが最大の報酬でした。
ビジービーバー問題の中心は、チューリングマシンの動作、特に停止問題におけるその振る舞いを理解することにあります。チューリングマシンの動作は一連の規則で定義され、これらの規則は表のように考えることができます。各規則は、特定の状態において、読み書きヘッドが0または1に遭遇した場合に実行する操作を指定します。
チューリングマシンは無限ループに陥る可能性がありますが、それが停止するかどうかを決定することは、有名な未解決問題です。数学者のティボール・ラドーはこの結論に満足せず、「ビジービーバーゲーム」を発明し、チューリングマシンを規則の数でグループ分けすることで、停止問題の本質を探求しました。
アレン・ブレイディなどの初期の研究者たちは、プログラムを書いてチューリングマシンの動作をシミュレートすることで、この問題を探求しました。彼の仕事と他の研究者の発見は、後の研究者たちの基盤となりました。
2022年、大学院生のトリスタン・ステリン氏が「ビジービーバーチャレンジ」というオンライン共同プロジェクトを開始し、最終的にBB(5)を決定することを目指しました。革新的な方法とCoq定理証明支援ツールの助けを借りて、このチームは最終的に5番目のビジービーバーを見つけ出すことに成功しました。
この成果は、数学的不可能性への挑戦であると同時に、コンピュータサイエンスの限界への探求でもあります。BB(5)が確認されたことで、研究者たちは学術論文を執筆中で、これはCoq証明を人間が読めるバージョンに補足するものです。同時に、彼らはBB(6)の探求が次の目標になるかどうかを検討しています。
参考文献:https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/