PaperlayerView exact revision on arXiv

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

arXiv:2603.25111v2cs.LGcs.PLcs.SE

TL;DR

Existing self-evolving agents lack formal safety and correctness guarantees despite autonomous execution on unseen inputs. SEVerA combines per-call contracts and verified fallbacks with parameter learning; across four tasks, it achieves zero held-out constraint violations while improving performance over every baseline.

  • Problem

    Existing self-evolving agent frameworks lack formal safety guarantees, while balancing correctness guarantees with task-specific performance remains an open challenge.

    Source: §1 · p. 2

  • Method

    SEVerA uses FGGM calls with verified local contracts, rejection sampling, and fallbacks, then separates program-structure search from parameter optimization.

    Source: §4.2.1 · p. 8, §8 · p. 24

  • Results

    Zero constraint violations on held-out test inputs and improved task performance over every baseline were achieved across all four tasks.

    Source: §6.5 · p. 23

  • Takeaways & Limitations

    Formal behavioral specifications can prune candidate programs and steer synthesis toward higher-quality agents, beyond enforcing safety.

    Source: §6.5 · p. 23

    SEVerA currently neither shares parameters nor caps FGGM calls, and supporting either could reduce the computational budget for parameter learning.

    Source: §4.3.1 · p. 11

Abstract

from arXiv · show

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 combines formal behavioral constraints with parameter learning for self-evolving agents, using per-call contracts and verified synthesis to target safety and task performance.

1 Introduction

  • Synthesized agents run autonomously on unseen inputs, and self-evolving frameworks update embedded-model parameters, so correctness must survive those updates.Failures cited include agents changing program inputs, deleting failing tests, violating tool-use policies, and bypassing security protections.Source: §1 · p. 2
  • The challenge is to combine formal correctness with task-specific optimization and support per-call constraints beyond limited constrained-decoding grammars without distorting output quality.Deductive synthesis typically does not optimize task-specific performance, while gradient-based methods such as GRPO offer no constraint guarantee; constrained decoding is limited in supported constraints and can degrade performance.Source: §1 · p. 2
  • SEVerA searches for parametric programs, verifies their contracts across all embedded-model parameters, then learns by unconstrained optimization while preserving correctness.Search uses a planner LLM and a verifier-aware language such as Dafny; Verify proves the contracts, and Learn enables scalable gradient-based training.Source: §1 · p. 3
  • Formally Guarded Generative Models (FGGM) specify local model-call contracts in first-order logic and enforce them on output strings for open- and closed-source models.The paper presents FGGM as combining deductive-synthesis guarantees with performance gains from gradient-based parameter optimization.Source: §1 · p. 3
  • SEVerA is sound: every returned agent satisfies its behavioral specification for all inputs and parameter values.A sufficient condition also guarantees a verified agent with no greater task loss than any unconstrained generative model at its initial parameters, with strict improvement when that model violates the specification.Source: §1 · p. 3
  • SEVerA reports 97.0% verification rate on HumanEvalDafny (vs. 86.9% for the best baseline), 66.0% accuracy on GSM-Symbolic (vs. 44.7% for the best constrained-decoding method), and 52.6% pass rate on τ²-bench airline using Qwen3-8B.Across benchmarks, SEVerA achieves provably zero constraint violations; on τ²-bench airline it also beats Agent-C [20] with Claude Sonnet 4.5.Source: §1 · p. 3

2 Background

The background defines LLMs as bounded probabilistic string generators, rejection sampling as a support-constrained sampling method, and self-evolving agents as programs synthesized by a planner and optimized over a program search space.

Notations and Terminology

  • An LLM samples a bounded string by repeatedly predicting and decoding characters until termination or the length limit n.The model predicts a distribution over the alphabet and an end-of-sequence symbol, then samples the next character at each step.Source: §2 · pp. 3–4

Rejection Sampling

  • Rejection sampling draws candidates from a proposal distribution whose support covers the target distribution, and accepted samples lie within the target support.The support of a distribution is the set of points with positive probability.Source: §2 · p. 4

