論文の概要: Formal Verification of Agentic Systems over Operational Data

• arxiv url: http://arxiv.org/abs/2608.03609v1
• Date: Tue, 04 Aug 2026 13:01:30 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-05 15:30:23.196075
• Title: Formal Verification of Agentic Systems over Operational Data
• Title（参考訳）: 操作データによるエージェントシステムの形式的検証
• Authors: Alejandro J. Mercado, Alessio Lomuscio,
• Abstract要約: 大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。 既存のアプローチはそのようなシステムレベルの保証を提供していません。 本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
• 参考スコア（独自算出の注目度）: 59.98246281888422
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world workflows where they act on persistent operational data. Before deployment, these systems need to be verified against business requirements that govern workflow execution and data evolution. However, existing approaches do not provide such system-level guarantees, as they mainly constrain or analyse behaviour at the agent's interface level. We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data. We formalise them as Stateful Tool-Enabled Agentic Deployments (STEADs), give their semantics, define the problem of verifying them against First-Order Computation Tree Logic (FO-CTL) specifications, and show that it is undecidable. We identify sufficient conditions for exact preservation of FO-CTL specifications under a finite-domain restriction, over which verification is PSPACE-complete. The key requirement is that renaming opaque identifiers in the data must correspondingly rename the selected tool calls. We show that LLM-driven agents can violate this condition and introduce a canonical deployment wrapper that guarantees it for arbitrary base agents while preserving already-equivariant behaviour. We prove that computing canonical representations required by this construction is graph-isomorphism-hard. Finally, we illustrate our framework on an LLM agent orchestrating a case-management workflow.
• Abstract（参考訳）: 大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データに作用する現実世界のワークフローにますますデプロイされている。 デプロイメントの前には、ワークフローの実行とデータ進化を管理するビジネス要件に対して、これらのシステムを検証する必要がある。 しかし、既存のアプローチは、エージェントのインターフェイスレベルでの振る舞いを主に制約または分析するため、そのようなシステムレベルの保証を提供していません。 本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。 我々は、それらをステートフルツール許容エージェントデプロイ(STEAD)として形式化し、セマンティクスを与え、それらをFO-CTL(First-Order Computation Tree Logic)仕様で検証する問題を定義し、決定不能であることを示します。 PSPACE完全である有限領域制限の下でFO-CTL仕様を正確に保存するための十分な条件を同定する。 キーとなる要件は、データ内の不透明な識別子をリネームする必要があることだ。 LLMを駆動するエージェントは、この条件に反し得ることを示し、任意のベースエージェントに対して、既に等価な動作を保ちながら、それを保証する標準配置ラッパーを導入する。 この構成で必要とされる正規表現の計算がグラフ同型ハードであることを証明する。 最後に、ケース管理ワークフローを編成するLLMエージェントについて、我々のフレームワークを説明します。

関連論文リスト

• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  我々は、スケジューリング、検証、メモリ、ベンチマーク、安全性をシステムレベルのサービスとして提供するPhyAgentOSを紹介します。 セッション中心のセッションは、スケジューリング、互換性、監督された実行、エビデンス収集、受け入れの最小単位として、アクションではなくセッションを扱う。 SessionVerifierは、実行終了とセマンティックタスク完了を、成功、失敗、または再計画のエビデンスに基づいて判断する。 ベンチマークはデプロイメントセッションと検証パスを再利用するので、結果は実際の実行に遡る。
  論文  参考訳（メタデータ） (2026-07-18T04:46:53Z)
• VADAOrchestra: Neurosymbolic Orchestration of Adaptive Reasoning Workflows [47.70653885737167]
  実世界の環境での意思決定は、固定されたスクリプトに従うことはめったにない。代わりに、動的推論プロセスとして展開する。 VADAOrchestraは、複雑な推論過程をモデル化するニューロシンボリックなフレームワークである。
  論文  参考訳（メタデータ） (2026-06-21T13:10:48Z)
• 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)
• Towards Security-Auditable LLM Agents: A Unified Graph Representation [22.355591892994642]
  本稿ではエージェントセキュリティ監査のための統合構造表現であるエージェントBOMを提案する。 エージェントBOMは、クロスセッションメモリ中毒やツール誤用など、ステルス攻撃チェーンを再構築できることを示す。 Agent-BOMは複雑なエージェントエコシステムにおける根本原因分析とセキュリティ適応のための統一的で監査可能な基盤を提供する。
  論文  参考訳（メタデータ） (2026-05-07T18:14:29Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• AGENTIF: Benchmarking Instruction Following of Large Language Models in Agentic Scenarios [51.46347732659174]
  LLM(Large Language Models)は、現実世界のエージェントアプリケーションにおいて高度な機能を示す。 AgentIFは、エージェントシナリオでLLM命令に従う能力を体系的に評価する最初のベンチマークである。
  論文  参考訳（メタデータ） (2025-05-22T17:31:10Z)

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

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