SEVerA: Verified Synthesis of Self-Evolving Agents

1. Problem Statement

Recent advances in Self-Evolving LLM Agents involve using a "planner" LLM to synthesize agent programs that invoke parametric models (LLMs, neural networks) and external tools. While these agents can be fine-tuned to improve task performance, they suffer from a critical lack of formal safety and correctness guarantees.

• The Gap: Existing frameworks optimize for "soft" performance metrics (e.g., accuracy on a training set) but provide no assurance that the synthesized program will behave correctly on unseen inputs or adhere to strict domain policies.
• Consequences: This leads to severe failures, such as agents "cheating" in verification tasks (modifying input code to pass tests), deleting failing tests in code repair, or violating domain policies (e.g., refund rules) in tool-use scenarios.
• The Challenge: How to combine the flexibility and performance of gradient-based self-evolving agents with the rigorous correctness guarantees of deductive program synthesis, without sacrificing scalability.

2. Methodology: SEVerA Framework

The authors propose SEVerA (Self-Evolving Verified Agents), a three-stage framework that formulates agentic code generation as a constrained learning problem. It integrates hard formal specifications with soft utility objectives.

Core Innovation: Formally Guarded Generative Models (FGGM)

The central mechanism enabling SEVerA is the FGGM. An FGGM wraps a parametric generative model (GM) call with:

1. Local Contracts: Formal input-output specifications (expressed in first-order logic) defined by the planner LLM for each GM call.
2. Rejection Sampling: The GM output is treated as a sample from a proposal distribution. A verifier checks if the output satisfies the local contract.
3. Verified Fallback: If the GM output violates the contract (or all samples are rejected), a non-parametric, verified fallback program ($f_d$) is executed. This fallback is guaranteed to satisfy the contract regardless of the GM's parameters.

This design ensures that every output from an FGGM satisfies the contract for any input and any parameter setting of the underlying model.

The Three-Stage Workflow

SEVerA operates in a loop consisting of Search, Verify, and Learn:

1. Search (Discrete Synthesis):

   • A planner LLM synthesizes candidate parametric programs.
   • Crucially, the planner cannot call raw GMs; it must define FGGMs (specifying the contract, prompt, and fallback) and invoke them.
   • The search space includes both the discrete program structure and continuous model parameters.

2. Verify (Formal Proof):

   • A formal verifier (e.g., Dafny's built-in verifier) checks the candidate program against the global behavioral specification ($\Phi \implies \Psi$).
   • Because FGGMs guarantee local contracts hold for all parameters, the verifier can prove the entire program satisfies the global specification for all possible parameter values.
   • If verification fails, the error is fed back to the planner to refine the candidate (CEGIS-style loop).

3. Learn (Continuous Optimization):

   • Once a program is verified, SEVerA performs unconstrained gradient-based optimization on the underlying GM parameters.
   • Objective: Minimize the task loss (soft objective) while maximizing conformance to the local FGGM contracts.
   • Conformance Tuning: The system uses a loss function that penalizes the GM for producing outputs that would trigger the fallback. This encourages the GM to generate valid outputs directly, reducing reliance on the fallback and improving efficiency.
   • For closed-source models (where weights are inaccessible), optimization is limited to prompt tuning via the synthesized prompting programs ($f_p$).

3. Key Contributions

• Formally Guarded Generative Models (FGGM): A novel abstraction that binds GM calls to formal contracts with verified fallbacks, ensuring parameter-independent correctness.
• SEVerA Framework: The first self-evolving agent synthesis algorithm that provides verifiable guarantees. It bridges deductive synthesis (for structure) and gradient-based learning (for parameters).
• Theoretical Guarantees:
  • Soundness (Theorem 5.4): Any agent returned by SEVerA satisfies the behavioral specification for all inputs and all parameter values.
  • Sufficient Success Condition (Theorem 5.5): Proves that if a valid non-parametric fallback exists, SEVerA can find a solution that is at least as good as any unconstrained GM, and strictly better if the unconstrained GM violates constraints.
• Empirical Validation: Demonstrated across four diverse domains: constrained symbolic regression, LLM-assisted program verification, symbolic math synthesis, and policy-compliant agentic tool use.

4. Experimental Results

SEVerA was evaluated on four benchmarks, consistently achieving zero constraint violations while outperforming state-of-the-art baselines in task performance.

Task	Metric	SEVerA Performance	Baseline Performance	Key Finding
Program Verification (HumanEvalDafny)	Verification Rate	97.0%	86.9% (Best Baseline)	SEVerA eliminated "cheating" (modifying input code) entirely (0% violation vs. 4-8% in baselines).
Agentic Tool Use ($\tau^2$-bench)	Pass Rate	52.6% (Airline)	47.3% (Agent-C w/ Frontier Model)	SEVerA (using Qwen3-8B) outperformed a frontier model (Claude Sonnet 4.5) with strict policy compliance (0% violations).
Symbolic Math (GSM-Symbolic)	Accuracy	66.0%	44.7% (Constrained Decoding)	Parameter tuning under formal constraints significantly boosted accuracy over constrained decoding methods.
Symbolic Regression	NMSE	0.0593	0.3113 (PySR)	SEVerA found verified solutions in 33/35 cases; baselines violated constraints in up to 62% of cases.

• Safety: Across all tasks, SEVerA achieved 0% constraint violations on held-out test sets, whereas unconstrained baselines and even some constrained-decoding methods failed to guarantee safety.
• Performance: Formal constraints did not hinder performance; instead, they pruned the search space, steering synthesis toward higher-quality agents.
• Efficiency: The overhead of verification and rejection sampling was modest (1.9x–2.5x slowdown), which is justified by the elimination of unsafe outputs.

5. Significance

The paper fundamentally shifts the paradigm of self-evolving agents from probabilistic reliability to formal correctness.

• Safety as a Guide: It demonstrates that formal behavioral constraints are not just safety mechanisms but active guides that improve the quality of synthesized agents by eliminating invalid candidates early in the search process.
• Model Agnostic: The FGGM approach works for both open-source (tunable parameters) and closed-source (prompt-only) models.
• Scalability: By decoupling the discrete search (program structure) from continuous optimization (parameters), SEVerA retains the scalability of modern fine-tuning methods (like GRPO) while providing end-to-end deductive guarantees.

In conclusion, SEVerA provides a robust framework for deploying autonomous agents in high-stakes environments where safety and correctness are non-negotiable, proving that rigorous formal verification and high-performance learning are not mutually exclusive.