Self-evolving LLM agents

  • A self-evolving agent is a program generated by a planner LLM from task instructions, invoking parametric models and tools supplied as library functions.The program maps user inputs to outputs and may be written in an imperative language such as Python.Source: §2 · p. 4
  • The planner’s search space contains syntactically valid programs using the available library, including all parametric model values, and seeks to minimize aggregated task loss.The loss can use ground-truth outputs when available or omit them when they are unavailable.Source: §2 · p. 4

3 Problem Formulation

The section formulates agent synthesis as learning under hard formal behavioral constraints, so synthesized programs can be checked beyond the training set. These constraints can also guide search by pruning candidates that fail verification.

Constrained learning formulation

  • The constrained objective optimizes task loss subject to Φ(x) => Ψ(x, f(x)) for every input x satisfying Φ.This replaces unconstrained training-set optimization with hard input and output specifications, while retaining a soft learning objective.Source: §3 · p. 4

Role of hard constraints

  • Formal specifications enable correctness proofs on valid inputs, prune unverified candidates, and catch errors that fixed-dataset evaluation may miss.The section identifies retaining the performance and scalability of gradient-based learning as the central challenge.Source: §3 · pp. 4–5

Application examples

  • In scientific discovery, constraints encode formula priors and reject invalid fits; in program verification, AST-based equivalence checks prevent cheating by input modification [3].For noisy data, formula constraints can also help prevent overfitting.Source: §3 · p. 5
  • For symbolic math generation, constraints require structurally valid expressions; for agentic tool use, each proposed call is checked against formal policy before execution.Tool-use utility is measured across the interaction, while policy compliance is enforced at each call regardless of user input.Source: §3 · p. 5

4 Overview

SEVerA combines planner-guided program search and formal verification with gradient-based model tuning, using formally guarded generative model calls to preserve correctness while improving task performance. Its overview illustrates the framework on constrained symbolic regression and Dafny annotation synthesis.

4.1.1 Constrained Symbolic Regression:

  • For constrained symbolic regression, SEVerA seeks the noisy-data ground truth 1.23 × max(x, 0.0) while enforcing x ≥ 0 and lower bounds on f(x) for x ≤ 1 and x ≥ 1.The search space uses a restricted Dafny subset with basic types, conditionals, loops, and calls to library functions including transcendental functions and parametric neural networks.Source: §4.1.1 · p. 7

4.1.2 LLM-Assisted Automated Verification.

  • For Dafny annotation synthesis, the agent maps specified programs to annotated programs, requiring parsable outputs that preserve the input except for added annotations.The task loss is 1 for programs that fail verification within a fixed time budget and 0 for verified programs; constraints apply to every parsable input, not only training examples.Source: §4.1.2 · pp. 7–8

4.2 Formally Guarded Generative Model

  • FGGMs bind each generative-model call to local input-output contracts and a verified fallback, so outputs satisfy the contracts regardless of model parameters.A fixed number K of model samples are checked and rejected if nonconforming; if all are rejected, the fallback returns a contract-satisfying output. Local contracts also guide learning toward higher acceptance rates.Source: §4.2 · p. 8, §4.2.1 · pp. 8–9
  • FGGM design combines flexible planner-defined first-order contracts, parameter-independent correctness, and local learning objectives that characterize expected model outputs.The planner also synthesizes a prompting program and a non-parametric fallback using constrained library functions; the fallback handles hallucinated or otherwise nonconforming samples.Source: §4.2 · p. 8, §4.2.1 · p. 8

4.2.2 Examples.

  • Examples show a bounded-parameter FGGM clamps violating neural-network samples into [l, u], while a Dafny FGGM falls back to the original program to preserve validity and annotations-only changes.The Dafny fallback relies on the reflexivity axiom for noDiff.Source: §4.2.2 · p. 9

4.2.3 Conformance Tuning.

  • Conformance tuning reduces the probability of contract-violating model outputs across inputs, improving rejection-sampler acceptance and reducing reliance on the fallback.The local loss aggregates violation probability over an input set P and tunes model parameters to concentrate probability mass on the contracts’ support.Source: §4.2.3 · pp. 9–10

