面向运行数据的Agentic系统形式化验证

基于大规模语言模型的智能体在现实工作流程中被部署，它们在持续操作数据上执行任务。在部署之前，这些系统需要验证其业务需求，这些需求控制和影响工作流的执行以及数据的变化。然而，现有的方法并未提供这样的系统级保证，因为它们主要约束或分析行为在代理接口级别。我们研究由单个语言模型和工具调度器组成的智能体系统的验证。我们将它们作为状态化工具-驱动型智能体部署（STEADs）来定义，并给出其语义。我们定义了通过第一-阶计算树逻辑（FO-CTL）规格进行验证的问题，证明该问题不可解。我们识别出在有限域限制下FO-CTL规范的精确保真条件，此时验证是PSPACE-complete。关键要求是，在数据中重命名不透明标识符时，必须相应地重命名选择工具调用。我们展示了LLM驱动代理可以违反这一条件，并引入一个可唯一化部署包装器来保证任意基础代理的行为不变且保持已等价性。我们证明了计算这种构造所需的唯一化表示是图同态难的。最后，我们在一个由语言模型驱动的工作流管理案例中说明我们的框架。