技術要約：AIエージェントのための効率的かつ健全な確率論的検証

問題提起

複雑なデジタル環境における大規模言語モデル（LLM）ベースのAIエージェントのデプロイメントは、エージェントがターミナルやファイルシステムのようなシステムインターフェースへのプログラムによるアクセス権を持つ場合、重大なセキュリティリスクをもたらします。ランタイムモニタリング（参照モニターによる監視）は、セキュリティポリシーを強制するための解決策となりますが、既存のアプローチは決定論的なポリシーに限定されています。実用的なシナリオでは、エージェントは多くの場合、上流のコンポーネント（例：PII（個人識別情報）検知器、リダクションツール、または分類器）に依存しており、これらは固有の失敗率を伴う確率的な出力を生成します。

現在の決定論的なモニターは、これらの曖昧さを扱うために、確率的な出力をバイナリの決定に変換するローカルな閾値を適用することで対処しています。この離散化は、セキュリティとユーティリティ（有用性）の間の脆弱なトレードオフを生み出します。

• 高い閾値は、有害なアクションの阻止漏れ（偽陰性）のリスクを招きます。
• 低い閾値は、安全なアクションの過剰なブロック（偽陽性）のリスクを招きます。
• 独立性の仮定： 標準的な確率推論技術（例：重み付きモデル計数）は、基本的事実が相互に独立していることを仮定することがよくあります。エージェントの設定では、この仮定は頻繁に無効になります。例えば、あるファイルに対するリダクションツールの失敗が、共有されたコンテンツやツールの挙動によって、別のファイルに対する失敗と完全に相関している場合があります。独立性に依存することは、マルチステップのツールチェイニングにおけるリスクを深刻に過小評価することにつながります。

本論文は、連続的な確率的コンテキストを保持し、独立性を仮定することなく述語間の任意の相関を扱い、リアルタイムでポリシー違反の確率に関する厳格かつ健全な上限を提供する検証フレームワークの必要性に取り組んでいます。

メソドロジー

提案されるフレームワークは、エージェントの実行軌跡を分布ロバスト最適化問題としてモデル化します。この手法は、以下の4つのステージで構成されます。

1. 確率的Datalogモデリング

エージェントの実行トレースは、以下の要素を持つDatalogプログラムへとコンパイルされます。

• 基本事実 ($F$): 環境の初期観測（例：「ファイルAにPIIが含まれる」）を表し、ツールの失敗率から導出された限界確率範囲 $[\ell_f, u_f]$ によってパラメータ化されます。
• ルール ($R$): 状態遷移ロジック（例：データの伝播、結合、非機密化）を記述する内延的ルールをエンコードします。
• 導出グラフ: 実行トレースは、事実にノードを持ち、ルールの適用をエッジとする有向非巡回グラフ（DAG）に翻訳されます。著者らは、あらゆるDatalogポリシーの実行は、すべての導出事実が最大2つの親事実（アリティ $\le 2$）に依存するように書き換え可能であることを証明しています。これにより、ロジックを多項式を用いて表現することが可能になります。

2. 正確な最適化定式化（理論的上界）

ポリシー違反のワーストケース確率を計算するために、著者らは結合確率測度の空間における**正確な線形計画法（LP）**を定式化します。

• 目的関数: 不安全な状態（例：機密データが外部の受信者に到達する）に到達する確率を最大化します。
• 制約条件:
  • 構造的一貫性: 測度 $\mu$ は、Datalogルールの決定論的な遷移ロジックに違反する状態に対してゼロの確率を割り当てなければなりません。
  • 限界値の境界: 測度は、基本事実の既知の下限および上限を尊重しなければなりません。
  • 分布ロバスト性: 決定的なことに、この定式化は、明示的に指定されない限り、結合分布（独立性、正の相関、負の相関）に関する仮定を一切行いません。これは、限界値と矛盾しない「ワーストケース」の結合分布を探索します。
• 制限: この正確なLPは指数サイズ（$2^{|V_F|}$）であり、リアルタイムモニタリングにおいては計算量的に困難です。

3. 半正定値計画法（SDP）緩和

実行時の効率性を実現するために、著者らは多項式サイズの半正定値計画法（SDP）緩和を導入します。

• モーメント・トラッキング: 全体の結合分布を最適化する代わりに、SDPは状態分布の一次および二次モーメント（期待値とペアごとの相関）のみを追跡します。
• 線形化: 境界条件から生じる非凸な二次項は、限界区間上の**マコーミック・エンベロープ（McCormick envelopes）**を用いて線形化されます。
• 相関クラス: フレームワークは、特定の述語間の明示的な相関制約（正の相関、負の相関、独立）をサポートしており、ドメイン知識が利用可能な場合には最適化を強化できます。
• 健全性: 著者らは、SDP緩和が真の実行リスクに対する健全な上限（$R^*_{SDP} \ge R^*$）を与えることを証明しています。これにより、時として過剰なブロック（ユーティリティの低下）が発生する場合でも、セキュリティ保証を維持し、決して違反を見逃さないことが保証されます。

