Source-linked AI summary
SEVerA: Verified Synthesis of Self-Evolving Agents
Debangshu Banerjee, Changming Xu, Eugene Ie, Ming Zhang, Daiyi Peng, Chu-Cheng Lin, Gagandeep Singh
TL;DR
Self-evolving agents lack formal guarantees despite autonomous execution on unseen inputs. SEVerA introduces FGGM-backed search and verification followed by unconstrained parameter learning, achieving zero constraint violations while improving performance across tasks; its formulation remains resource-unaware.
Problem
Existing self-evolving agent frameworks tune synthesized programs for performance without formal safety or correctness guarantees on unseen inputs.
Method
SEVerA uses FGGM calls with verified fallbacks, searches and verifies parametric programs for all model parameters, then applies gradient-based learning to verified programs.
Results
Across four tasks, SEVerA achieves zero constraint violations on held-out test inputs while improving task performance over every baseline.
Takeaways & Limitations
Formal behavioral constraints both guarantee safety and prune candidate programs toward higher-quality agents within the evaluated tasks.
Takeaways & Limitations
The formulation is resource-unaware: behavioral specifications constrain functional correctness but not computational resources such as LLM calls.
Abstract
from arXiv · showhide
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.
1 Introduction
SEVerA addresses the tension between formal safety guarantees and task-specific performance in self-evolving agent synthesis. It introduces FGGM and combines verified program synthesis with parameter optimization.
- Existing self-evolving frameworks synthesize programs that invoke tunable models, but autonomous execution on unseen inputs creates safety and reliability concerns.
- Safe agent synthesis must combine formal correctness guarantees with task-specific performance optimization.
- FGGM defines local first-order input-output contracts for individual generative-model calls, including LLM calls.
- SEVerA searches for FGGM-based parametric programs, verifies them over all embedded-model parameters, then learns parameters without sacrificing verified constraints.
2 Background
The paper models LLMs and self-evolving agents as string-generating programs that combine parametric models and tools, with learning defined over a program search space. Rejection sampling supplies the relevant background for guarded generation.
- LLMs are bounded probabilistic string generators that sample output strings from prompts over a finite alphabet.
- LLM generation repeatedly predicts a distribution over the next character or end-of-sequence symbol and decodes one choice.
- Rejection sampling draws candidates from an easy proposal distribution and accepts only samples within the target support.
- Self-evolving agents are programs that invoke parametric models and tools, while optimization seeks a low-loss program over a grammar-defined search space.
3 Problem Formulation
The paper formulates agent synthesis as learning under hard behavioral constraints that must hold for every valid input, rather than only optimizing loss on observed data. These constraints can expose errors missed by dataset evaluation.
- Optimizing training loss alone provides no guarantee that the synthesized program behaves correctly on unseen inputs.
- Behavioral specifications characterize expected outputs for any valid input, allowing correctness proofs beyond the training dataset.
- The constrained objective requires minimizing task loss while enforcing ∀x∈T_i. Φ(x) =⇒ Ψ(x, f(x)).
- Formal constraints can encode domain knowledge such as symbolic bounds or asymptotic behavior in scientific-discovery tasks.
4 Overview
SEVerA combines planner-guided program search, formal verification, and parameter learning around FGGMs. FGGMs use local contracts, rejection sampling, and verified fallbacks to preserve correctness while models are tuned for task performance.
- Learn: After verification, SEVerA tunes model parameters, maintains verified candidates, and returns the pool member with minimum task loss.
- Formally Guarded Generative Models: A verified FGGM rejection sampler preserves its local contract for all well-typed inputs and all underlying-model parameters.
- Formally Guarded Generative Models: Verified fallback programs handle violating or hallucinated outputs, making contract preservation unconditional even when sampling exhausts its attempts.
- Candidate Pool and Execution Feedback: The current design assigns separate parameter sets to different FGGM call sites and does not cap the number of FGGM calls.
5 Technical Details
SEVerA searches for parametric agent programs in a restricted Dafny space, verifies their formal behavioral contracts for all parameter values, and then optimizes task loss while preserving correctness. FGGM calls combine first-order local contracts, rejection sampling, and verified fallbacks to make generative-model outputs contract-compliant.
- 5.1 Search Space: SEVerA searches candidate programs in a restricted Dafny subset with typed expressions, control flow, annotations, and first-order input-output specifications.The planner LLM samples candidate programs, which Dafny can check for syntactic validity and formal correctness.
- 5.2 FGGM: An FGGM specifies a model-call type signature, first-order input-output contracts, prompting code, and a verified fallback around a parametric generative model.Well-formedness requires valid contracts, terminating type-checked programs, and a fallback satisfying the local contract.
- 5.2.1 FGGM Formal Definition: FGGM rejection sampling preserves each local contract for every well-typed input and every parameter setting of the underlying generative model.The checker is complete when the output contract is quantifier-free, although timeout-bounded checking may reject valid samples when quantifiers are present.
- 5.3 Verification: Verification accepts a candidate only after checking syntax, termination, and behavioral compliance, thereby guaranteeing the resulting program satisfies its specifications over all parameters.The soundness theorem applies to any returned non-bottom program and all inputs satisfying the input specification.
- 5.2.5 Learn: Learning uses task loss together with local conformance losses, encouraging model parameters to produce contract-satisfying outputs while reducing fallback use.The conformance loss aggregates the probability that sampled outputs violate each local checker; scalable gradient descent addresses the otherwise expensive optimization.
- 5.3 Theoretical Results: Under a loss that prefers satisfying outputs, quantifier-free contracts, and an available valid fallback, SEVerA can produce a compliant program with no greater loss than a type-correct generative model.The improvement is strict when the compared generative model violates the specification on a dataset example.
6 Evaluation
SEVerA is evaluated across four constrained agent-synthesis tasks using search, FGGM-based rejection sampling, verification, and learning where model access permits. It achieves zero violations while improving task performance across baselines, with ablations showing complementary benefits from global and local tuning.
- Evaluation setup: SEVerA evaluates formal safety, constrained learning effectiveness, and local-contract tuning across four tasks spanning verification, mathematics, scientific discovery, and tool use.The tasks are DafnyBench, GSM-Symbolic, τ2-bench, and constrained symbolic regression.
- Dafny verification: 0% violation rates and the highest Verif. & NoDiff rates—97.0% on HumanEvalDafny and 89.1% on DafnyBench—are achieved by full SEVerA.Unconstrained baselines still produce 8.1%, 4.0%, and 5.1% violations in the reported Dafny comparisons.
- Agentic tool use: 53.6% retail and 52.6% airline pass rates accompany 0% policy violations for SEVerA on τ2-bench.The unconstrained SEVerA variant reaches 49.4% and 44.7% pass rates but retains 10.3% and 25.5% violation rates.
- Symbolic math synthesis: 66.0% GSM-Symbolic accuracy is achieved with parameter tuning while maintaining zero violations, improving 12.8% over untuned SEVerA.The full pipeline combines global task tuning and local conformance tuning; global-only tuning reaches 61.7% and local-only tuning 55.3%.
- Constrained symbolic regression: SEVerA finds verified symbolic-regression solutions in 33 of 35 instances and achieves significantly lower test NMSE than PySR and LLM-SR.The baselines violate behavioral specifications in up to 62.86% and 34.29% of synthesis instances, respectively.
- Overall results: SEVerA achieves zero constraint violations on held-out inputs while improving task performance over every baseline across all four tasks.The shared pipeline uses planner-guided search, FGGM rejection sampling, deductive verification, and parameter tuning when model parameters are accessible.
- Runtime and scope: The full pipeline incurs a modest 1.9–2.5× slowdown relative to the LLM baseline on Dafny and GSM-Symbolic, while remaining faster than Agent-C on τ2-bench.SEVerA’s formulation is resource-unaware: its behavioral specifications do not constrain calls, tokens, or wall-clock budgets.
7 Related Work
Recent self-evolving agent work explores automatic synthesis and self-improvement, but does not provide formal behavioral guarantees despite demonstrated coding-agent risks.
- Prior work spans code-based action unification, skill libraries, architecture search, symbolic updates, world-model co-evolution, and reinforcement-learning-driven refinement.
- These approaches lack formal behavioral guarantees, making verification an unresolved concern for self-evolving agents.
8 Conclusion
SEVerA combines formally guarded model calls with program search and gradient-based learning to synthesize self-evolving agents with behavioral guarantees. Across four tasks, it achieves zero constraint violations while improving task performance over baselines, and formal constraints guide the search toward higher-quality agents.
- SEVerA binds each generative model call to a verified local contract using rejection sampling and a provably correct fallback.
- Its CEGIS-style pipeline searches over program structure before unconstrained gradient-based parameter optimization, retaining the scalability of methods such as GRPO.
- Zero constraint violations across all tasks accompanied improved task performance over unconstrained and state-of-the-art baselines.
- Formal behavioral constraints prune the candidate-program space and steer synthesis toward higher-quality agents.
A Restricted Dafny Grammar
The restricted Dafny grammar defines functions, statements, expressions, strings, formulas, bound variables, integer literals, and letters. Rejection sampling accepts proposal samples according to a target-to-proposal density ratio and rejects outputs outside the target support.
- Function declarations include an identifier, parameters, return type, specifications, and an expression body.
- Statements comprise assignments, conditionals, loops, assertions, and calls, while conditionals may include an else branch.
- Arithmetic and string expressions support literals, identifiers, operators, parentheses, and function calls; formulas additionally support negation, quantifiers, and relational expressions.
- Rejection sampling repeatedly draws proposal samples and accepts them using the target-to-proposal density ratio, with acceptance probability 1/M.
- Samples outside the target distribution’s support are always rejected, so every accepted sample lies within the target support.
C Library Functions for Symbolic Regression
The symbolic-regression library provides formally specified functions for arithmetic and mathematical operations. Its contracts constrain outputs and, where needed, impose input requirements.
- The library includes absolute value, maximum, minimum, sine, cosine, pi, and power functions with requires and ensures clauses.
- Contracts specify properties such as nonnegative absolute values, bounded trigonometric outputs, and input requirements for pi and power.
D.1 Axiom Syntax
The axiom library defines interval arithmetic and elementary-function properties, alongside verified string, Dafny, tool-safety, and GSM-parsing interfaces used by the framework.
- Interval multiplication bounds x×y using the minimum and maximum of the four endpoint products.
- The library exposes string-difference, Dafny-verification, and error-reporting functions for checking and repairing annotated programs.
- Reflexivity and transitivity axioms relate noDiff to equality-like program preservation, while empty error messages characterize successful checks.
- Agent safety axioms require non-tool responses to pass agentCCheck and permit transfer_to_human_agents calls when their parsed tool name matches.
K Example Agents for LLM Assisted Program Verification
The example Dafny agent uses three formally guarded model calls to generate and iteratively repair annotations while preserving the base program and verification postcondition.
- Example Agent: Three FGGMs handle initial annotation generation, diff-checker failures, and verifier failures with distinct prompting functions.
- Example Agent: Each FGGM enforces noDiff(base_program, output), using the original program as a fallback justified by reflexivity.
- Iteration Logic: The agent dispatches to diffErrorFGGM after diff failure and verifierErrorFGGM after verification failure on subsequent loop iterations.
- Validation: FGGM validity checking verifies contracts, library terms, type correctness, termination, and fallback satisfaction of the local contract.
- Contract Checking: Concrete output contracts are checked directly when quantifier-free and through axioms plus an SMT solver when quantified.
- Learning: GRPO fine-tunes each FGGM policy using grouped relative rewards that incorporate task loss and contract checking.
O Hyperparameters
The appendix records shared and task-specific hyperparameter settings, verifier and solver timeouts, and the planner prompt and feedback used across iterations.
- Hyperparameters: Table 8 lists shared pipeline settings, task-specific GSM-Symbolic and Symbolic Regression configurations, and per-task verifier and solver timeouts.
- Feedback: After each iteration, SEVerA builds structured feedback from the current best agent’s training traces, including failed examples, outputs, and error messages.
- Planner Prompt: The planner prompt is populated with the task specification, postcondition, operator library, agent signature, and previous execution-trace feedback.
R Proof Details
The proof details establish that FGGM checking is sound and complete under stated conditions, yielding local and global correctness guarantees while preserving or improving loss under additional assumptions.
- Checker Properties: For quantifier-free contracts, the checker is complete: under the input contract, it returns true exactly when the output contract holds.
- Checker Properties: Checker soundness extends to quantified contracts when axioms and input contracts imply the output contract for solver-accepted results.
- FGGM Guarantees: The valid-local-contract theorem guarantees every FGGM output satisfies its local contract for all parameters and inputs satisfying the input contract.
- Global Guarantees: The global theorem lifts local guarantees across a verified FGGM set to every parameter assignment and every input satisfying the global specification.
- Global Guarantees: The soundness theorem states that any non-bottom synthesized program satisfies the global input-output specification for all inputs.
- Sufficient Success: Under loss penalties for violations, quantifier-free specifications, and a satisfying non-parametric fallback, synthesis can preserve or improve loss while restoring correctness.