SEVerA: 自己進化エージェントの検証可能な合成

SEVerA: Verified Synthesis of Self-Evolving Agents

March 26, 2026

著者: Debangshu Banerjee, Changming Xu, Gagandeep Singh

cs.AI

要旨

最近の研究により、プログラム修正や科学的発見などのタスクにおいて、自己進化型大規模言語モデル（LLM）エージェントの有効性が実証されている。このパラダイムでは、プランナーLLMがパラメトリックモデル（LLMを含む）を呼び出すエージェントプログラムを合成し、タスクごとにチューニングすることで性能を向上させる。しかし、既存の自己進化型エージェントフレームワークには安全性や正当性に関する形式的保証が存在しない。このようなプログラムは未知の入力に対して自律的に実行されることが多いため、保証の欠如は信頼性とセキュリティ上の懸念を引き起こす。 我々はエージェントコード生成を、厳密な形式的仕様とタスク効用を捉えた軟性目的を組み合わせた制約付き学習問題として定式化する。**形式的に保護された生成モデル（FGGM）**を提案し、プランナーLLMが一階述語論理を用いて各生成モデル呼び出しに対する形式的な出力契約を指定できるようにする。各FGGM呼び出しは、検証済みのフォールバック機能を持つ拒否サンプラーで基礎となるモデルをラップし、あらゆる入力とパラメータ設定に対して返される出力が契約を満たすことを保証する。 FGGMを基盤として、3段階のフレームワーク**SEVerA（自己進化検証エージェント）**を構築する：**探索**段階ではFGGM呼び出しを含む候補パラメトリックプログラムを合成し、**検証**段階ではすべてのパラメータ値に対する厳密な制約の正当性を証明することで問題を制約なし学習に還元し、**学習**段階ではGRPO様のファインチューニングを含むスケーラブルな勾配ベース最適化を適用して、正当性を保ちつつ軟性目的を改善する。 Dafnyプログラム検証、記号数学合成、ポリシー準拠型エージェントツール使用（τ^2-bench）における評価では、SEVerAはすべてのタスクで制約違反をゼロに抑えつつ、制約なしおよび最先端ベースラインを上回る性能を達成した。これは形式的な振る舞い制約が正当性を保証するだけでなく、より高品質なエージェントへの合成を誘導することを示している。

English

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.