🤖 AI

An Undecidability Proof for the Plan Existence Problem

この論文は、エピステミック・アクション（認識的行為）の前提条件の様相深度が1以下で後条件がない場合であっても、目標状態に到達するための計画が存在するかを判定する問題（Plan Existence Problem）が決定不能であることを証明しています。

原著者： Antonis Achilleos

公開日 2026-04-27

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

CC BY 4.0

原著者： Antonis Achilleos

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

1. この研究が扱っている「ゲーム」のルール

想像してみてください。あなたは**「記憶喪失の探偵」**です。
あなたの目的は、ある「ゴール（真実）」にたどり着くことです。

このゲームには、以下のルールがあります。

あなたの状態（エピステミック・ステート）: あなたは今、何が真実で、何が嘘か、あるいは「自分が何を知っていて、何を知らないか」という、複雑な「知識の迷路」の中にいます。
アクション（行動）: あなたができることは、限られた「アクション」だけです。例えば、「誰かに質問する」「手紙を読む」といったことです。
アクションの条件（前提条件）: ただし、何でもできるわけではありません。「もし、あなたが『Aは犯人ではない』と確信しているなら、この手紙を読める」というように、**「今のあなたの知識の状態」**によって、次にできることが決まります。
アクションの結果（事後条件）: この論文の面白い（そして難しい）ところは、「アクションによって、世界の事実そのものは変わらない」という点です。手紙を読んでも、犯人が変わるわけではありません。変わるのは、「あなたの知識（迷路の形）」だけです。

問題はこうです：
「ある初期状態からスタートして、決められたアクションを組み合わせて、最終的に『ゴール（真実）』にたどり着くルート（プラン）は存在するのか？」

2. 何がそんなにすごいの？（論文の核心）

これまでの研究では、「アクションの条件がめちゃくちゃ複雑なら、解けないのは当たり前だよね」と思われていました。

しかし、この論文が証明したのは、もっと恐ろしい事実です。
「アクションの条件は、ものすごくシンプル（深さ1）で、アクションによって世界の事実も変わらない。それなのに、このゲームは『解けない（決定不能）』！」

【たとえ話：無限に続く「合わせ絵」パズル】

これを、**「無限に続く、超複雑な合わせ絵パズル」**に例えてみましょう。

あなたは、バラバラの絵のピース（アクション）を持っています。
ピースを組み合わせる条件は、「今持っている絵の端っこが、赤色であること」くらい、ものすごく単純です。
そして、ピースを繋げても、絵の内容（世界の事実）は増えたり減ったりしません。ただ、絵がどんどん長く伸びていくだけです。

この論文は、**「この『単純な条件』でピースを繋いでいく作業が、実は『数学的に解けないほど複雑なパズル（PCP問題）』を再現できてしまう」**ということを数学的に証明したのです。

つまり、あなたが「このパズル、いつか完成するかな？」とコンピュータに計算させたとしても、そのコンピュータは**「永遠に答えが出ない（計算が終わらない）」**状態に陥ってしまうのです。

3. なぜ「解けない」のか？（仕組みのイメージ）

論文の中では、**「PCP（ポストの対応問題）」**という、数学界で有名な「解けない問題」を、このゲームの中に「翻訳」して持ち込んでいます。

第1ステージ（積み上げ）: アクションを使って、知識の迷路の中に「情報の列」をどんどん積み上げていきます。これは、パズルのピースを長く繋げていく作業です。
第2ステージ（照合）: 最後に、積み上げた「上の列」と「下の列」が、一文字も違わずに一致しているかをチェックします。
ゴール: もし、完全に一致して、かつ全てのピースを使い切ることができれば「クリア」です。

この「積み上げて、後で比べる」というプロセスが、アクションの条件（「今の知識がこうなら、次はこの情報を足せる」）だけで完璧に再現できてしまう。だから、このゲームを解くことは、数学的に不可能な問題に挑むことと同じになってしまうのです。

まとめ：この論文のメッセージ

この論文は、**「ルールが単純だからといって、その先にある未来（プランの存在）が予測できるとは限らない」**ということを、数学の厳密さをもって突きつけました。

「知識」が絡む計画（エピステミック・プランニング）の世界は、私たちが思っている以上に、底知れぬ深さと複雑さを秘めているのです。

