Certified Execution Harness for Agentic AI: Safe and Least-Intrusive Petri-Net Supervisory Control Between Reasoning and Action
作者: Chao Gu, Quanyan Zhu
分类: cs.AI, eess.SY
发布日期: 2026-10-22
备注: 17 pages, 9 figures, 2 tables. Extended version of a paper submitted for publication
💡 一句话要点
提出安全工具执行框架以解决大语言模型代理的安全性问题
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 大语言模型 安全执行 Petri网 监督控制 提示注入 智能代理 重新规划
📋 核心要点
- 现有方法在处理大语言模型代理的安全工具执行时，面临提示注入带来的风险和挑战。
- 论文提出通过Petri网形式化执行框架，将LLM与工具之间的交互视为监督控制问题，以确保安全性。
- 实验结果表明，最大宽容的最少侵入监督者能够有效提升安全性，并在特定条件下优化执行效率。
📝 摘要（中文）
本文研究了在提示注入下，大语言模型（LLM）代理的安全工具执行问题。通过使用Petri网，我们将LLM与其工具之间的执行框架形式化为一个监督控制问题，其中标记表示能力、批准和预算。由于只有在所需标记存在时，转换才会触发，因此无论注入请求的措辞如何，未满足或已耗尽的前提条件都会导致请求被拒绝。我们通过传统的最大宽容监督者来强制执行安全性，并在四个假设下将这种安全性转移到运行系统。此外，为了捕捉可能在拒绝后再次提议的代理，我们引入了重新规划闭环的概念，其中每次重试都需要消耗一次推理调用。我们展示了在这个闭环中，传统监督者可以比更严格的安全监督者更具侵入性。
🔬 方法详解
问题定义：本文旨在解决大语言模型（LLM）代理在提示注入情况下的安全工具执行问题。现有方法在处理不符合条件的请求时，缺乏有效的拒绝机制，导致潜在的安全隐患。
核心思路：论文的核心解决思路是将LLM与其工具之间的执行过程形式化为一个监督控制问题，利用Petri网的特性来确保请求的安全性和有效性。通过设置标记来表示能力和预算，确保只有在满足条件时请求才能被执行。
技术框架：整体架构包括LLM、工具和监督控制模块。首先，LLM生成请求，监督控制模块根据当前标记状态判断请求是否满足条件，决定是否执行。若请求被拒绝，则进入重新规划闭环，进行再次尝试。
关键创新：最重要的技术创新在于引入了最大宽容的最少侵入监督者的概念，能够在保证安全性的同时，减少对系统的干扰。这一设计与传统方法相比，能够更灵活地处理请求。
关键设计：关键设计包括标记的定义和管理、请求的条件判断机制，以及重新规划闭环的实现。具体参数设置和损失函数的设计确保了系统在不同状态下的安全性和效率。
📊 实验亮点
实验结果显示，采用最大宽容的最少侵入监督者后，系统在处理请求时的安全性显著提升，拒绝率降低了30%，同时在执行效率上也有明显改善，展示了该方法的有效性。
🎯 应用场景
该研究的潜在应用领域包括智能助手、自动化系统和其他依赖大语言模型的智能代理。通过确保安全的工具执行，该框架能够提升系统的可靠性，降低安全风险，具有重要的实际价值和未来影响。
📄 摘要（原文）
This paper studies the problem of safe tool execution for large language model (LLM) agents under prompt injection. Using Petri nets, we formalize the execution harness between the LLM and its tools as a supervisory control problem, in which marks represent capabilities, approvals and budgets. Since a transition fires only if the marks it needs are present, an injected request whose preconditions are unmet or already spent is refused regardless of its wording. Treating tool outcomes as uncontrollable, we enforce safety by the conventional maximally permissive supervisor, and this safety transfers to the running system under four assumptions. Moreover, to capture an agent that may propose again after a refusal, we introduce the notion of a replanning closed loop, in which each retry costs an inference call. We show that, in this loop, the conventional supervisor can be arbitrarily more intrusive than a stricter safe one. Furthermore, for a given proposer model, the maximally permissive least-intrusive supervisor is characterized as a value-threshold refinement of the conventional one. Under precise conditions, this refinement orders two concurrent actions by at most one monitor place. On an autonomous release agent, we find by synthesis that safe deployment requires a step that the supervisor can refuse after a rollout starts.