SEVerA: Verified Synthesis of Self-Evolving Agents

• URL: http://arxiv.org/abs/2603.25111v1
• Date: Thu, 26 Mar 2026 07:32:20 GMT
• Title: SEVerA: Verified Synthesis of Self-Evolving Agents
• Abstract summary: Self-evolving agent frameworks provide no formal guarantees of safety or correctness.<n>We formulate agentic code generation as a constrained learning problem, combining hard formal specifications with soft objectives capturing task utility.<n>We present SEVerA, 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.
• Score: 12.9624447364193
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• CAPO: Constraint-Aware Prompt Optimization for LLM Agents [9.4076372340902]
  Large language models (LLMs) are increasingly deployed as agents that rely on system prompts to use tools and complete tasks.<n>We introduce CAPO, a primal-dual method that combines pool-based rewrites with adaptive constraint weighting to optimize system prompts under explicit operational constraints.<n>We also introduce DCAPO, which trains a feedback- and dual-conditioned rewriter with pool-based GRPO while keeping the task agent frozen.
  arXiv  Detail & Related papers  (2026-08-17T04:01:04Z)
• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
  arXiv  Detail & Related papers  (2026-08-04T13:01:30Z)
• GRACE-DS: a Guarded Reward-guided Agent Correction Environment in Data Science [39.146761527401424]
  GRACE-DS is a Reward-guided Agent Correction Environment in Data Science for pre-deployment evaluation of LLM-powered AutoML agents.<n>It exposes agents to realistic workflow stages, from planning and data inspection through feature engineering, model development, validation, and code repair to final submission.<n>These results establish GRACE-DS as a robust platform for assessing the capacity of LLM-based AutoML agents to execute machine learning under production-like conditions.
  arXiv  Detail & Related papers  (2026-06-14T19:58:06Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  We introduce VASO, a framework for verification-guided self-evolution of robot skill contracts.<n>VASO verifies logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications.<n>On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples.
  arXiv  Detail & Related papers  (2026-06-03T20:02:35Z)
• Quality-Driven Agentic Reasoning for LLM-Assisted Software Design: Questions-of-Thoughts (QoT) as a Time-Series Self-QA Chain [0.0]
  We introduce Questions-of-Thoughts (QoT), a quality-driven inference-time scaffold that turns a user goal into an ordered sequence of engineering steps.<n>We evaluate QoT across three representative backend engineering domains: API Design, Data Communication, and File Systems.
  arXiv  Detail & Related papers  (2026-03-10T23:49:09Z)
• Execution-State-Aware LLM Reasoning for Automated Proof-of-Vulnerability Generation [36.950993500170014]
  We present DrillAgent, an agentic framework that reformulates PoV generation as an iterative hypothesis-verification-refinement process.<n>We evaluate DrillAgent on SEC-bench, a large-scale benchmark of real-world C/C++ vulnerabilities.
  arXiv  Detail & Related papers  (2026-02-14T03:17:27Z)
• From Completion to Editing: Unlocking Context-Aware Code Infilling via Search-and-Replace Instruction Tuning [81.97788535387286]
  We propose a framework that internalizes the agentic verification-and-editing mechanism into a unified, single-pass inference process.<n>With minimal data, SRI-Coder enables Chat models to surpass the completion performance of their Base counterparts.<n>Unlike FIM-style tuning, SRI preserves general coding competencies and maintains inference latency comparable to standard FIM.
  arXiv  Detail & Related papers  (2026-01-19T20:33:53Z)
• Evaluating Implicit Regulatory Compliance in LLM Tool Invocation via Logic-Guided Synthesis [18.51135049856393]
  We introduce LogiSafetyGen, a framework that converts unstructured regulations into Linear Temporal Logic oracles and employs logic-guided fuzzing to synthesize valid, safety-critical traces.<n>Building on this framework, we construct LogiSafetyBench, a benchmark comprising 240 human-verified tasks that require LLMs to generate Python programs that satisfy both functional objectives and latent compliance rules.<n> Evaluations of 13 state-of-the-art (SOTA) LLMs reveal that larger models, despite achieving better functional correctness, frequently prioritize task completion over safety, which results in non-compliant behavior.
  arXiv  Detail & Related papers  (2026-01-13T03:55:18Z)
• Reasoning with Confidence: Efficient Verification of LLM Reasoning Steps via Uncertainty Heads [104.9566359759396]
  We propose a lightweight alternative for step-level reasoning verification based on data-driven uncertainty scores.<n>Our findings suggest that the internal states of LLMs encode their uncertainty and can serve as reliable signals for reasoning verification.
  arXiv  Detail & Related papers  (2025-11-09T03:38:29Z)
• Alita-G: Self-Evolving Generative Agent for Agent Generation [54.49365835457433]
  We present ALITA-G, a framework that transforms a general-purpose agent into a domain expert.<n>In this framework, a generalist agent executes a curated suite of target-domain tasks.<n>It attains strong gains while reducing computation costs.
  arXiv  Detail & Related papers  (2025-10-27T17:59:14Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• Collab: Controlled Decoding using Mixture of Agents for LLM Alignment [90.6117569025754]
  Reinforcement learning from human feedback has emerged as an effective technique to align Large Language models.<n>Controlled Decoding provides a mechanism for aligning a model at inference time without retraining.<n>We propose a mixture of agent-based decoding strategies leveraging the existing off-the-shelf aligned LLM policies.
  arXiv  Detail & Related papers  (2025-03-27T17:34:25Z)
• SagaLLM: Context Management, Validation, and Transaction Guarantees for Multi-Agent LLM Planning [2.1331883629523634]
  SagaLLM is a structured multi-agent architecture designed to address four foundational limitations of current LLM-based planning systems.<n>It bridges this gap by integrating the Saga transactional pattern with persistent memory, automated compensation, and independent validation agents.<n>It achieves significant improvements in consistency, validation accuracy, and adaptive coordination under uncertainty.
  arXiv  Detail & Related papers  (2025-03-15T01:43:03Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.