SEVerA: Síntesis Verificada de Agentes Autoevolutivos

SEVerA: Verified Synthesis of Self-Evolving Agents

March 26, 2026

Autores: Debangshu Banerjee, Changming Xu, Gagandeep Singh

cs.AI

Resumen

Los avances recientes han demostrado la efectividad de agentes de LLM auto-evolutivos en tareas como la reparación de programas y el descubrimiento científico. En este paradigma, un LLM planificador sintetiza un programa de agente que invoca modelos paramétricos, incluidos LLMs, los cuales luego se ajustan por tarea para mejorar el rendimiento. Sin embargo, los marcos de agentes auto-evolutivos existentes no ofrecen garantías formales de seguridad o corrección. Dado que tales programas a menudo se ejecutan de forma autónoma con entradas no vistas, esta falta de garantías plantea problemas de confiabilidad y seguridad. Formulamos la generación de código agéntico como un problema de aprendizaje con restricciones, combinando especificaciones formales estrictas con objetivos flexibles que capturan la utilidad de la tarea. Introducimos los Modelos Generativos con Guardas Formales (FGGM), que permiten al LLM planificador especificar un contrato formal de salida para cada llamada a un modelo generativo utilizando lógica de primer orden. Cada llamada FGGM encapsula el modelo subyacente en un muestreador por rechazo con una alternativa verificada, garantizando que cada salida devuelta satisfaga el contrato para cualquier entrada y configuración de parámetros. Basándonos en FGGM, presentamos SEVerA (Agentes Verificados Auto-Evolutivos), un marco de tres etapas: Búsqueda sintetiza programas paramétricos candidatos que contienen llamadas FGGM; Verificación demuestra la corrección con respecto a las restricciones estrictas para todos los valores de los parámetros, reduciendo el problema a un aprendizaje sin restricciones; y Aprendizaje aplica una optimización escalable basada en gradientes, incluyendo ajuste fino estilo GRPO, para mejorar el objetivo flexible preservando la corrección. Evaluamos SEVerA en verificación de programas Dafny, síntesis de matemáticas simbólicas y uso de herramientas agénticas compatibles con políticas (τ²-bench). En todas las tareas, SEVerA logra cero violaciones de restricciones mientras mejora el rendimiento respecto a líneas base no restringidas y de vanguardia (SOTA), demostrando que las restricciones formales de comportamiento no solo garantizan la corrección, sino que también dirigen la síntesis hacia agentes de mayor calidad.

English

Recent advances have shown the effectiveness of self-evolving LLM agents on tasks such as program repair and scientific discovery. In this paradigm, a planner LLM synthesizes an agent program that invokes parametric models, including LLMs, which are then tuned per task to improve performance. However, existing self-evolving agent frameworks provide no formal guarantees of safety or correctness. Because such programs are often executed autonomously on unseen inputs, this lack of guarantees raises reliability and security concerns. We formulate agentic code generation as a constrained learning problem, combining hard formal specifications with soft objectives capturing task utility. We introduce Formally Guarded Generative Models (FGGM), which allow the planner LLM to specify a formal output contract for each generative model call using first-order logic. Each FGGM call wraps the underlying model in a rejection sampler with a verified fallback, ensuring every returned output satisfies the contract for any input and parameter setting. Building on FGGM, we present SEVerA (Self-Evolving Verified Agents), a three-stage framework: Search synthesizes candidate parametric programs containing FGGM calls; Verification proves correctness with respect to hard constraints for all parameter values, reducing the problem to unconstrained learning; and Learning applies scalable gradient-based optimization, including GRPO-style fine-tuning, to improve the soft objective while preserving correctness. We evaluate SEVerA on Dafny program verification, symbolic math synthesis, and policy-compliant agentic tool use (τ^2-bench). Across tasks, SEVerA achieves zero constraint violations while improving performance over unconstrained and SOTA baselines, showing that formal behavioral constraints not only guarantee correctness but also steer synthesis toward higher-quality agents.