概要: 構造的に統治されるAIワークフロー・アーキテクチャの機械検証された形式化を提示し、効果レベルの統治を課しても内部の計算的な表現力を低下させずに済むことを証明します。Rocq 8.19におけるInteraction Treesを用いて、メモリアクセス、外部呼び出し、オラクル（LLM）への問い合わせを含む、あらゆる効果的な指令を仲介する統治演算子Gを定義します。開発は0個の認められた補題（admitted lemmas）でコンパイルされ、36モジュール、約12,000行のRocq、454の定理から成ります。次の7つの性質を確立します：(P1) 統治されたチューリング完全性、(P2) 統治されたオラクル表現力、(P3) 決定可能性の境界：統治述語が全称であり、かつブールの合成に対して閉じている一方で、意味論的なプログラム性質は統治によって非自明のままであり、統治により決定不能である、(P4) 許可された実行に対する目標の保存、(P5) 原始的能力（計算、メモリ、推論、外部呼び出し、観測可能性）の表現力における最小性、(P6) 吸収の非対称性：構造的統治が内容レベルのフィルタリングを厳密に包含することを示す、(P7) 意味論的透明性：統治が許可するすべての実行において、統治された解釈は（統治のみのイベントを除いた上で）統治されていない解釈と観測的に同等です。これらの結果から、統治と計算的表現力は直交する次元であることが示されます。統治はプログラムの効果境界を制約しますが、内部計算に対しては意味論的に透明なままです。
効果の可視性を保つAIワークフロー・アーキテクチャのガバナンス：意味保存、表現の最小性、決定可能性の境界
arXiv cs.AI / 2026/5/5
💬 オピニオンIdeas & Deep AnalysisModels & Research
要点
- この論文は、メモリアクセス、外部呼び出し、LLM（オラクル）クエリといった効果的な指示を統制する、効果の透明性を保ったAIワークフロー・アーキテクチャのガバナンス枠組みを機械検証で提示します。
- Rocq 8.19のInteraction Treesを用いてガバナンス演算子Gを定義し、認められた補題（admitted lemmas）0件の完全検証を、36モジュール・約12,000行・454の定理として報告しています。
- 著者らは、ガバナンスを課しても内部の計算能力（表現力）が損なわれないことを証明し、「ガバナンス付き」チューリング完全性やガバナンス付きのオラクル表現力も含めて示します。
- 決定可能性の境界として、ガバナンス述語は全体でありBoolean合成に閉じている一方で、意味論的なプログラム性質は非自明であり、ガバナンス下でもなお決定不能であることを明らかにします。
- 許可された実行における目標の保存、原始能力（計算・メモリ・推論・外部呼び出し・観測）の表現の最小性、コンテンツレベルのフィルタリングに対する厳密な包含関係、そしてガバナンス固有のイベントを除いた観測可能な同値性による意味の透明性も示されます。
