VeriGuard: 検証済みコード生成によるLLMエージェントの安全性向上

VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation

October 3, 2025

著者: Lesly Miculicich, Mihir Parmar, Hamid Palangi, Krishnamurthy Dj Dvijotham, Mirko Montanari, Tomas Pfister, Long T. Le

cs.AI

要旨

医療などの機密性の高い領域における自律型AIエージェントの導入は、安全性、セキュリティ、プライバシーに重大なリスクをもたらします。これらのエージェントは、ユーザーの目的から逸脱したり、データ処理ポリシーに違反したり、敵対的攻撃によって侵害されたりする可能性があります。こうした危険を軽減するためには、エージェントの行動が事前に定義された安全制約に準拠していることを正式に保証するメカニズムが必要であり、これは既存のシステムでは完全に対応できていない課題です。本論文では、VeriGuardという新しいフレームワークを紹介します。このフレームワークは、堅牢で検証可能な正確性を実現するための二段階アーキテクチャを通じて、LLMベースのエージェントに正式な安全性保証を提供します。最初のオフライン段階では、包括的な検証プロセスが行われます。まず、ユーザーの意図を明確化して正確な安全仕様を確立します。その後、VeriGuardは行動ポリシーを合成し、テストと正式な検証を実施して、これらの仕様に準拠していることを証明します。この反復プロセスにより、ポリシーが正しいと判断されるまで洗練されます。続く第二段階では、オンラインでの行動監視が行われ、VeriGuardは実行前に各提案されたエージェントの行動を事前に検証済みのポリシーに対して検証するランタイムモニターとして機能します。このように、徹底的なオフライン検証と軽量なオンラインモニタリングを分離することで、正式な保証を実用的に適用することが可能になり、LLMエージェントの信頼性を大幅に向上させる堅牢な保護を提供します。

English

The deployment of autonomous AI agents in sensitive domains, such as healthcare, introduces critical risks to safety, security, and privacy. These agents may deviate from user objectives, violate data handling policies, or be compromised by adversarial attacks. Mitigating these dangers necessitates a mechanism to formally guarantee that an agent's actions adhere to predefined safety constraints, a challenge that existing systems do not fully address. We introduce VeriGuard, a novel framework that provides formal safety guarantees for LLM-based agents through a dual-stage architecture designed for robust and verifiable correctness. The initial offline stage involves a comprehensive validation process. It begins by clarifying user intent to establish precise safety specifications. VeriGuard then synthesizes a behavioral policy and subjects it to both testing and formal verification to prove its compliance with these specifications. This iterative process refines the policy until it is deemed correct. Subsequently, the second stage provides online action monitoring, where VeriGuard operates as a runtime monitor to validate each proposed agent action against the pre-verified policy before execution. This separation of the exhaustive offline validation from the lightweight online monitoring allows formal guarantees to be practically applied, providing a robust safeguard that substantially improves the trustworthiness of LLM agents.