基于操作数据的智能体系统的形式化验证

中文摘要 AI 辅助

由大语言模型（LLM）驱动的智能体系统正越来越多地被部署到现实工作流中，这些系统会对持久化的操作数据进行操作。在部署前，需要针对控制工作流执行和数据演化的业务需求对这些系统进行验证。然而，现有方法无法提供此类系统级保证，因为它们主要在智能体的接口层面约束或分析行为。本文研究了由单个LLM和工具编排层组成的智能体系统在关系型操作数据上的验证问题，将其形式化为有状态工具使能智能体部署（STEADs），给出其语义，定义针对一阶计算树逻辑（FO-CTL）规范的验证问题，并证明该问题是不可判定的。我们确定了在有限域限制下精确保留FO-CTL规范的充分条件，在此限制下验证问题是PSPACE完全的。关键要求是，数据中不透明标识符的重命名必须对应地重命名所选的工具调用。我们证明由LLM驱动的智能体可能违反该条件，并引入了一个规范部署包装器，该包装器可为任意基础智能体保证该条件，同时保留已有的等变行为。我们证明，计算该构造所需的规范表示是图同构困难的。最后，我们在一个编排案例管理工作流的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.

补充信息

备注

21 pages, including appendix; 0 figures