4.3 SEVerA

  • SEVerA searches over candidate programs, verifies them against behavioral specifications, then tunes model parameters while retaining the correctness guarantees of verified candidates.The planner receives verifier feedback to refine failing candidates; direct calls to parametric generative models are disallowed unless wrapped in a verified FGGM.Source: §4.3 · p. 10

4.3.1 Candidate Pool and Execution Feedback.

  • In the symbolic-regression example, separately tuned boundedParam calls return constants a = 1.11 and d = 0.503, recovering the ground-truth function with negligible error.SEVerA maintains a pool of verified, fine-tuned candidates and selects the one with lowest task loss; the described implementation does not share parameters across call sites or cap FGGM calls.Source: §4.3.1 · pp. 10–11

5 Technical Details

Section 5 details SEVerA’s program space and search–verification–learning procedure, proving behavioral-constraint preservation and giving conditions for constraint-satisfying solutions with competitive loss. It also shows that FGGM filtering can improve on bare generative-model calls under mild assumptions, without guaranteeing that SEVerA finds the optimal program.

5.1 Search Space

  • Dafny’s restricted, verification-aware subset defines the candidate program space, with built-in verification and termination checking applied under a fixed timeout.The subset includes control flow, assignments, assertions, calls, and annotations; library functions have types and first-order input–output contracts. The framework is not language-specific, but Dafny supplies verification and termination infrastructure.Source: §5.1 · pp. 11–12

5.2.1 FGGM Formal Definition.

  • For each FGGM, SEVerA validates its types, contracts, prompting program, and terminating fallback, then synthesizes a rejection sampler that preserves the local contract for every parameter value.The sampler terminates because its sample count is finite and its prompting, fallback, and checking components terminate. For quantifier-free output contracts, the checker is sound and complete; with quantifiers, timeout-bounded SMT checking is sound but may reject valid samples.Source: §5.2.1 · pp. 12–14

5.2.4 Search and Verify.

  • Search and verification form a CEGIS-style loop that proposes FGGM definitions and parametric programs, checks syntax, termination, and behavioral compliance, and accepts only verified programs.If a candidate fails, SEVerA uses error feedback to continue searching until the fixed budget is exhausted; an accepted program satisfies its specification for all parameter values.Source: §5.2.4 · p. 14

5.2.5 Learn.

  • Learning combines task loss with local FGGM conformance losses, encouraging contract-satisfying outputs and reducing fallback use; independent per-call conformance terms enable modular, parallel optimization.Accessible generative-model parameters can be fine-tuned with methods such as GRPO [36]; for closed-source models, learning is skipped and improvements rely on prompt tuning.Source: §5.2.5 · pp. 15–16

5.2.6 SEVerA.

  • SEVerA iteratively adds tuned verified agents to a candidate pool, uses their execution traces as planner feedback, and returns the pool member with the lowest dataset task loss, or ⊥ if the pool is empty.For agents without optimizable parameters, the learning step is skipped and improvement relies on prompt tuning.Source: §5.2.6 · p. 16

5.3 Theoretical Results

  • Theorem 5.4 establishes that any non-⊥ agent returned by SEVerA satisfies the behavioral specification for all inputs, given the axioms.The guarantee follows because the candidate pool contains only programs verified to satisfy the specification, and learning preserves their all-parameter guarantee.Source: §5.3 · p. 16
  • Theorem 5.5 gives a sufficient success condition: if violations incur greater loss, the output contract is quantifier-free, and a valid non-parametric satisfying program exists, SEVerA’s search space contains a satisfying program with no greater loss than any type-correct generative model.The condition uses a valid non-parametric program as an FGGM fallback and relies on checker completeness for quantifier-free contracts.Source: §5.3 · pp. 16–17
  • Theorem 5.5 shows FGGM filtering with a valid fallback cannot increase loss and strictly improves it when a bare GM violates Ψ.The mechanism rejects constraint-violating outputs and substitutes the fallback.Source: §5.3 · p. 17
  • The result assumes constraint-satisfying outputs are preferred, Ψ is quantifier-free for checker completeness, and a valid fallback exists.The paper describes these assumptions as mild in practice.Source: §5.3 · p. 17
  • Experiments use quantifier-free specifications for symbolic regression and computable library predicates such as parse and noDiff as runtime checks for program verification.Source: §5.3 · p. 17
  • The theorem does not ensure SEVerA finds the optimal program, since the planner may not propose the right candidate within the search budget.It establishes that the search space can contain solutions that dominate unconstrained GM calls.Source: §5.3 · p. 17

