技術的概要：形式手法と大規模言語モデル（LLM）の融合

問題定義

本論文は、AI ガバナンスにおける重要なギャップ、すなわち、AI 搭載製品およびサービスの開発ライフサイクル全体を通じて、それらを監視、監査、介入するための堅牢なメカニズムの欠如という課題に取り組んでいます。フロンティア AI モデルの安全性に向けた多大な努力（安全性フレームワークやレッドチーム化など）が払われている一方で、中小企業（SME）やサードパーティ開発者は、展開されたブラックボックス AI システム（具体的には大規模言語モデル、LLM）が製品固有、業界固有、および管轄区域固有の規制に準拠していることを保証するためのツールを欠いていることが多く見られます。

特定された核心的な課題は、多くのコンプライアンス要件が時間的に拡張されたものであることです。これらは、イベント間の関係が時間を跨ぐ行動制約であり、「請求書を受領した場合、最終的に支払われなければならない」や「支払いが確認されるまで製品を発送してはならない」などがその例です。著者らは、現在の監査におけるLLM を裁判官として用いる手法への依存は不十分であると主張しています。なぜなら、LLM はイベント間の時間間隔が変動する場合、制約の数が増加する場合、または各ステップにおける命題の数が増加する場合など、これらの時間的パターンについての推論に苦慮するからです。

手法

著者らは、形式手法（具体的には線形時間論理、LTL）と機械学習を橋渡しし、ブラックボックスの監視および監査システムを構築するフレームワークを提案します。核心的なアプローチは、問題を分解することです。すなわち、LLM を用いてイベントをラベル付けし（非構造化テキストから原子命題を抽出）、形式論理を用いてこれらのイベントの系列に対して推論を行うというものです。

TRAC フレームワーク

著者らは、ブラックボックス AI システム向けに設計されたアルゴリズムのファミリーである**TRAC（Temporal Rule Assessment and Compliance：時間的ルールの評価とコンプライアンス）**を導入します。

1. ラベル付け関数 ($L$): LLM（または他の分類器）が入出力の系列を、特定の時間ステップにおいて真となる命題記号（原子事実）の集合にマッピングします。
2. LTL 進行（Progression）: 制約を静的なオートマトンにコンパイルする代わりに、システムはLTL 進行を使用します。この技術は、現在の真理値割り当て $\sigma_t$ に基づいて LTL 式 $\psi$ を書き換え、トレースの残りに対して何が成り立たなければならないかを記述する残余式 $\psi_{t+1}$ を生成します。
   • これにより、時間的性質の動的かつ漸進的な評価が可能になります。
   • 制約の記号構造を保持し、違反が発生した理由を説明する解釈可能な「証人（witness：実行トレース）」の生成を可能にします。
3. アルゴリズム:
   • TRAC: リアルタイム監視とオフライン監査のための基本アルゴリズムです。判定（違反、満足、または未確定）と証人を出力します。
   • TRACR（TRAC with Reset）: 継続的監視を処理するために TRAC を拡張したものです。違反または満足が検出された場合、システムは式を初期状態にリセットし、その後の違反を検出できるようにします（ノイズの多い環境や反復タスクに有用です）。
   • TRACP+I（TRAC with Predictive and Intervening capabilities：予測および介入機能を備えた TRAC）:
     • 予測的監視: サンプルベースの手法を用いて、地平線 $k$ 内での将来の違反の確率を推定します。
     • 介入: 予測されたリスクが閾値を超えた場合、システムはブラックボックス介入をトリガーします。戦略には以下が含まれます：
       • 拒否サンプリング: 準拠した出力が見つかるまでモデルの出力を再サンプリングします。
       • 制約誘導型プロンプティング: 残余 LTL 式（自然言語で）をプロンプトに注入し、モデルを誘導します。
       • モデル置換: 出力を生成するために、より安全な代替モデルに切り替えます。

主要な貢献

