Search papers, labs, and topics across Lattice.
SEVerA introduces a framework for synthesizing self-evolving LLM agents with formal guarantees of safety and correctness by formulating agentic code generation as a constrained learning problem. It uses Formally Guarded Generative Models (FGGM) to allow planner LLMs to specify formal output contracts for each generative model call, ensuring every output satisfies the contract via a rejection sampler with verified fallback. SEVerA demonstrates zero constraint violations and improved performance over baselines on tasks like program verification and tool use, suggesting formal constraints can enhance agent quality.
Guaranteeing safety and correctness in self-evolving LLM agents is now possible: SEVerA achieves zero constraint violations while *improving* performance.
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.