4. 実行時強制

計算された上限は、グローバルな安全性閾値 $\tau$ と比較されます。推定リスクが $\tau$ を超える場合、リファレンスモニターは提案されたツール呼び出しをブロックし、そうでなければ実行を許可します。

主な貢献

1. 確率的検証モデル: 曖昧な環境における決定論的エンジンのセキュリティリスクを特定し、早期の二値化を避ける確率的検証モデルを導入したこと。
2. 正確なリスク定式化: マルチステップのエージェント・トラジェクトリをDatalog導出グラフを通じてモデル化し、結合測数上のワーストケース・ポリシー違反リスクの計算を正確な最適化問題として定式化したこと。
3. 健全なSDP緩和: 二次モーメントを追跡してリスクを効率的に近似する、多項式サイズのSDP緩和の導入。本論文は、この緩和が実行リスクの厳密な上限となることを数学的に証明しており、独立性の仮定なしに健全性を確保している。
4. 実証的検証: Intercode-NL2Bash、ATBenchなどのターミナルエージェント・ベンチマーク、およびサイドチャネル脆弱性タスク（Praline）を用いた評価により、従来手法と比較して改善されたセキュリティ・ユーティリティのトレードオフを実証したこと。

結果

本フレームワークは、Praline（相関処理を行う最先端のDatalog推論エンジン）、モンテカルロサンプリング（厳密な独立性を仮定）、および決定論的エンジン（ローカルな閾値を使用）の3つのベースラインと比較して評価されました。

• セキュリティ・ユーティリティのトレードオフ: SDPアプローチは、ユーティリティとセキュリティのトレードオフに関するAUC（曲線下の面積）において、一貫してベースラインを上回りました。
  • vs. モンテカルロ: モンテカルロは高いユーティリティを達成しましたが、独立性の仮定によりワーストケースのリスクを過小評価したため、セキュリティ面で失敗しました（高い偽陰性）。特に、入力が正の相関を持つ場合に顕著でした。
  • vs. Praline: Pralineは完全なセキュリティを実現しましたが、ソルバーのタイムアウトや複雑なタスクにおける緩い境界により、過剰なブロック（低いユーティリティ）を招きました。SDPアプローチは、完全なセキュリティを維持しつつ、より高いユーティリティと低いレイテンシを実現しました。
  • vs. 決定論的: 決定論的エンジンは両方の指標においてパフォーマンスが悪く、閾値処理による情報の損失により、安全でないアクションを阻止できなかったり、安全なアクションをブロックしたりすることが頻繁にありました。
• レイテンシ: SDP緩和は多項式的なスケーラビリティを示しました。IntercodeおよびATBenchのベンチマークにおいて、SDPはベースラインよりも大幅に高速でした（例：IntercodeにおいてPralineの1015msに対し、SDPは221ms）。多くの相関制約を含む複雑なサイドチャネルタスクでは、SDPのレイテンシは増加しましたが、予測可能な範囲内に留まり、正確なSMT推論に伴う指数関数的なテールレイテンシやタイムアウトを回避しました。
• 相関への感度: 実験の結果、入力の相関が増加するにつれ、独立性の仮定（モンテカルロ）は、真のワーストケースの上限がよりタイトである相関設定においてリスクを過大評価し、ユーティリティが急激に低下（偽陽性の増加）することが示されました。SDPフレームワークは、これらの制約に対して効果的に適応しました。

重要性と主張

本論文は、AIエージェントのための検証を決定論的なものから確率的なものへと転換させるパラダイムシフトであると主張しています。その主な意義は、曖昧さが存在する環境において、健全性（厳格なセキュリティ保証）と計算可能性（リアルタイム性能）の間の溝を埋めたことにあります。

• 堅牢性: 分布ロバスト最適化を利用することで、本フレームワークは、述語間の未知の相関に関わらずセキュリティ保証が保持されることを保証します。これは、ツールの失敗が結合している可能性がある実世界の自律エージェントのデプロイメントにおいて、極めて重要な要件です。
• 実用性: SDP緩和により、連続的な確率的入力を伴う複雑なマルチステップ・セキュリティポリシーを、正確な推論の計算量的な困難さや、独立性の仮定による安全性のリスクなしに実行することが可能になります。
• 基盤: 本研究は、ヒューリスティックな防御を超えて、形式的かつ確率的な強制を実現する、自律エージェントを保護するためのスケーラブルな基盤を確立しました。

著者らは、限界についても認めています。具体的には、事実に高度な結合（merging）が発生する非常に長い実行ホライゾンでは、リスク上限が劣化（1.0に収束）する可能性があること、および、エージェントが生成する任意のスクリプトに対しては、定義済みのツールセマンティクスに依存するという点です。しかしながら、本フレームワークは、曖昧な環境で作動する自律エージェントを保護するための、厳格かつスケーラブルな一歩として提示されています。