論文の概要: SEVerA: Verified Synthesis of Self-Evolving Agents

• arxiv url: http://arxiv.org/abs/2603.25111v1
• Date: Thu, 26 Mar 2026 07:32:20 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-27 20:52:48.156326
• Title: SEVerA: Verified Synthesis of Self-Evolving Agents
• Title（参考訳）: SEVerA: 自己進化剤の確立された合成
• Abstract要約: 自己進化型エージェントフレームワークは、安全性や正確性の正式な保証を提供しない。 エージェントコード生成を制約付き学習問題として定式化し、ハードな形式仕様とソフトな目的とを組み合わせてタスクユーティリティをキャプチャする。 探索はFGGMコールを含む候補パラメトリックプログラムを合成し、検証は全てのパラメータ値に対する厳しい制約に関して正当性を証明し、制約のない学習に還元する。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: 近年の進歩は、自己進化型LLMエージェントがプログラム修復や科学的発見などのタスクに有効であることを示している。 このパラダイムでは、プランナーのLLMが、LLMを含むパラメトリックモデルを呼び出すエージェントプログラムを合成し、タスク毎に調整してパフォーマンスを向上させる。 しかし、既存の自己進化エージェントフレームワークは、安全性や正確性に関する正式な保証を提供していない。 このようなプログラムは目に見えない入力で自律的に実行されることが多いため、保証の欠如は信頼性とセキュリティ上の懸念を引き起こす。 エージェントコード生成を制約付き学習問題として定式化し、ハードな形式仕様とソフトな目的とを組み合わせてタスクユーティリティをキャプチャする。 本稿では,FGGM (Formally Guarded Generative Models) を導入し,一階述語論理を用いた各生成モデル呼び出しの形式的出力契約をプランナー LLM が指定できるようにする。 各FGGMコールは、下層のモデルを検証されたフォールバックでリジェクションサンプリングでラップし、返却された出力が任意の入力とパラメータ設定のコントラクトを満たすことを保証します。 FGGMをベースとしたSEVerA(Self-Evolving Verified Agents)は,3段階のフレームワークである。検索はFGGMコールを含む候補パラメトリックプログラムを合成し,検証はすべてのパラメータ値に対する厳しい制約に対して正当性を証明し,問題を制約なしの学習に還元し,学習はGRPOスタイルの微調整を含むスケーラブルな勾配に基づく最適化を適用し,正当性を保ちながらソフトな目標を改善する。 本研究では,Dafnyプログラムの検証,シンボリックな数学合成,およびポリシーに準拠したエージェントツールの使用(τ^2$-bench)に関するSEVerAを評価する。 タスク全体にわたって、SEVerAは制約違反をゼロとし、制約なしおよびSOTAベースラインのパフォーマンスを改善し、形式的な動作制約が正確性を保証するだけでなく、高品質なエージェントに対するステアシンセサイザーの合成も保証している。

関連論文リスト

• CAPO: Constraint-Aware Prompt Optimization for LLM Agents [9.4076372340902]
  大規模言語モデル(LLM)は、ツールやタスクの完全な使用をシステムプロンプトに依存するエージェントとして、ますます多くデプロイされている。 本稿では,プールベースリライトと適応的制約重み付けを組み合わせて,明示的な操作制約の下でシステムプロンプトを最適化するプリミティブ・デュアル手法CAPOを紹介する。 また,DCAPOを導入し,タスクエージェントの凍結を保ちながら,プールベースのGRPOでフィードバックと二重条件のリライタを訓練する。
  論文  参考訳（メタデータ） (2026-08-17T04:01:04Z)
• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。 既存のアプローチはそのようなシステムレベルの保証を提供していません。 本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
  論文  参考訳（メタデータ） (2026-08-04T13:01:30Z)