論文要約：計画存在問題の決定不能性の証明

1. 背景と問題設定 (Problem)

エピステミック・プランニング (Epistemic Planning, EP) とは、マルチエージェントの知識や信念の状態をモデル化し、特定の目標（ゴール）を達成するためのアクションのシーケンス（計画）を構築する問題です。

本論文が扱う計画存在問題 (Plan Existence Problem) は、以下の要素が与えられたときに、初期エピステミック状態から目標となる論理式を満たす状態へ遷移できるアクションの列が存在するかを問うものです。

初期エピステミック状態: 指標付きクリプキ・モデル (Pointed Kripke model)。
目標 (Goal): マルチエージェント様相論理の論理式。
エピステミック・アクション: 前置条件 (Preconditions) と事後条件 (Postconditions) を持つ。

既存の研究では、前置条件の様相深度（Modal Depth）が深い場合や、事後条件が複雑な場合には決定不能であることが知られていました。しかし、**「前置条件の様相深度が最大1であり、かつ事後条件を持たない」**という非常に制限されたケースにおいて、問題が決定可能か決定不能かは未解決の課題でした。

2. 研究の目的と貢献 (Key Contributions)

本論文の主な貢献は、前置条件の様相深度が最大1で、事後条件が全く存在しないという極めて制約の強い設定においても、計画存在問題は決定不能であることを数学的に証明した点にあります。

具体的には、以下の範囲において決定不能性を証明しました。

単一エージェントの場合: 様相論理 $K$ に基づく場合（負のイントロスペクションを持たない場合）。
マルチエージェントの場合: 様相論理のフレーム条件（反射性、対称性、推移性など）に関わらず。

3. 研究手法 (Methodology)

証明には、決定不能問題として有名な Post's Correspondence Problem (PCP) からの帰着 (Reduction) が用いられています。

帰着の戦略:
PCPのインスタンス（文字列のペアの集合）を、エピステミック・プランニングのインスタンスに変換します。計画のプロセスは以下の2段階で構成されます。

第1段階 (構築フェーズ): エピステミック・アクションを用いて、PCPのブロックを次々と追加し、2つの「パス」（一方は文字列の「上部」、もう一方は「下部」を表現）を構築します。この際、事後条件が使えないため、アクションの適用によってクリプキ・モデルのパス（状態の連鎖）を物理的に伸ばしていく手法をとります。
第2段階 (検証フェーズ): 構築された2つのパスが一致しているかを検証します。アクションを用いて、パスの末尾から1文字ずつ順番に「削除」していき、両方のパスが同時に根（root）まで到達できれば、PCPの解（マッチ）が存在したことになります。

技術的な工夫:

事後条件がないため、状態の遷移を制御するために、様相深度1の論理式を用いた「局所的な」前置条件を巧みに設計しています。
マルチエージェントや、反射性・対称性を持つフレーム（エージェントの知識がより現実的な性質を持つ場合）においても、エージェント間でアクセス関係を交互に切り替える、あるいは状態を複製するなどの手法を用いて、意図しない接続を防ぎつつ、PCPの符号化を維持しています。

4. 結果 (Results)

決定不能性の証明: 前置条件の様相深度 $\le 1$ かつ事後条件なしの条件下で、計画存在問題は決定不能である。
単一エージェントの境界条件: 単一エージェントにおいて、エージェントが負のイントロスペクション（自分が知らないことを知っている性質、すなわち $S5$ 論理など）を持つ場合は、問題は決定可能になることを示しました（これは状態空間が有限に抑えられるためです）。
複雑性の境界: 負のイントロスペクションを持つ単一エージェントの場合、問題は NP に属することを示しました。

5. 意義 (Significance)

本研究は、エピステミック・プランニングにおける「計算の複雑さ」の境界線をより明確にしました。
「アクションによる状態の変化（事後条件）が極めて単純であっても、エージェントの知識の状態（前置条件）をわずかに参照するだけで、計算能力が爆発的に増大し、計算不能な問題へと変貌する」という事実を明らかにしました。これは、実用的なエピステミック・プランニングのアルゴリズムを設計する上で、どの程度の制約を設けるべきかという理論的な指針を与えています。