LeanGuard、Lean4でツール利用エージェントの行動を検証

導入

言語モデルのエージェントが検索、データ更新、外部システムの操作まで担うようになると、安全性は生成された文章だけでは測れません。重要なのは、モデルが提案した操作が実際の環境に到達するかどうかです。プロンプトインジェクションや不適切な引数によって、エージェントがドメインのルールに反する呼び出しを行う可能性は残ります。LeanGuardは、この実行経路に検証層を置き、すべてのツール呼び出しを実行前に確認します。

主なポイント

• 現在の状態と過去の履歴を扱う。 ポリシーはLean4で記述され、状態述語に加えて、範囲を限定した過去時制の時間演算子を利用できます。そのため、現在の引数だけでなく、以前に特定の操作が行われたかどうかも条件にできます。
• 証明できなければ拒否する。 LeanGuardはフェイルクローズで動作し、適合性を確認できない呼び出しを許可しません。判定手続きがLeanLTLの意味論と等価であることも証明されています。
• 拒否後の修正を支援する。 フィードバック方式では、違反したルールとヒントをエージェントに返します。証明誘導型修復では、Leanのメタプログラミングが元の意図に近い代替呼び出しを探索し、その呼び出しがポリシーを満たすことを証明します。
• 禁止操作を実際に止める。 Tau-Benchで0.8Bから27Bまでの5つのQwenモデルを評価したところ、保護なしのエージェントはポリシーが禁止する呼び出しを少なくとも33回実行しました。一方、LeanGuardはそれらを許可しませんでした。フィードバックを加えてもタスク成功率は大きく変わらず、拒否された呼び出しの反復は減少しました。
• プロンプトインジェクションにも効果。 DTapでは直接的なプロンプトインジェクションの成功率が57.9%から5.9%に低下しました。正常タスクで書き込みが不要な通信シナリオでは、良性タスクの成功率は変わりませんでした。引数値が原因となった拒否の再生では、252件中88件で許可可能な編集を証明でき、中央値の処理時間は2ミリ秒でした。

意義と課題

LeanGuardの重要性は、モデルを完全に正しくすることではなく、モデルの提案と環境での実行を分離する点にあります。モデルは意図理解や計画を担当し、Lean4で定義されたポリシーが、現在の状態と履歴において実行を許可するかを判断します。口座変更やデータ書き込みなど、誤操作の影響が大きい用途で有効な分担です。

ただし、形式検証はポリシー自体の妥当性を自動的に保証しません。ポリシーの網羅性、ツールのスキーマ変更、検証遅延、拒否後の再試行コストは運用側の課題として残ります。今回の結果は実行前検証の有効性を示しますが、システムの変化に合わせてポリシーを見直す必要性をなくすものではありません。

それでも、プロンプトだけに依存した制御や事後監査に比べ、実行境界で保守的かつ監査可能な判定を行う設計は、エージェントを実システムへ接続する際の有力な方向性です。

出典：Hugging Face Daily Papers