Formal Verification of Agentic Systems over Operational Data

📄 arXiv: 2608.03609v1 📥 PDF

作者: Alejandro J. Mercado, Alessio Lomuscio

分类: cs.AI

发布日期: 2026-08-04

备注: 21 pages, including appendix; 0 figures

💡 一句话要点

提出STEADs框架以解决LLM驱动系统的验证问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大语言模型 代理系统 形式验证 工具编排 计算树逻辑 操作数据 系统级保证

📋 核心要点

  1. 现有方法在验证LLM驱动的代理系统时缺乏系统级的保证，主要集中在代理接口层面，无法有效处理持久操作数据的验证问题。
  2. 本文提出了状态工具启用代理部署（STEADs）框架，定义了验证问题并识别了FO-CTL规范的保留条件，提供了一种新的验证方法。
  3. 通过引入规范部署包装器，确保了数据标识符的重命名与工具调用的一致性，验证过程在有限域下为PSPACE完全，具有较高的理论价值。

📝 摘要（中文）

随着大语言模型（LLMs）在实际工作流程中的广泛应用，如何在部署前验证这些系统以确保其符合业务需求变得尤为重要。现有方法主要在代理接口层面进行约束或分析，缺乏系统级的保证。本文研究了由单个LLM和工具编排框架组成的代理系统的验证，正式定义为状态工具启用代理部署（STEADs），并给出了其语义。我们定义了基于一阶计算树逻辑（FO-CTL）规范的验证问题，并证明其不可判定性。通过有限域限制，我们识别了FO-CTL规范精确保留的充分条件，验证过程为PSPACE完全。关键要求是数据中的不透明标识符重命名必须对应于所选工具调用的重命名。我们展示了LLM驱动的代理可能违反此条件，并引入了一个规范部署包装器以保证这一点，同时保留已有的等变行为。最后，我们通过一个LLM代理协调案例管理工作流程来说明我们的框架。

🔬 方法详解

问题定义：本文旨在解决LLM驱动的代理系统在操作数据上的验证问题，现有方法无法提供系统级的保证，主要局限于代理接口层面。

核心思路：提出状态工具启用代理部署（STEADs）框架，定义验证问题并识别FO-CTL规范的保留条件，确保数据标识符与工具调用的一致性。

技术框架：整体架构包括LLM、工具编排框架和验证模块，首先对代理系统进行建模，然后通过FO-CTL规范进行验证，最后引入包装器以保证一致性。

关键创新：最重要的创新在于引入了规范部署包装器，确保数据标识符的重命名与工具调用的对应关系，从而解决了LLM驱动代理可能违反的条件。

关键设计：在设计中，重命名的不透明标识符必须与工具调用相对应，验证过程在有限域下为PSPACE完全，计算规范表示的复杂度为图同构难度。

🖼️ 关键图片

img_0
img_1
img_2

📊 实验亮点

实验结果表明，在有限域下，验证过程为PSPACE完全，且通过引入规范部署包装器，成功保证了数据标识符与工具调用的一致性，显著提升了系统的验证能力和可靠性。

🎯 应用场景

该研究的潜在应用领域包括智能客服、自动化工作流程管理和复杂系统的决策支持等。通过提供系统级的验证保证，能够提升LLM驱动系统在实际应用中的可靠性和安全性，具有重要的实际价值和未来影响。

📄 摘要（原文）

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.