SEVerA: Verifizierte Synthese selbst-evolutionärer Agenten

SEVerA: Verified Synthesis of Self-Evolving Agents

March 26, 2026

Autoren: Debangshu Banerjee, Changming Xu, Gagandeep Singh

cs.AI

Zusammenfassung

Jüngste Fortschritte haben die Wirksamkeit selbstentwickelnder LLM-Agenten bei Aufgaben wie Programminstandsetzung und wissenschaftlicher Entdeckung gezeigt. In diesem Paradigma synthetisiert eine planende LLM ein Agentenprogramm, das parametrische Modelle – einschließlich LLMs – aufruft, die dann pro Aufgabe optimiert werden, um die Leistung zu verbessern. Bestehende Frameworks für selbstentwickelnde Agenten bieten jedoch keine formalen Garantien für Sicherheit oder Korrektheit. Da solche Programme oft autonom auf unbekannten Eingaben ausgeführt werden, wirft dieser Mangel an Garantien Bedenken hinsichtlich Zuverlässigkeit und Sicherheit auf. Wir formulieren die agentenbasierte Codegenerierung als ein eingeschränktes Lernproblem, das harte formale Spezifikationen mit weichen Zielvorgaben kombiniert, die den Aufgabennutzen erfassen. Wir führen Formally Guarded Generative Models (FGGM) ein, die es der planenden LLM ermöglichen, für jeden Aufruf eines generativen Modells einen formalen Ausgabevertrag mittels Logik erster Stufe zu spezifizieren. Jeder FGGM-Aufruf umhüllt das zugrundeliegende Modell mit einem Verwerfungssampler und einer verifizierten Fallback-Lösung, um sicherzustellen, dass jede zurückgegebene Ausgabe den Vertrag für jede Eingabe und jede Parametereinstellung erfüllt. Aufbauend auf FGGM präsentieren wir SEVerA (Self-Evolving Verified Agents), ein dreistufiges Framework: Search synthetisiert kanditative parametrische Programme, die FGGM-Aufrufe enthalten; Verification beweist die Korrektheit hinsichtlich harter Einschränkungen für alle Parameterwerte und reduziert das Problem auf unbegrenztes Lernen; und Learning wendet skalierbare gradientenbasierte Optimierung an, einschließlich GRPO-artigem Fine-Tuning, um die weiche Zielvorgabe zu verbessern, während die Korrektheit erhalten bleibt. Wir evaluieren SEVerA anhand von Dafny-Programmverifikation, symbolischer Mathematik-Synthese und richtlinienkonformer agentenbasierter Werkzeugnutzung (τ^2-bench). Über alle Aufgaben hinweg erreicht SEVerA null Einschränkungsverletzungen bei gleichzeitiger Leistungssteigerung im Vergleich zu uneingeschränkten und state-of-the-art Baseline-Modellen. Dies zeigt, dass formale Verhaltensbeschränkungen nicht nur Korrektheit garantieren, sondern die Synthese auch zu höherwertigeren Agenten lenken.

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.