サイバー防衛 LLM エージェントの安定性を Lean 4 で形式証明──攻撃者の利得を 59% 削減
決定論的ツールと有限アクションカタログを介した制御アーキテクチャにより、LLM の非決定性を排除しつつ ISS 堅牢性を保証。（原題: Stable Agentic Control: Tool-Mediated LLM Architecture for Autonomous Cyber Defense）
リリース: 2026-05-04 · 読了 5 分282 件の実企業攻撃グラフを用いた検証で、Claude Sonnet 4 ベースの制御器が攻撃者の期待利得をベースライン比で 59% 削減した。
Lean 4 を用いてリアプノフ関数を機械チェックし、制御可能性、観測可能性、および入力状態安定性（ISS）堅牢性を数学的に証明した。
4 つの温度設定で行われた 40 回の試行において出力の分散がゼロ（zero variance）であり、LLM 特有の非決定性に左右されない実行安定性を実証した。
Claude Haiku 4.5 のような小規模モデルにおいても、アーキテクチャが規定するアクションカタログの範囲内に挙動が制限される「モデル非依存の安定性」を確認した。
セキュリティ運用（SOC）のような高リスク環境で LLM エージェントを導入する際、非決定的な挙動や暴走を数学的に防ぐ「形式証明」の手法が確立された。
プロンプトによる指示（ソフトな制約）ではなく、制御理論に基づいた「決定論的ツール」を介在させることで、LLM の創造性とシステムの安全性を分離できることを示した。
ハルシネーションや敵対的入力（脱獄）が致命的となるドメインにおいて、エージェントを「信頼できるコンポーネント」として組み込むための設計指針となる。
自律型エージェントを開発するエンジニアは、LLM に直接アクションを実行させる設計を避け、本論文のように「決定論的ツール」と「有限のアクションカタログ」を介在させるべき。これにより、モデルの更新やパラメータ変更に伴う予期せぬ挙動のリスクを数学的に排除できる。
国内固有の追加文脈は限定的（汎用的に有用）。
| Metric | Score | Δ |
|---|---|---|
| Attacker Expected Payoff Reduction (vs Greedy Baseline) | 59 | +59.0 |