VeriGuard: Mejora de la Seguridad de Agentes de LLM mediante Generación de Código Verificado

VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation

October 3, 2025

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

cs.AI

Resumen

El despliegue de agentes autónomos de IA en dominios sensibles, como la atención médica, introduce riesgos críticos para la seguridad, la protección y la privacidad. Estos agentes pueden desviarse de los objetivos del usuario, violar políticas de manejo de datos o ser comprometidos por ataques adversarios. Mitigar estos peligros requiere un mecanismo que garantice formalmente que las acciones de un agente se adhieran a restricciones de seguridad predefinidas, un desafío que los sistemas existentes no abordan completamente. Presentamos VeriGuard, un marco novedoso que proporciona garantías formales de seguridad para agentes basados en LLM mediante una arquitectura de dos etapas diseñada para una corrección robusta y verificable. La etapa inicial fuera de línea implica un proceso de validación exhaustivo. Comienza clarificando la intención del usuario para establecer especificaciones de seguridad precisas. VeriGuard luego sintetiza una política de comportamiento y la somete tanto a pruebas como a verificación formal para demostrar su cumplimiento con estas especificaciones. Este proceso iterativo refina la política hasta que se considera correcta. Posteriormente, la segunda etapa proporciona monitoreo de acciones en línea, donde VeriGuard opera como un monitor en tiempo de ejecución para validar cada acción propuesta por el agente contra la política previamente verificada antes de su ejecución. Esta separación de la validación exhaustiva fuera de línea del monitoreo ligero en línea permite que las garantías formales se apliquen de manera práctica, proporcionando una salvaguarda robusta que mejora sustancialmente la confiabilidad de los agentes 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.