VeriGuard: Повышение безопасности агентов на основе больших языковых моделей через верифицированную генерацию кода

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

Аннотация

Развертывание автономных ИИ-агентов в чувствительных областях, таких как здравоохранение, влечет за собой серьезные риски для безопасности, защиты и конфиденциальности. Эти агенты могут отклоняться от целей пользователя, нарушать политики обработки данных или быть скомпрометированы атаками злоумышленников. Для снижения этих угроз необходим механизм, который формально гарантирует, что действия агента соответствуют заранее заданным ограничениям безопасности, — задача, которую существующие системы не решают в полной мере. Мы представляем 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.