VeriGuard: Aprimorando a Segurança de Agentes de LLM por meio de Geração 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
Resumo
A implantação de agentes de IA autônomos em domínios sensíveis, como a área da saúde, introduz riscos críticos à segurança, proteção e privacidade. Esses agentes podem desviar-se dos objetivos do usuário, violar políticas de manipulação de dados ou serem comprometidos por ataques adversariais. Mitigar esses perigos exige um mecanismo para garantir formalmente que as ações de um agente estejam em conformidade com restrições de segurança predefinidas, um desafio que os sistemas existentes não abordam completamente. Apresentamos o VeriGuard, uma estrutura inovadora que fornece garantias formais de segurança para agentes baseados em LLM (Large Language Models) por meio de uma arquitetura de duplo estágio projetada para robustez e correção verificável. O estágio inicial offline envolve um processo abrangente de validação. Ele começa esclarecendo a intenção do usuário para estabelecer especificações de segurança precisas. O VeriGuard então sintetiza uma política comportamental e a submete a testes e verificação formal para comprovar sua conformidade com essas especificações. Esse processo iterativo refina a política até que ela seja considerada correta. Posteriormente, o segundo estágio fornece monitoramento online de ações, onde o VeriGuard atua como um monitor em tempo de execução para validar cada ação proposta pelo agente em relação à política pré-verificada antes da execução. Essa separação entre a validação offline exaustiva e o monitoramento online leve permite que garantias formais sejam aplicadas de forma prática, fornecendo uma salvaguarda robusta que melhora substancialmente a confiabilidade dos 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.