SEVerA: Síntese Verificada de Agentes Autoevolutivos

SEVerA: Verified Synthesis of Self-Evolving Agents

March 26, 2026

Autores: Debangshu Banerjee, Changming Xu, Gagandeep Singh

cs.AI

Resumo

Avanços recentes demonstraram a eficácia de agentes de LLM que evoluem autonomamente em tarefas como correção de programas e descoberta científica. Neste paradigma, um LLM planeador sintetiza um programa de agente que invoca modelos paramétricos, incluindo LLMs, que são subsequentemente ajustados por tarefa para melhorar o desempenho. No entanto, as arquiteturas existentes de agentes auto-evolutivos não fornecem garantias formais de segurança ou correção. Como estes programas são frequentemente executados de forma autónoma em entradas não vistas, esta falta de garantias levanta preocupações de fiabilidade e segurança. Nós formulamos a geração de código agente como um problema de aprendizagem com restrições, combinando especificações formais rígidas com objetivos flexíveis que capturam a utilidade da tarefa. Introduzimos os Modelos Generativos Formalmente Guardados (FGGM), que permitem ao LLM planeador especificar um contrato formal de saída para cada chamada de modelo generativo usando lógica de primeira ordem. Cada chamada FGGM encapsula o modelo subjacente num amostrador de rejeição com um *fallback* verificado, garantindo que cada resultado devolvido satisfaz o contrato para qualquer entrada e configuração de parâmetros. Com base nos FGGM, apresentamos o SEVerA (Agentes Verificados Auto-Evolutivos), uma arquitetura de três fases: Pesquisa sintetiza programas paramétricos candidatos contendo chamadas FGGM; Verificação prova a correção em relação a restrições rígidas para todos os valores dos parâmetros, reduzindo o problema a uma aprendizagem sem restrições; e Aprendizagem aplica uma optimização escalável baseada em gradientes, incluindo *fine-tuning* do estilo GRPO, para melhorar o objetivo flexível, preservando a correção. Avaliamos o SEVerA na verificação de programas Dafny, na síntese de matemática simbólica e no uso de ferramentas agentes em conformidade com políticas (τ^2-bench). Através das tarefas, o SEVerA alcança zero violações de restrições enquanto melhora o desempenho face a linhas de base não restritas e de estado da arte, mostrando que as restrições comportamentais formais não só garantem a correção, como também orientam a síntese na direção de agentes de maior qualidade.

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.