SEVerA: Sintesi Verificata di Agenti Auto-Evolutivi
SEVerA: Verified Synthesis of Self-Evolving Agents
March 26, 2026
Autori: Debangshu Banerjee, Changming Xu, Gagandeep Singh
cs.AI
Abstract
Recenti progressi hanno dimostrato l'efficacia di agenti LLM auto-evolventi in compiti come la riparazione di programmi e la scoperta scientifica. In questo paradigma, un LLM pianificatore sintetizza un programma agente che richiama modelli parametrici, inclusi gli LLM, che vengono poi sintonizzati per ogni specifico compito per migliorare le prestazioni. Tuttavia, i framework esistenti per agenti auto-evolventi non forniscono garanzie formali di sicurezza o correttezza. Poiché tali programmi sono spesso eseguiti autonomamente su input non visti, questa mancanza di garanzie solleva preoccupazioni di affidabilità e sicurezza. Noi formuliamo la generazione di codice agentivo come un problema di apprendimento vincolato, combinando specifiche formali rigide (hard) con obiettivi flessibili (soft) che catturano l'utilità del compito. Introduciamo i Modelli Generativi Formalmente Protetti (FGGM), che permettono all'LLM pianificatore di specificare un contratto formale di output per ogni chiamata a un modello generativo usando la logica del primo ordine. Ogni chiamata FGGM avvolge il modello sottostante in un campionatore per rifiuto con una fallback verificata, garantendo che ogni output restituito soddisfi il contratto per qualsiasi input e configurazione dei parametri. Basandoci sugli FGGM, presentiamo SEVerA (Self-Evolving Verified Agents), un framework a tre fasi: la fase di Ricerca sintetizza programmi parametrici candidati contenenti chiamate FGGM; la Verifica dimostra la correttezza rispetto ai vincoli rigidi per tutti i valori dei parametri, riducendo il problema a un apprendimento senza vincoli; e l'Apprendimento applica un'ottimizzazione scalabile basata su gradienti, incluso fine-tuning in stile GRPO, per migliorare l'obiettivo flessibile preservando la correttezza. Valutiamo SEVerA sulla verifica di programmi Dafny, sulla sintesi matematica simbolica e sull'uso agentico di strumenti conforme a policy (τ^2-bench). In tutti i compiti, SEVerA raggiunge zero violazioni dei vincoli migliorando allo stesso tempo le prestazioni rispetto alle baseline senza vincoli e allo stato dell'arte, dimostrando che i vincoli comportamentali formali non solo garantiscono la correttezza, ma anche indirizzano la sintesi verso agenti di qualità superiore.
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.