6 Evaluation

SEVerA is evaluated on four constrained agent-synthesis tasks to test safety, learning under hard constraints, and the effects of local conformance tuning. Across the tasks, results report that formal constraints can both prevent violations and improve task performance.

6.1 Experimental Setup

  • The evaluation reports constraint-violation rate, task-specific performance, and wall-clock time across Dafny, GSM-Symbolic, τ²-bench, and symbolic regression.The common pipeline uses 10 search iterations and a rejection-sampling budget K=5; tuning is omitted for Dafny and τ²-bench because weights are inaccessible or traces make gradient-based fine-tuning prohibitively expensive.Source: §6 · p. 17, §6.1.1 · p. 18, §6.1.2 · p. 18

6.2.1 LLM-Assisted Program Verification (Dafny).

  • SEVerA achieves 0% violations and the highest Verif. & NoDiff rates on both Dafny benchmarks: 97.0% on HumanEvalDafny and 89.1% on DafnyBench.The LLM baseline reaches 76.8% verification on HumanEvalDafny, but only 73.7% of those outputs preserve the input; full SEVerA uses no parameter tuning because Claude Sonnet 4.5 is closed-source. The synthesized Dafny agent uses three FGGMs with a no-diff contract to prevent changes beyond added annotations.Source: Table 2 · p. 19, §6.2.1 · p. 20, §6.4 · p. 22

6.2.2 Agentic Tool Use (𝜏2-bench).

  • SEVerA eliminates tool-policy violations and raises pass rates to 53.6% in retail and 52.6% in airline, outperforming Agent-C’s 47.3% in airline.SEVerA is faster than Agent-C in both domains: 212.4s vs. 234.7s in retail and 241.1s vs. 272.6s in airline. Constraints apply to each tool call, while pass rate measures success across the full interaction trace.Source: Table 3 · p. 20, §6.2.2 · pp. 20–21

6.2.3 Symbolic Math Synthesis (GSM-Symbolic).

  • GRPO-tuned SEVerA reaches 66.0% GSM-Symbolic accuracy with zero violations, up from 53.2% untuned and 44.7% for CRANE [4].The tuned variant is faster than untuned SEVerA (16.7 s vs. 18.8 s); tuning improves first-sample conformance, reducing reliance on the verified fallback.Source: Table 4 · p. 21, §6.2.3 · p. 21

6.2.4 Constrained Symbolic Regression.

  • On constrained symbolic regression, SEVerA finds a verified solution in 33 out of 35 instances at both noise levels and achieves significantly lower NMSE than both baselines on valid instances.PySR violates behavioral specifications in up to 62.86% of instances and LLM-SR in up to 34.29%; NMSE comparisons exclude instances where baseline programs violate constraints.Source: §6.2.4 · p. 21, Table 5 · p. 22, Table 6 · p. 22

6.3 Constraint Decomposition

  • On GSM-Symbolic, local-only tuning raises accuracy from 53.2% to 55.3%, global-only tuning to 61.7%, and combining both losses to 66.0%.The local conformance loss improves per-call contract satisfaction, while the global task loss improves semantic correctness; the results indicate complementary training signals.Source: Table 7 · p. 22, §6.3 · p. 22

6.5 Discussion

  • Across all four tasks, SEVerA reports zero held-out constraint violations and better task performance than every baseline; it is faster than Agent-C on τ²-bench, with 1.9–2.5× slowdown on Dafny and GSM-Symbolic.The evaluation identifies verification and rejection sampling as sources of the slowdown; the formulation does not constrain resource use such as LLM calls, tokens, or wall-clock time.Source: §6.5 · p. 23

7 Related Work

SEVerA relates to agent synthesis, runtime safety, neuro-symbolic synthesis, constrained decoding, and deductive synthesis. It addresses their respective limitations by verifying hard formal specifications at synthesis time and binding generative calls to verified contracts.