1. 数学的フレームワーク: 自然言語または形式論理（LTL）で表現されたユーザー指定の行動要件に対するブラックボックス AI システムの評価のための形式的定義。
2. TRAC アルゴリズム: LTL 進行を活用して違反を検出、発生源を特定し、説明可能な証人を提供するアルゴリズム群（TRAC、TRACR、TRACP+I）。本論文は、完全なラベル付け関数の条件下において、LTL 進行に基づくアルゴリズムの健全性を証明しています。
3. LLM 裁判官への優位性: 時間的に拡張された違反の検出において、TRAC が LLM を裁判官としたベースラインを大幅に上回ることを示す実証的証拠。特筆すべきは、TRAC フレームワーク内でラベル付けに使用されるより小規模なモデルが、スタンドアロンの裁判官として機能するフロンティア LLM と同等かそれ以上の性能を発揮することです。
4. 予測的および介入的監視: 能動的介入を通じて LLM ベースのエージェントの違反率を削減し、タスク性能を大幅に低下させることなく実装する TRACP+I の導入。
5. LLM の限界の特性評価: 以下の要因に伴い、LLM の時間的推論精度が予測可能に低下することを示す統制実験：
   • 関連イベント間の距離の増加（時間的弾力性）。
   • 同時制約数の増加。
   • 時間ステップあたりの命題数の増加。

実験結果

著者らは、3 つの環境（物流計画のIPC-Trucks、調理タスクのTextWorld、科学的推論のScienceWorld）において、自らのアプローチを評価しました。

• 監査性能: 監査タスクにおいて、**TRACR + LLM（ラベル付け器として）**がすべての環境で最高 F1 スコアを達成しました。Qwen-7B などの小規模なラベル付けモデルを TRACR と組み合わせた場合でも、ゼロショットまたはフューショット裁判官として使用された大規模なフロンティアモデル（GPT-4.1、Gemini-2.5-Pro など）を上回りました。
• 時間的推論の限界: 合成トレースを用いた実験により、LLM が時間的パターンに苦慮することが確認されました。単純な式において、イベント間のギャップが増加するにつれて（小規模モデルで約 10 ステップからフロンティアモデルで約 1000 ステップへ）、また式の複雑さ（制約数/命題数）が増加するにつれて、精度は著しく低下しました。
• 介入の有効性: TRACP+Iフレームワークは、すべてのモデルおよび環境において制約違反率を成功裡に削減しました。介入（再サンプリング、プロンプティング、置換）は、ベースラインと同等のタスク性能（累積報酬）を維持しつつ、エージェントをコンプライアンスへと効果的に誘導しました。

意義と主張

本論文は、古典的な形式手法が AI 監視において依然として価値があると主張していますが、言語ベースのシステムに適応させる必要があるとしています。主な意義は、提案された分解戦略にあります。すなわち、意味的ラベル付け（命題の抽出）における LLM の強みを活用しつつ、時間的パターンに対する推論における形式手法（LTL 進行）の強みに依存するという戦略です。

著者らは、このアプローチが以下の点において重要であると強調しています。

• フロンティアモデルに必要な予算なしに、コンプライアンス監査をアクセス可能にする。
• 証人を通じた解釈可能性を提供し、デバッグと説明責任に不可欠である。
• 予測的監視と介入を通じて能動的ガバナンスを可能にし、事後診断を超えて前進させる。
• 事前展開評価がしばしば不十分な領域である、長期的な地平線にわたって行動が進化するエージェント型 AI システムの特定のガバナンス課題に対処する。

論文は、限界に対する控え目な認識で締めくくられています。ブラックボックス監視はすべての失敗モードを検出できず、ラベル付け関数は誤りを導入する可能性があり、曖昧な自然言語要件を正確な LTL 式へ翻訳することは、「形式主義の罠」に直面する社会技術的課題であるとしています。最終的に、TRAC は、より広範な AI 説明責任のエコシステム内で展開可能なツールとして提示されています。