VeriGuard: Verbetering van de veiligheid van LLM-agents via geverifieerde codegeneratie

VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation

October 3, 2025

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

cs.AI

Samenvatting

De inzet van autonome AI-agenten in gevoelige domeinen, zoals de gezondheidszorg, brengt kritieke risico's met zich mee voor veiligheid, beveiliging en privacy. Deze agenten kunnen afwijken van gebruikersdoelen, gegevensverwerkingsbeleid schenden of worden gecompromitteerd door adversariële aanvallen. Het beperken van deze gevaren vereist een mechanisme om formeel te garanderen dat de acties van een agent voldoen aan vooraf gedefinieerde veiligheidsbeperkingen, een uitdaging die bestaande systemen niet volledig aanpakken. Wij introduceren VeriGuard, een nieuw raamwerk dat formele veiligheidsgaranties biedt voor op LLM gebaseerde agenten via een dual-stage architectuur die is ontworpen voor robuuste en verifieerbare correctheid. De initiële offline fase omvat een uitgebreid validatieproces. Het begint met het verhelderen van de gebruikersintentie om nauwkeurige veiligheidsspecificaties vast te stellen. VeriGuard synthetiseert vervolgens een gedragsbeleid en onderwerpt dit aan zowel testen als formele verificatie om de naleving van deze specificaties te bewijzen. Dit iteratieve proces verfijnt het beleid totdat het als correct wordt beschouwd. Vervolgens biedt de tweede fase online actiemonitoring, waarbij VeriGuard fungeert als een runtime-monitor om elke voorgestelde agentactie te valideren tegen het vooraf geverifieerde beleid voordat deze wordt uitgevoerd. Deze scheiding van de uitgebreide offline validatie en de lichtgewicht online monitoring maakt het mogelijk om formele garanties praktisch toe te passen, wat een robuuste bescherming biedt die de betrouwbaarheid van LLM-agenten aanzienlijk verbetert.

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.