Self-Evolving Agents and Their Risks

  • SEVerA adds verified hard specifications to self-evolving agent synthesis, whose prior approaches offer no formal behavioral guarantees despite demonstrated risks from exploits and verification cheating [3] [15] [25] [50].Prior work spans action unification, skill libraries [47], architecture search [13] [19], symbolic updates [51], world-model co-evolution [11], and reinforcement-learning-driven skill refinement [43] [48].Source: §7 · p. 23

Runtime Monitoring and Shielding

  • Unlike runtime shields and trace monitors [20] [52], which cover observed executions, SEVerA verifies synthesized programs at synthesis time for all inputs and parameter values.Monitoring checks can also define specifications, as in [20].Source: §7 · p. 23

Neuro-Symbolic Program Synthesis

  • SEVerA extends neuro-symbolic program synthesis, whose neural-component programs lack composed-system correctness guarantees, by binding each model call to a verified local contract.Related approaches include neural generation from examples [34], differentiable programming [46], library learning, vision-language composition [41], and symbolic regression [37].Source: §7 · p. 23

Constrained Decoding

  • Unlike constrained decoding methods [4] [6] [32] [33] [35] [40] [44] [45], SEVerA uses model-agnostic rejection sampling to enforce first-order-logic specifications verified at program level.Prior decoding approaches require access to decoding internals and constrain tokens or outputs rather than program-level behavior.Source: §7 · p. 23

Deductive Program Synthesis

  • SEVerA extends deductive synthesis, which guarantees correctness for deterministic, non-parametric programs, with CEGIS-style structural search and verified contracts around parametric generative models.Classical approaches include syntax-guided, semantics-guided [22], counterexample-guided, abstraction-guided [16], and component-based [12] synthesis.Source: §7 · p. 23

8 Conclusion

SEVerA combines formally guarded generative model calls with a search-and-optimization framework to provide behavioral guarantees while improving agent performance. Its formal constraints also prune the search space and steer synthesis toward higher-quality agents.

8 Conclusion

  • Across constrained symbolic regression, LLM-assisted Dafny verification, symbolic math synthesis, and policy-compliant agentic tool use, SEVerA achieves zero constraint violations and improves performance over unconstrained and state-of-the-art baselines.The evaluation covers all four tasks.Source: §8 · p. 24
  • FGGMs bind each generative model call to a verified local contract, using rejection sampling with a provably correct fallback to ensure specifications hold for all inputs and parameter values.Source: §8 · p. 24
  • SEVerA uses CEGIS-style discrete search over program structure followed by unconstrained gradient-based parameter optimization, retaining the scalability of methods such as GRPO while providing end-to-end correctness guarantees.Source: §8 · p. 24
  • Formal behavioral constraints do more than provide safety: they prune the search space and steer synthesis toward higher-quality agents.Source: §8 · p. 24

A Restricted Dafny Grammar · B Rejection Sampling Details

The appendices specify a restricted Dafny grammar for generated programs and describe rejection sampling, including its assumptions, acceptance rule, and guarantees.

A Restricted Dafny Grammar

  • The restricted grammar defines function declarations as a function name, parameters, return type, specifications, and expression.Source: A Restricted Dafny Grammar · p. 28
  • Statements comprise assignments, conditionals, loops, assertions, and calls, with conditionals permitting an optional else branch.Source: A Restricted Dafny Grammar · p. 28
  • Arithmetic expressions allow integer literals, identifiers, binary arithmetic, parentheses, and function calls; integer literals are digit sequences.Identifiers use letters from a–z or A–Z.Source: A Restricted Dafny Grammar · p. 28
  • String expressions allow string literals, identifiers, parentheses, and function calls.Source: A Restricted Dafny Grammar · p. 28
  • Formulas include relational expressions, negation, parentheses, predicate calls, and universal or existential quantification over typed variables.Bound variables may be listed as comma-separated typed declarations.Source: A Restricted Dafny Grammar · p. 28

