SEVerA：自己進化するエージェントの検証済み合成

要旨: 近年の進展により、プログラム修復や科学的発見といったタスクにおいて、自律的に自己進化するLLMエージェントが有効であることが示されてきました。このパラダイムでは、プランナーLLMが、LLMを含むパラメトリックモデルを呼び出すエージェント・プログラムを合成し、その後、タスクごとにそれらを調整して性能を向上させます。しかし、既存の自己進化型エージェント・フレームワークには、安全性や正しさに関する形式的な保証がありません。そのようなプログラムは、未知の入力に対して自律的に実行されることが多いため、この保証の欠如は信頼性とセキュリティに関する懸念を引き起こします。本研究では、エージェント的なコード生成を、制約付き学習問題として定式化します。ここでは、ハードな形式仕様と、タスク有用性を捉えるソフト目標を組み合わせます。そこで、形式的にガードされた生成モデル（Formally Guarded Generative Models; FGGM）を導入します。FGGMにより、プランナーLLMは、一階述語論理を用いて、生成モデル呼び出しごとに形式的な出力契約（出力の取り決め）を指定できます。各FGGMの呼び出しは、基盤となるモデルをリジェクション・サンプラーでラップし、検証済みのフォールバックを組み込みます。これにより、あらゆる入力およびパラメータ設定に対して、返されるすべての出力が契約を満たすことが保証されます。FGGMを基に、三段階フレームワークであるSEVerA（Self-Evolving Verified Agents）を提示します。Search（探索）は、FGGM呼び出しを含む候補となるパラメトリック・プログラムを合成します。Verification（検証）は、パラメータ値のすべてに対してハード制約に関する正しさを証明し、問題を制約なし学習に還元します。そしてLearning（学習）は、GRPOスタイルのファインチューニングを含む、スケーラブルな勾配ベース最適化を適用して、正しさを保ったままソフト目標を改善します。SEVerAを、Dafnyプログラム検証、記号数学の合成、ならびにポリシー準拠のエージェント的ツール利用（ au^2-bench）で評価します。すべてのタスクにおいてSEVerAは、拘束違反をゼロに保ちながら、制約なしおよびSOTAのベースラインよりも性能を向上させます。これにより、形式的な行動制約は正しさを保証するだけでなく、合成をより高品質なエージェントへと導くことが示されます。