ゲーデルマシン(Gödel machine)とは、計算機科学者ユルゲン・シュミットフーバーが2003年に提唱した、「完全に自己言及的で、かつ証明可能に最適な自己改善を行う汎用問題解決器」の理論モデルである。
クルト・ゲーデルが1931年の不完全性定理の論文で用いた自己言及的な論理式の構成に着想を得ており、稼働中に「自分自身のプログラムコードの任意の部分を読み取り、その書き換えが与えられた効用関数の観点から有用であることを自ら証明できた場合に限り、その書き換えを実行する」という設計になっている。この書き換えは、シュミットフューバーが「大域的最適性定理」と呼ぶ定理により、局所最適に陥ることのない大域的に最適な自己改変であることが示される。
ゲーデルマシンはあくまで数学的に定式化された理論的構成であり、シュミットフューバー自身の提唱から20年以上を経た2020年代半ばの時点でも、その定義に完全に忠実な実装は実現していない。しかし、その基本思想は再帰的自己改善やメタ学習に関する研究、および大規模言語モデルを用いた自己改変型AIエージェントの研究において、繰り返し参照される理論的基盤となっている。
概要 ゲーデルマシンは、離散的な時間ステップ t = 1, 2, ... ごとに動作する仮想的なハードウェア（万能チューリングマシンや通常の計算機の抽象モデル）上で稼働するプログラムとして定式化される。その初期ソフトウェア p(1) は、大きく分けて次の二つの要素から構成される。
ソルバー(solver) 環境と相互作用し、与えられた問題(たとえばロボット制御における将来の期待報酬の最大化)に取り組む、当初はおそらく最適とはいえないサブプログラム。
証明探索器(proof searcher) 「現在のプログラム p を、ある書き換えプログラム switchprog によって書き換えることが、書き換えずに p を維持し続けるよりも高い効用をもたらす」という内容の「目標定理」を、計算可能な証明技法を体系的に試すことによって探索するサブプログラム。
証明探索器が目標定理の証明に成功すると、ゲーデルマシンは switchprog を実行し、証明探索器自身を含む p の任意の部分を書き換える。この過程は、書き換え後も含めて何度でも繰り返され得る。
ここで用いられる効用関数、ハードウェアの挙動、環境に関する既知の性質、そして初期コード p(1) 自身までもが、p(1) に組み込まれた公理系 (axiomatic system) A によって形式的に記述される。この公理系には「ハードウェア公理、報酬公理、環境公理、確率論公理、初期状態公理」などが含まれ、証明探索器はこれらの公理から出発して目標定理の証明を構築する。重要な点として、公理系 A の中で初期コード p(1) 自身を記述することは、循環参照を引き起こすことなく可能であるとされる。
背景・開発経緯 シュミットフューバーは、伝統的な問題解決アルゴリズムや強化学習アルゴリズムの多くが「ハードワイヤード」であり、すなわち自分自身の学習方針を改善することはあっても、その改善アルゴリズム自体を理論的に健全な形で改善することはできない、という限界を出発点とした。
この限界を克服し、人間の手を介さずに、証明探索を含むあらゆる作業を計算可能な範囲で自己遂行できる汎用問題解決器を構築することを、シュミットフューバーは「人工知能の大問題(Grand Problem of AI)」と位置づけ、その解決策としてゲーデルマシンの概念を導入した。
最初のテクニカルレポートは2003年にIDSIA（イタリア語圏スイスの人工知能研究所）から発表され、その後複数回の改訂を経て、2006年に書籍『Artificial General Intelligence』の一章として出版された。
シュミットフューバーはその後も、ゲーデルマシンと意識の技術的な正当化を関連づける論考など、複数の関連論文を発表している。
主な内容・特徴
大域的最適性定理 ゲーデルマシンの中心的な結果は「大域的最適性定理」(Global Optimality Theorem)と呼ばれる。この定理は、証明探索器が目標定理を証明した時点で実行される switchprog による自己書き換えが、単に局所的に良いだけでなく、大域的に最適であることを主張する。
その直感的な理由は次の通りである。目標定理は「今すぐ switchprog を実行する」か「switchprog の実行を保留し、証明探索器がより良い switchprog を将来発見するのを待つ」かという二者択一について述べており、後者の選択肢は証明探索器が将来発見しうるすべての switchprog の候補を暗黙のうちに考慮に入れている。したがって、現在の switchprog の実行がより高い効用をもたらすと証明できたということは、それが将来のあらゆる代替案よりも(与えられた資源制約と初期の証明探索戦略のもとでは)優れていることを意味する。
この性質により、複数の「メタレベル」の自己改善が単一のレベルに収束し、自己改善についての自己改善を無限に問い直す必要がなくなるとされる。
バイアス最適証明探索 (BIOPS) ゲーデルマシンの初期の証明探索器として、シュミットフューバーはレオニード・レヴィンの「万能探索」(Universal Search)をオンライン設定に拡張した「バイアス最適証明探索」（Bias-Optimal Proof Search, BIOPS）を提案している。
これは、証明技法（証明を生成するプログラム）の集合にあらかじめ与えられた確率分布(バイアス)に応じて、各証明技法にほぼ比例した計算時間を割り当てる探索手法であり、計算量のオーダーの意味で最適(O()-最適)であることが証明されている。
ただし、このO()-最適性はオーダー記法の背後に隠れた巨大な定数係数を無視するものであり、ゲーデルマシン自身がこの証明探索器を含むあらゆる部分をより高速な手法に書き換えることで、O()-最適性を超えた改善を実現できる可能性がある点が、後述するマーカス・ハッターの先行研究との重要な相違点とされる。
限界 ゲーデルマシンの限界は、ゲーデル自身が示した不完全性定理の帰結と密接に関係している。算術を含む無矛盾な形式体系は、真であっても証明不可能な命題を含まざるを得ないため、ゲーデルマシンは、たとえ「無制限の計算資源を持っていたとしても、その有用性を証明できない」自己改善については実行を見送らざるを得ない。
シュミットフューバーは、目標定理の証明可能性に関するこうした限界について、人間の研究者も同様の限界に直面していると指摘し、ゲーデルマシンに特有の弱点ではないと論じている。
AIXIおよび関連手法との比較 ゲーデルマシンは、しばしばマーカス・ハッターが提案した汎用人工知能の形式的モデルAIXIおよびその時間・空間制限版AIXI(t,l)と比較される。シュミットフューバーによれば、ゲーデルマシンの最大の特徴は、証明探索器を含む初期ソフトウェアのあらゆる部分が書き換え可能である点にあり、これに対しAIXI(t,l)やハッターのHSEARCHは、証明探索の手続き自体がハードワイヤードされており、自己改善の対象にはならない。
シュミットフューバーは、ゲーデルマシンの初期方策としてAIXI(t,l)のような既存の手法を組み込み、証明探索器がより優れた戦略を発見し次第、それに置き換えるという構成も可能であると述べている。
影響・評価
実装の試み ゲーデルマシンは当初から純粋に理論的な構成として提示されていたが、その後、部分的な実装を試みる研究も現れた。シュミットフューバーの研究室に所属していたバス・R・ステューネブリンクは、シュミットフューバーとの共著論文「A Family of Gödel Machine Implementations」(2011年)において、元のゲーデルマシンの定式化に含まれる実装上の不便な点を整理し、実際に動作する仮想機械上でゲーデルマシンの自己言及的コードを走らせる最初の試みについて報告している。
ステューネブリンクは、機械知能研究所(MIRI)によるインタビューの中で、ゲーデルマシンの実装を「ソルバー」「サーチャー」「両者を並行して走らせるスケジューラー」という三つの構成要素として説明し、実行中の資源制約付きコードの状態と振る舞いをいつでも検査し、安全に書き換えるための「いつでも自己反省(anytime self-reflection)」の技術的な問題は解決可能であるとしつつ、レーブの定理(Löb's theorem)に関連する理論的な難点が残っていることを指摘している。
AI安全性の議論における位置づけ ゲーデルマシンは、機械知能研究所(MIRI)をはじめとするAI安全性研究のコミュニティにおいて、自己改善型AIが自らの効用関数や目標を書き換えてしまう可能性(いわゆる目標の不安定性問題)を検討するための参照点の一つとして議論されてきた。シュミットフューバー自身は、ゲーデルマシンが効用関数を書き換えられるのは、あくまで現在の(書き換え前の)効用関数に照らしてその書き換えが証明可能に有用である場合に限られると強調しており、根拠のない自己申告的な効用の書き換えは起こり得ないと説明している。
シュミットフューバー自身、インタビューにおいてゲーデルマシンをアーヴィング・グッドが1965年に非形式的に論じた「知能爆発」の考え方を形式化する試みの一つとして位置づけている。
近年の展開:ダーウィン・ゲーデルマシン 2025年、ジェニー・チャンらは、大規模言語モデルを基盤とするコーディングエージェントの文脈でゲーデルマシンの思想を再解釈した「ダーウィン・ゲーデルマシン」(Darwin Gödel Machine, DGM)を提案した。
ゲーデルマシンが要求する「ある書き換えが真に有益であることの形式的証明」は実際には得ることがほぼ不可能であるという課題を踏まえ、DGMは自己書き換えの有用性を形式的に証明する代わりに、コーディングベンチマーク上での実証的な性能評価によって置き換え、進化的アルゴリズムにヒントを得たアーカイブベースの探索により、多様な自己改変エージェントの集団を維持しながら段階的に性能を向上させる仕組みを採用している。
DGMは複数のコーディングベンチマークにおいて、反復的な自己改変を通じた性能向上を実証したと報告されており、証明に基づく理論的枠組みであったゲーデルマシンの発想を、経験的な自己改善エージェントの設計原理として応用した代表例として位置づけられている。
関連項目 AIXI 再帰的自己改善 メタ学習 強化学習 クルト・ゲーデル 不完全性定理 人工汎用知能 知能爆発
脚注
外部リンク Schmidhuber, J. "Gödel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements"(arXiv版原論文) Darwin Gödel Machine 実装コード(GitHub)