B Rejection Sampling Details

  • Rejection sampling accepts proposal draws according to the target-to-proposal density ratio and repeats after rejection, yielding samples from the target distribution.The procedure assumes the target support is contained in the proposal support and that the target density is bounded by M times the proposal density.Source: B Rejection Sampling Details · p. 29
  • Accepted samples always lie in the target support, and the acceptance probability is 1/M; this paper assumes M = 1.Samples outside the target support are always rejected.Source: B Rejection Sampling Details · p. 29

C Library Functions for Symbolic Regression · D Additional Axioms for Symbolic Regression

The symbolic-regression library exposes real-valued functions with formal preconditions and output guarantees, alongside neutral functions without listed contracts. The supplied passages describe this library but provide no additional axioms from Section D.

C Library Functions for Symbolic Regression

  • The library specifies abs as nonnegative and equal to either x or -x, while max and min return one of their inputs and bound both inputs appropriately.For max, each input is at most the result; for min, each input is at least the result.Source: C Library Functions for Symbolic… · p. 29
  • sin and cos are bounded between -1 and 1, with specified values at zero; pi requires nonnegative input and bounds its result by two close decimal multiples of that input.sin(0)=0, cos(0)=1, and the pi bounds use 3.141592653589790 and 3.141592653589793.Source: C Library Functions for Symbolic… · p. 29
  • pow requires x >= 0 and either x != 0 or d >= 0, then guarantees nonnegative output and sign, unit-exponent, and monotonicity-style conditions.Its listed conditions include d=0 implying r=1 and cases relating whether x and d are above or below 1 to bounds on r.Source: C Library Functions for Symbolic… · p. 29
  • sqrt requires x >= 0 and guarantees a nonnegative result whose square equals x.Source: C Library Functions for Symbolic… · p. 29
  • exp is constrained to be nonnegative, to lie on specified sides of 1 for nonpositive or nonnegative inputs, to satisfy 2.71 <= r <= 2.72 at x=1, and to obey r >= 1+x.Source: C Library Functions for Symbolic… · p. 29
  • log requires x > 0 and specifies output signs around x=1, including r=0 when x=1; neutral1, neutral2, and neutral3 have no listed guarantees.Source: C Library Functions for Symbolic… · p. 29

D.1 Axiom Syntax … J Additional Axioms for GSM-Symbolic

The appendix gives formal axioms for arithmetic and task-specific properties, alongside library-function interfaces for Dafny verification, τ²-bench, and GSM-Symbolic.

D.1 Axiom Syntax

  • Interval multiplication bounds the product by the minimum and maximum of the four endpoint products, alongside axioms for power, exponential, logarithm, and square root.The power axioms specify monotonicity for bases in [0,1] and bases at least 1; the remaining axioms relate exp, log, and sqrt to power.Source: §D.1 · p. 29

E Library Functions for Dafny Program Verification

  • Dafny’s library set F provides clause prompting, code-difference checks, verifier calls, Dafny-code extraction, and substring testing.The interfaces include variants that return verifier or difference error messages.Source: E Library Functions for Dafny Program… · pp. 29–30

F Additional Axioms for Dafny Program Verification

G Library Functions for 𝜏2-bench

H Additional Axioms for 𝜏2-bench

I Library Functions for GSM-Symbolic

K Example Agents for LLM Assisted Program Verification … N Background on GRPO

The appendices illustrate how SEVerA builds verified Dafny agents, checks FGGM definitions and outputs, and applies GRPO to fine-tune FGGM policies. The examples preserve program logic through contracts and fallbacks, while the checks enforce contract validity.

K Example Agents for LLM Assisted Program Verification

  • The Dafny agent dispatches among three FGGMs for initial annotation, diff-checker repair, and verification-error repair, each preserving the base program through a noDiff contract and fallback.Each fallback returns the original program, justified by reflexivity; the loop returns its best attempt after exhausting retries.Source: K Example Agents for LLM Assisted… · p. 30, Figure 5 · p. 33, Figure 6 · p. 34

L FGGM Syntax

  • The FGGM syntax is specified with a BNF grammar using the production rules for identifiers, types, specifications, programs, string literals, and formulas from Appendix A.Source: L FGGM Syntax · p. 36