• GRACE-DS: a Guarded Reward-guided Agent Correction Environment in Data Science [39.146761527401424]
  GRACE-DSは、LSMを用いたオートMLエージェントの事前デプロイ評価のための、データサイエンスにおけるリワード誘導エージェント補正環境である。 エージェントをリアルなワークフローステージに公開し、計画やデータインスペクションから機能エンジニアリング、モデル開発、バリデーション、コード修正まで、最終提出まで。 これらの結果から、GRACE-DSはLLMベースのAutoMLエージェントが実運用環境下で機械学習を実行する能力を評価するための堅牢なプラットフォームとして確立された。
  論文  参考訳（メタデータ） (2026-06-14T19:58:06Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  本稿では,ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。 VASOは論理的に一貫性のないスキル契約を検証し、グローバルおよびローカルな時間的仕様に対してスキルによって誘発される計画を検証する。 Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100点未満の最適化サンプルを使用して97.2% の形式的な仕様準拠に達した。
  論文  参考訳（メタデータ） (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]
  品質駆動型推論時間スキャフォールドであるQoTを導入し,ユーザ目標をエンジニアリングステップの順序付きシーケンスに変換する。 QoTは、API設計、データ通信、ファイルシステムの3つの代表的なバックエンドエンジニアリング領域にまたがって評価する。
  論文  参考訳（メタデータ） (2026-03-10T23:49:09Z)
• Execution-State-Aware LLM Reasoning for Automated Proof-of-Vulnerability Generation [36.950993500170014]
  本稿では,PoV生成を反復的仮説検証法として再構成するエージェントフレームワークであるDrillAgentを提案する。 我々は、実世界のC/C++脆弱性の大規模なベンチマークであるSEC-bench上でDrillAgentを評価する。
  論文  参考訳（メタデータ） (2026-02-14T03:17:27Z)
• From Completion to Editing: Unlocking Context-Aware Code Infilling via Search-and-Replace Instruction Tuning [81.97788535387286]
  本稿では,エージェントによる検証・編集機構を統一された単一パス推論プロセスに内部化するフレームワークを提案する。 最小限のデータで、SRI-Coderは、ChatモデルがBaseモデルの完了性能を上回ることができる。 FIMスタイルのチューニングとは異なり、SRIは一般的なコーディング能力を保持し、標準のFIMに匹敵する推論遅延を維持する。
  論文  参考訳（メタデータ） (2026-01-19T20:33:53Z)
• Evaluating Implicit Regulatory Compliance in LLM Tool Invocation via Logic-Guided Synthesis [18.51135049856393]
  我々は,非構造化規則を線形時間論理託に変換するフレームワークであるLogiSafetyGenを導入し,論理誘導ファジングを用いて,有効かつ安全クリティカルなトレースを合成する。 このフレームワーク上に構築したLogiSafetyBenchは,LLMが機能目標と遅延コンプライアンスルールの両方を満たすPythonプログラムを生成するために必要な,240の人間認証タスクからなるベンチマークである。 13種類のSOTA (State-of-the-art) LLMの評価により、より優れた機能的正当性を達成したにもかかわらず、安全よりもタスク完了を優先し、非準拠な振る舞いをもたらすことが判明した。
  論文  参考訳（メタデータ） (2026-01-13T03:55:18Z)
• Reasoning with Confidence: Efficient Verification of LLM Reasoning Steps via Uncertainty Heads [104.9566359759396]
  データ駆動の不確実性スコアに基づくステップレベルの推論検証の軽量な代替案を提案する。 本研究は, LLMの内部状態が不確実性を符号化し, 信頼性の高い検証信号として機能することが示唆された。
  論文  参考訳（メタデータ） (2025-11-09T03:38:29Z)
• Alita-G: Self-Evolving Generative Agent for Agent Generation [54.49365835457433]
  汎用エージェントをドメインエキスパートに変換するフレームワークであるALITA-Gを提案する。 このフレームワークでは、ジェネラリストエージェントが対象ドメインタスクのキュレートされたスイートを実行する。 計算コストを削減しながら、大きな利益を得ることができます。
  論文  参考訳（メタデータ） (2025-10-27T17:59:14Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• Collab: Controlled Decoding using Mixture of Agents for LLM Alignment [90.6117569025754]
  人間のフィードバックからの強化学習は、大規模言語モデルを整合させる効果的な手法として現れてきた。 制御された復号化は、再訓練せずに推論時にモデルを整列するメカニズムを提供する。 本稿では,既存の既成のLCMポリシを活用するエージェントベースのデコーディング戦略の混合を提案する。
  論文  参考訳（メタデータ） (2025-03-27T17:34:25Z)
• SagaLLM: Context Management, Validation, and Transaction Guarantees for Multi-Agent LLM Planning [2.1331883629523634]
  SagaLLMは、現在のLLMベースの計画システムの4つの基本的な制限に対処するために設計された構造化マルチエージェントアーキテクチャである。 Sagaトランザクションパターンを永続メモリ、自動補償、独立バリデーションエージェントに統合することで、このギャップを埋める。 不確実性の下では、一貫性、検証精度、適応調整において大幅な改善が達成される。
  論文  参考訳（メタデータ） (2025-03-15T01:43:03Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。