技術的概要：AI ワークフローアーキテクチャのための効果透過的ガバナンス

問題定義

AI ワークフローシステムが、大規模言語モデル（LLM）へのクエリ、状態管理、外部ツールの呼び出しなどを通じて、現実世界で動作するようになるにつれ、安全でないまたは許可されていない動作を防ぐためのガバナンスメカニズムの必要性が高まっている。この分野では、ガバナンスは必然的に能力とのトレードオフを伴うという一般的な仮定がなされている。すなわち、安全性を高めるために意図された制限は、システムが示し得る行動の空間を縮小すると考えられている。本論文は、この仮定に異議を唱え、内部計算を変更したり出力を事後処理したりするのではなく、効果境界においてガバナンスを課すというアーキテクチャ的代替案を形式化する。ここで扱われる中心的な意味論的問いは、ガバナンスが許可されたプログラムが計算するものを改变するかどうかである。

手法

著者らは、Rocq 8.19（旧 Coq）証明支援器内におけるインタラクション木（Interaction Trees）を用いた、構造的にガバナンスされた AI ワークフローアーキテクチャの機械検証された形式化を提示する。この開発は、36 のモジュール、12,000 行のコード、454 の定理から構成され、承認された補題（admitted lemmas）はゼロである。

中核的な形式化

1. インタラクション木（ITrees）：プログラムは、イベント型 $E$ 上の共帰納的木としてモデル化される。これは Ret(v)、Tau(t)、または Vis(e, k) として定義される。これにより、再帰的および不純なプログラムの表現が可能となる。
2. 指示イベント型：システムは、プリミティブな機能（計算モルフィズム、メモリ操作、オラクル（LLM）呼び出し、外部ツール呼び出し、観測イベント）のコンストラクタを含む DirectiveE 型を定義する。
3. ガバナンス演算子（$G$）：ガバナンスは、代数的効果ハンドラの伝統に従い、効果解釈をラップするものとして実装される。演算子 $G(h)$ は、基底ハンドラ $h$ によって発行されるすべての指示を仲介する。これは事前チェック（信頼、権限、フェーズ検証）と事後計装（出所、観測性）を実行する。チェックが失敗した場合、実行は ITree.spin を介して発散し、成功した場合、指示は基盤となるハンドラに委任される。
4. 安全性述語：安全性は、パラメータ付き共帰納法（paco）を用いた共帰納的述語 gov_safe によって定義される。この述語は、ガバナンスのみのイベント（常に許可される）と、明示的な承認を必要とする実際の I/O イベントを区別する。

主要な貢献と結果

本論文は、ガバナンスと計算表現性が直交する次元であることを証明する 7 つの主要な性質（P1–P7）を確立する。

1. 意味論的透過性（中核定理）

中核的な貢献は、意味論的透過性を証明する機械検証された定理である。ガバナンスチェックが成功するすべての実行において、ガバナンスされた解釈は（ガバナンスのみのイベントを除き）、ガバナンスされていない解釈と観測的に同等である。

• 含意：許可されたプログラムは、ガバナンスなしの場合と全く同じ部分関数を計算し、同じ到達可能な戻り値を生成する。ガバナンスは、許可されたパスの内部計算を変更することなく、効果の境界を制約する。

2. ガバナンスされた表現性（P1 および P2）

著者らは、ガバナンスラッパーが計算能力を低下させないことを証明する。

• ガバナンスされたチューリング完全性：システムはガバナンス下でもチューリング完全性を維持する。レジスタマシンプログラムは、表現性の損失なしにガバナンスされたインタラクション木に変換できる。
• ガバナンスされたオラクル表現性：このアーキテクチャは、ガバナンス下でのオラクル拡張（LLM クエリ）をサポートし、複雑な推論ワークフローをモデル化する能力を維持する。

3. 決定可能性の境界（P3）

本論文は、ガバナンスが決定できることとできないことの厳密な境界を形式化する。

• ガバナンス述語：これらは構造的、構文論的、全関数的であり、ブール合成（AND、OR、NOT）に対して閉じている。これらは信頼レベルや機能クラスなどの性質を決定できる。
• 意味論的性質：停止性などのプログラム性質は非自明であり、ガバナンスによって決定不可能である。本論文は、2 つのプログラムが同一の指示構造（したがってガバナンスチェックをパスする）を共有しつつも、グローバルな終了動作において異なる場合があり得るため、ガバナンスが停止性を決定できないことを証明する。これは、構造的境界に適用されたライス定理と整合する。

4. 表現的必要性（P5）

著者らは、プリミティブな機能（計算、メモリ、推論、外部呼び出し、観測性）の集合が必要最小限であることを証明する。

• 厳密な階層：機能は厳密な連鎖を形成する：コード < コード＋メモリ < コード＋メモリ＋推論 < コード＋メモリ＋推論＋呼び出し。
• 必要性：任意の単一のプリミティブ機能を除去すると、システムの表現力が厳密に低下する。例えば、メモリ指示はチューリング完全性のために構造的に必要であり、LLMCall 指示はオラクル拡張のために必要である。

5. 包含の非対称性（P6）

本論文は、構造的ガバナンスとコンテンツレベルのフィルタリングの間に厳密な分離を確立する。

• 構造的はコンテンツを包含する：構造的ガバナンスは、コンテンツフィルタリングを厳密に包含する。解釈境界において効果を仲介することにより、構造的ガバナンスは許可されていない I/O イベントの発生を防ぐ。
• コンテンツは構造的を包含しない：コンテンツフィルタ（例えば、出力書き換え）は値を変更し得るが、許可されていない効果ステップの発生を防ぐことはできない。したがって、コンテンツフィルタリングのみでは効果安全性を意味しない。

6. 目標の維持（P4）

ガバナンスが許可するすべての実行において、システムはプログラムの目標を維持する。あるプログラムが特定の戻り値 $v$ に到達するように設計されており、ガバナンスチェックが通過する場合、ガバナンスされた実行は $v$ に到達する。

7. 拒否による安全性（活性対安全性）

ガバナンスチェックが失敗した場合、システムは安全性のために活性を犠牲にする。実行は誤った結果を生成するのではなく、発散（spin）する。システムは、許可されていない効果が決して発生せず、「安全でない」戻り値が決して生成されないことを保証する。

意義と範囲

本論文は、ガバナンスと計算表現性が直交することを実証すると主張する。ガバナンスは、許可されたトレースにおける意味論を変更したり、内部計算表現性を低下させたりすることなく、プログラムの効果境界を制約するために課すことができる。

• 信頼境界：保証は、Rocq カーネル、インタラクション木ライブラリ、および $G$ 演算子のランタイム実装からなる信頼計算基盤（TCB）に対して相対的に成り立つ。本論文は、検証済みコンパイラ（CompCert）や OS カーネル（seL4）との類似性を指摘し、形式モデルと展開されたランタイムの間のギャップは、テスト（70,000 件以上の生成シーケンスに対して検証済み）によって埋められていると述べる。
• 限界：透過性定理は許可された実行にのみ適用され、拒否された実行は発散する。このモデルは、リソース枯渇、スケジューリング、確率的モデルの動作を抽象化している。定理は抽象アーキテクチャとインタプリタに適用されるものであり、コンパイルされたバイナリに対するエンドツーエンドの保証ではない。

この研究は、意味論的透過性、表現的必要性、および形式的決定可能性境界を追加することで、McCann [2026b, 2026e] の以前の機械化された開発を拡張し、AI システムにおける「効果透過的ガバナンス」のための厳密な基盤を提供する。