SEVerA : Synthèse Vérifiée d'Agents Auto-Évolutifs

SEVerA: Verified Synthesis of Self-Evolving Agents

March 26, 2026

Auteurs: Debangshu Banerjee, Changming Xu, Gagandeep Singh

cs.AI

Résumé

Les progrès récents ont démontré l'efficacité des agents LLM auto-évolutifs pour des tâches telles que la correction de programmes et la découverte scientifique. Dans ce paradigme, un LLM planificateur synthétise un programme d'agent qui invoque des modèles paramétriques, y compris des LLM, lesquels sont ensuite ajustés par tâche pour améliorer les performances. Cependant, les frameworks d'agents auto-évolutifs existants n'offrent aucune garantie formelle de sécurité ou de correction. Étant donné que ces programmes sont souvent exécutés de manière autonome sur des entrées non vues, cette absence de garanties soulève des préoccupations en matière de fiabilité et de sécurité. Nous formulons la génération de code agentique comme un problème d'apprentissage contraint, combinant des spécifications formelles rigides avec des objectifs souples captant l'utilité de la tâche. Nous introduisons les Modèles Génératifs Formellement Gardés (FGGM), qui permettent au LLM planificateur de spécifier un contrat de sortie formel pour chaque appel à un modèle génératif en utilisant la logique du premier ordre. Chaque appel FGGM encapsule le modèle sous-jacent dans un échantillonneur de rejet avec une solution de repli vérifiée, garantissant que chaque sortie retournée satisfait le contrat pour toute entrée et tout réglage de paramètre. S'appuyant sur les FGGM, nous présentons SEVerA (Self-Evolving Verified Agents), un framework en trois étapes : la Recherche synthétise des programmes paramétriques candidats contenant des appels FGGM ; la Vérification prouve la correction par rapport aux contraintes rigides pour toutes les valeurs des paramètres, réduisant le problème à un apprentissage non contraint ; et l'Apprentissage applique une optimisation scalable basée sur le gradient, incluant un fine-tuning de type GRPO, pour améliorer l'objectif souple tout en préservant la correction. Nous évaluons SEVerA sur la vérification de programmes Dafny, la synthèse mathématique symbolique et l'utilisation agentique d'outils conforme à des politiques (τ^2-bench). Sur l'ensemble des tâches, SEVerA n'enregistre aucune violation de contrainte tout en améliorant les performances par rapport aux lignes de base non contraintes et à l'état de l'art, montrant que les contraintes comportementales formelles garantissent non seulement la correction mais orientent également la synthèse vers des agents de plus haute qualité.

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.