SEVerA: Geverifieerde Synthese van Zelfontwikkelende Agenten

SEVerA: Verified Synthesis of Self-Evolving Agents

March 26, 2026

Auteurs: Debangshu Banerjee, Changming Xu, Gagandeep Singh

cs.AI

Samenvatting

Recente vooruitgang heeft de effectiviteit van zelf-evoluerende LLM-agenten aangetoond bij taken zoals programmareparatie en wetenschappelijke ontdekking. In dit paradigma synthetiseert een planner-LLM een agentprogramma dat parametrische modellen aanroept, inclusief LLM's, die vervolgens per taak worden afgesteld om de prestaties te verbeteren. Bestaande kaders voor zelf-evoluerende agenten bieden echter geen formele garanties voor veiligheid of correctheid. Omdat dergelijke programma's vaak autonoom worden uitgevoerd op onbekende invoer, wekt dit gebrek aan garanties zorgen op over betrouwbaarheid en veiligheid. Wij formuleren de generatie van agentcode als een beperkt leerprobleem, waarbij harde formele specificaties worden gecombineerd met zachte doelstellingen die de taaknut bepalen. Wij introduceren Formeel Bewaakte Generatieve Modellen (FGGM), die de planner-LLM in staat stellen een formeel uitvoercontract voor elke generatieve modelaanroep te specificeren met behulp van logica van de eerste orde. Elke FGGM-aanroep verpakt het onderliggende model in een rejection sampler met een geverifieerde fallback, waardoor gegarandeerd wordt dat elke teruggegeven uitvoer voldoet aan het contract voor elke invoer en parameterinstelling. Voortbouwend op FGGM presenteren wij SEVerA (Self-Evolving Verified Agents), een raamwerk met drie fasen: Search synthetiseert kandidaat parametrische programma's die FGGM-aanroepen bevatten; Verificatie bewijst correctheid met betrekking tot harde beperkingen voor alle parameterwaarden, wat het probleem reduceert tot onbeperkt leren; en Learning past schaalbare, op gradienten gebaseerde optimalisatie toe, inclusief GRPO-stijl fine-tuning, om het zachte doel te verbeteren terwijl de correctheid behouden blijft. Wij evalueren SEVerA op Dafny-programmaverificatie, symbolische wiskundesynthese en beleidsconform instrumentgebruik door agenten (τ^2-bench). Over alle taken heen behaalt SEVerA nul schendingen van de beperkingen en verbetert het de prestaties ten opzichte van onbeperkte en state-of-the-art baseline-methoden. Dit toont aan dat formele gedragsbeperkingen niet alleen correctheid garanderen, maar ook de synthese sturen naar agenten van hogere kwaliteit.

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.