M FGGM Validity Check

  • FGGM validity checking rejects definitions with ill-formed contracts, invalid library terms, non-type-correct or nonterminating prompt and fallback programs, or a fallback that fails deductive verification.The check also validates the type signature and proves that the fallback satisfies the local output contract for all inputs.Source: M FGGM Validity Check · pp. 36–37
  • For a concrete input-output tuple, the contract checker evaluates quantifier-free specifications directly and sends quantified formulas with axioms and the input contract to a timeout-bounded SMT solver.It returns true only when the solver confirms satisfiability within the time bound.Source: M FGGM Validity Check · pp. 37–38

N Background on GRPO

  • GRPO samples G candidate outputs per prompt, assigns each a scalar reward, and computes relative advantages using rewards within that group.The group’s mean and standard deviation define the reward normalization.Source: N Background on GRPO · p. 38
  • GRPO uses a PPO-like clipped objective for stable policy updates, with each parameterized FGGM defining a policy over outputs for its input prompt.Source: N Background on GRPO · p. 38

O Hyperparameters · P Planner Feedback · Q Planner LLM Prompt

The appendices document SEVerA’s hyperparameter organization, iterative planner feedback, and the prompt template used to synthesize candidate agent programs. The feedback uses training execution traces to inform later candidate sampling.

O Hyperparameters

  • Table 8 groups shared pipeline settings, task-specific training configurations, and per-task verifier and solver timeouts.The task-specific configurations cover GSM-Symbolic and Symbolic Regression.Source: O Hyperparameters · p. 38, Table 8 · p. 39
  • Task-specific training configurations in Table 8 are reported for GSM-Symbolic and Symbolic Regression.The table also reports shared pipeline settings and per-task verifier and solver timeouts.Source: O Hyperparameters · p. 38, Table 8 · p. 39

P Planner Feedback

  • After each search–verify–learn iteration, SEVerA builds feedback from the current best candidate’s execution traces on the training data.The planner receives the previous program’s performance score and per-example error diagnostics.Source: P Planner Feedback · p. 39
  • For each failed training example, feedback includes its input, the agent’s output, and the associated verification, grammar, or answer error.The planner is asked to describe each failure in one or two sentences and suggest a fix.Source: P Planner Feedback · p. 39
  • The planner’s per-example descriptions and suggested fixes enter the next candidate-sampling context, helping it address recurring failures in FGGM definitions and prompting programs.The feedback is collected as I′ for the next iteration.Source: P Planner Feedback · p. 39

Q Planner LLM Prompt

  • At each search–verify–learn iteration, the planner prompt template is populated with the task specification, postcondition, operator library, agent signature, and prior-trace feedback.Figure 8 presents the prompt template.Source: Q Planner LLM Prompt · p. 39, Figure 8 · p. 40

R Proof Details

The proofs establish checker correctness and show how verified local contracts yield global guarantees for composed and selected programs. Under stated assumptions, they also give a sufficient condition for constructing a contract-satisfying program with no greater loss than the initial generative model.

R Proof Details

  • For valid FGGM calls with quantifier-free Ψ_l, the checker returns true exactly when Ψ_l holds, assuming Φ_l holds.The proof uses structural induction, with computable library functions evaluating atomic predicates.Source: R Proof Details · pp. 40–41
  • For any valid FGGM and parameter setting, its output satisfies Ψ_l whenever Φ_l holds.The rejection sampler returns a checker-approved sample or a valid fallback; checker soundness supports the guarantee.Source: R Proof Details · pp. 41–42
  • If P{Θ} ≠ ⊥, the composed program satisfies the global contract for all parameter settings and inputs meeting Φ.The proof combines the local contracts established for each FGGM with verification of the composed program.Source: R Proof Details · p. 42
  • Under φ_A, any selected program f* ≠ ⊥ satisfies the global contract for every input meeting Φ.Theorem 5.4 derives this soundness from the property that every candidate in the program set satisfies the contract.Source: R Proof Details · p. 42
  • If the loss penalizes violations, Ψ is quantifier-free, and a satisfying non-parametric program exists, a contract-satisfying program has loss no greater than the initial generative model’s.The theorem further states that loss strictly improves when the initial model violates Ψ on some data input.Source: R Proof Details · pp. 42–43

Related papers

Loading 2603.25111v2…