構造化ガバナンスの機械化された基盤：統治されたインテリジェンスに対する機械チェック可能な証明

arXiv cs.AI / 2026/5/1

📰 ニュースDeveloper Stack & InfrastructureIdeas & Deep AnalysisModels & Research

原文を読む →

共有:

要点

この論文は、認知ワークフローシステムに対する「構造化ガバナンス」に関する5つの結果を提示し、そのうち3つはCoq 8.19でInteraction Treesライブラリを用いて機械化され、残り2つは論文上で証明されています。
共帰納的な安全性述語（gov_safe）を導入し、無限のプログラム挙動に対するガバナンスの安全性を捉えます。さらに許可フラグでインデックス付けし、未統治のI/Oでは偽、統治された解釈では真であることが機械的に証明されています。
ガバナンスの不変性定理により、ガバナンスがメタ再帰的な「タワー」全体で一様であり、レベルn+1のガバナンスが型の定義的等価性によってレベルnのガバナンスへ還元されることが示されます。また十分性定理により、4つのプリミティブ（code, reason, memory, call）が離散的なインテリジェントシステム全般を表現し尽くせることが（クライスリ圏の随伴的閉包として）証明されます。
Alternating Normal Formでは、機械を「交互のコード層と効果層」に分解する正規形を与え、収束性のある書き換えシステムによってそれが保証されます。さらに必要性定理では、秘匿的な「reason」プリミティブが意味判断を要する問題に数学的に必須であることが、Riceの定理への還元を通じて論じられます。
6つ目の貢献として、BEAMランタイム向けのVerified Interpreter SpecificationをCoqで形式化し、70,000件超のランダムなディレクティブ列に対するプロパティベーステストで実行系を検証したところ、相違はゼロでした。