VeriGuard : Amélioration de la sécurité des agents LLM grâce à la génération de code vérifié

VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation

October 3, 2025

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

cs.AI

papers.abstract

Le déploiement d'agents d'IA autonomes dans des domaines sensibles, tels que les soins de santé, introduit des risques critiques pour la sécurité, la sûreté et la confidentialité. Ces agents peuvent s'écarter des objectifs de l'utilisateur, enfreindre les politiques de gestion des données ou être compromis par des attaques adverses. Atténuer ces dangers nécessite un mécanisme permettant de garantir formellement que les actions d'un agent respectent des contraintes de sécurité prédéfinies, un défi que les systèmes existants ne parviennent pas à relever pleinement. Nous présentons VeriGuard, un cadre novateur qui offre des garanties de sécurité formelles pour les agents basés sur des modèles de langage (LLM) grâce à une architecture en deux étapes conçue pour une robustesse et une vérifiabilité accrues. La première étape, hors ligne, implique un processus de validation approfondi. Elle commence par clarifier l'intention de l'utilisateur pour établir des spécifications de sécurité précises. VeriGuard synthétise ensuite une politique comportementale et la soumet à des tests ainsi qu'à une vérification formelle pour prouver sa conformité à ces spécifications. Ce processus itératif affine la politique jusqu'à ce qu'elle soit jugée correcte. Par la suite, la deuxième étape assure une surveillance en ligne des actions, où VeriGuard fonctionne comme un moniteur en temps réel pour valider chaque action proposée par l'agent par rapport à la politique pré-vérifiée avant son exécution. Cette séparation entre la validation exhaustive hors ligne et la surveillance légère en ligne permet d'appliquer pratiquement des garanties formelles, offrant ainsi une sauvegarde robuste qui améliore considérablement la fiabilité des agents 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.