可证明安全的智能体护栏

# 可证明安全的智能体护栏

**来源：** https://arxiv.org/html/2605.29251

Weiming Zhang [[email protected]](https://arxiv.org/html/2605.29251v1/mailto:[email protected])  
中国科学技术大学，合肥，中国

Kejiang Chen [[email protected]](https://arxiv.org/html/2605.29251v1/mailto:[email protected])  
中国科学技术大学，合肥，中国

Han Fang [[email protected]](https://arxiv.org/html/2605.29251v1/mailto:[email protected])  
中国科学技术大学，合肥，中国

Nenghai Yu [[email protected]](https://arxiv.org/html/2605.29251v1/mailto:[email protected])  
中国科学技术大学，合肥，中国

###### 摘要.
随着大型语言模型从有边界的生成式引擎转变为具有广泛执行权限的智能体，人工智能失控成为人工智能安全领域的一场根本性危机。现有防御架构严重依赖经验性语义护栏和概率性大模型裁决机制，这些方法在面对复杂的语义符号解耦攻击时，无法提供确定性的安全下限。为克服这一经验性语义护栏困境，本文提出了一种基于逻辑推理根本局限性的新型智能体安全范式。基于该范式，我们进一步引入了一个可执行证明约束动作（ePCA）框架，该框架采用神经符号隔离架构。该框架放弃了对自然语言的语义信任，强制智能体在执行物理操作前将其意图无损形式化为一阶逻辑数学约束。对宏观和微观二维动态对抗系统的实证评估表明，我们的形式化验证机制在评估场景中实现了零攻击成功率和零误报率，且计算延迟极低。本研究为在明确系统假设条件下构建有条件的形式化基础，以及为未来智能系统构筑底层防御基础提供了一种工程范式。

**可证明安全，智能体，护栏**

††ccs: 安全与隐私 逻辑与验证

## 1. 引言

1976年，为应对远程机器互联带来的安全挑战，Whitfield Diffie 和 Martin E. Hellman 开创了密码学的新方向，提出了非对称（公钥）密码学 (DIFFIE and HELLMAN, 1976)。他们引入了可证明安全的概念，将密码安全性归约为计算复杂性假设。公钥密码学的深远意义在于其应用远远超出了安全通信的范畴，能够建立密码协议来解决虚拟世界中的信任问题。半个世纪以来，安全理论与技术在 Diffie 和 Hellman 提出的基础思想上不断发展。这是因为，从互联网、移动网络到云计算，远程互联引入的安全需求的根本性质始终未变。

参见图注 图 1. AI失控的风险迫切需要底层安全技术的转型。

2026年，如同1976年的 Diffie 和 Hellman，我们正站在一场巨大变革的门槛上。如果说上一个互联网安全时代影响了人类发展的轨迹，那么当前AI失控的风险则关乎人类的生存。如图1所示，全新的安全需求已经涌现。由大模型驱动的智能体能够进行复杂推理、多步骤规划和独立决策，推动人工智能快速迈向自我递归迭代。智能体超越人类智能并脱离人类控制的风险已成为现实。现有的经验性安全方法，如价值观对齐和经验性语义护栏，无法保证通用人工智能（AGI）和超级人工智能（ASI）的可控性。“AI失控风险”本质上不同于“远程互联”所带来的安全问题。密码学攻击与防御根植于计算；因此，Diffie 和 Hellman 基于（人类）智能的计算局限性构建了安全的基石。由于AI能够思考和推理，一个自然的问题随之而来：如何在逻辑推理的局限性下，从理论上可证明地确保智能体动作的可控性？哥德尔不完备定理和 Turing 不可判定定理可能为从数学底层构建形式化的符号强制层提供了理论基础。如果不安全动作可以被形式化地转化为“逻辑悖论”或“不可判定命题”，那么试图突破安全边界的大模型将不可避免地陷入逻辑死锁或停滞状态，如同一台被困在“第22条军规”中的机器。

**智能体的安全局限性。**

为了更好地理解这种范式转变的紧迫性，有必要审视当前智能体安全的现状以及现有防御的根本局限性。大型语言模型的激增打破了被动语义处理的静态边界，推动AI向能够进行多步规划和动态工具操作的智能体发展 (Yao et al., 2023; Varadharajan, 2000; Bagdasarian et al., 2024; Hu et al., 2025; Greshake et al., 2023)。这种从文本生成到物理干预的进化飞跃赋予了智能体前所未有的系统级权限 (Shi et al., 2024; Liu et al., 2025a)，暴露出当前防御架构的结构性弱点。以 OpenClaw¹ 为例（一个开源智能体操作环境），它无意中将底层操作系统的完整读写权限和外部数据接口访问权限直接暴露给了推理模型 (Liu et al., 2026a; Wu et al., 2025)。当这种固有的逻辑不稳定性与泛滥的系统权限相结合时，即使是微小的上下文欺骗或工具节点投毒也能触发级联故障，摧毁整体防御 (Raza et al., 2025)。最近针对该生态系统的大量通用漏洞披露集群 (Ying et al., 2026; Suwansathit et al., 2026) 深刻展示了这种权限膨胀的系统性灾难。面对智能体的系统级威胁，现有主流防御架构已暴露出结构性局限。一方面，传统的基于无状态单步模式匹配的静态访问控制和低级行为隔离机制，在自然语言工具调用背后的高维意图方面存在语义鸿沟 (Li et al., 2025)。这使得它们极易受到高级攻击者使用基于时间有效载荷分割策略等逻辑方法进行的静默渗透 (Chang et al., 2025)。另一方面，为了弥合这一语义鸿沟，业界广泛采用 LLM-as-a-Judge 和经验性语义护栏作为协议防御手段。这种同构的经验性语义护栏范式对于广泛的合规性非常有效，但容易出现上下文遗忘和错误授权等问题。在此类对抗场景中，恶意实体可以轻易利用看似合规的自然语言修辞来完美伪装和隐藏危险的底层调用指令 (Shi et al., 2024; Deng et al., 2026)。这种依赖于经验性语义监督的同构防御范式，在提供可验证的安全下限方面面临结构性限制 (Glukhov et al., 2023)。因此，这种经验性语义护栏范式从根本上不足以提供可验证的安全保障，迫切需要向构建逻辑严密、独立的运行时形式化验证范式转变。

参见图注 图 2. 从经验性安全到智能体系统的可证明安全。

虽然持续叠加语义审查规则对于通用内容对齐仍然非常有价值，但仅依赖经验性语义护栏难以满足高权限自主操作所需的保障 (Geng et al., 2026)。解决这一挑战需要的不是增量改进，而是转向一种新的范式以实现可证明安全。核心挑战在于，控制自主智能体的高维连续行为不能通过启发式地修补语义过滤器来解决；它需要形式化可判定的约束。安全防御的核心必须完全脱离不可靠的语义博弈论，转向基于形式化代数演算的确定性控制 (Garavel and Graf, 2013; Seshia et al., 2022)。这一推论并非孤例。形式逻辑和神经符号架构的理论突破 (Tegmark and Omohundro, 2023) 也表明，为高阶智能系统提供可证明的安全下限是可能的。

**我们的解决方案。**

因此，我们提出了一种从概率性保护到基于逻辑悖论的可证明防御的范式转变。与传统的证明携带代码（PCC）不同——后者会引入额外的推理开销，并且无法保证模型生成的证明与实际执行之间的一致性，可能创造新的攻击面——我们的方法直接从可执行动作中推导出证明。逻辑悖论指的是行为形式逻辑的不一致性，即智能体的意图动作同时要求并违反系统安全不变量，从而导致可证明的死锁，阻止执行。通过将未经授权的代理行为严格映射到可证明的逻辑死锁上，我们可以在结构上阻止恶意行为的执行。当面对这种死锁时，智能体违反公理的动作轨迹不仅产生低概率输出，而且在动作图中会遇到可证明的不可达状态，从而通过逻辑上可验证的不可达性在逻辑上阻止未经授权的执行。基于此分析，我们朝着更严格的智能体安全执行范式迈进了一步。我们引入了可执行证明约束动作（ePCA）框架。我们不依赖模型内部的语义推理，而是将安全执行外部化为一个形式化结构化且可验证的执行层。该层在执行前确定性地评估动作是否满足预定义的安全约束，从而在运行时阻止不安全的状态转换。图2展示了从经验性、经验驱动的护栏到形式化强制验证架构的转变。这些保证在明确界定的执行接口和验证保真度假设下成立。在该系统中，智能体必须使用基于一阶逻辑的可满足性模理论（SMT）求解器，将其动作意图自动形式化为数学约束，从而严格推导出预定义安全公理集的合法性。最终，求解器确定性地输出不可满足（UNSAT）决策，在逻辑层面保证没有任何行为违反预定义公理。为了实验验证 ePCA 范式的有效性，本研究放弃了传统的静态测试，转而采用深入的、动态的多轮对抗案例研究。具体来说，我们通过两个代表性场景评估该架构：一个**多步骤金融转账**任务，通过重复试验验证系统对时间分割和无信息规则利用的一致性；一个**跨域数据窃取**模拟，展示了我们的框架如何在真实的企业沙盒中逻辑死锁智能体的12轮渗透尝试。实证结果在两个场景中都清晰地验证了我们框架的有效性。在多步骤金融转账任务中，该机制在最先进的模型上实现了零攻击成功率和零误报率。此外，核心形式化计算的平均延迟被压缩到低至 0.44 毫秒，证明了其在高并发生产环境中的工程可行性。此外，在跨域数据窃取沙盒中，我们的系统不仅完全阻止了未经授权的操作，还导致智能体推理过程的强制终止。代数死锁迫使模型的推理主动终止，并明确承认对抗目标无法实现。这种从逻辑阻塞到诱导智能体推理过程逻辑终止的转变，为构建通用智能体的安全基础提供了实证支持。最后，作为智能体安全的开创性范式，我们审视了当前的局限性，并概述了未来的关键发展方向。

我们的核心创新体现在四个方面：

- **• 范式：** 我们引入了一种新颖的智能体系统安全视角，将基本防御范式从启发式、基于语义的概率性对齐转变为确定性的形式化约束。
- **• 框架：** 我们设计了可执行证明约束动作（ePCA）框架，这是一种创新架构，在执行接口处严格形式化并验证关键智能体操作，通过将不安全状态转换映射到可证明的逻辑死锁来强制安全。
- **• 系统：** 我们实现了一个功能完整的原型系统，并构建了一个动态的多轮对抗基准。实证评估表明，我们的系统在定义的操作边界内确定性地拦截了未经授权的智能体行为。
- **• 讨论：** 我们对所提出范式的适用性和理论局限性进行了广泛分析，并概述了未来在更好的悖论构建和意图提取方面的潜在方向。

## 2. 动机

随着智能体能力的不断提高，安全问题逐渐从传统的内容风险识别演变为复杂行为的系统级控制问题。现有依赖概率模型判断或启发式规则的防御机制主要基于同构语义监督：通过进一步的语言模型分析动作描述来推断意图的安全性。然而，这种范式在本质上受限于语义检测和逻辑决策之间的根本差异。只要智能体仍然以自然语言表达意图，就存在利用语义二义性或隐喻表达绕过护栏的方法。因此，安全的关键不在于用更好的语言模型分析语言，而在于创建智能体无法操纵或误解的不可绕过形式化约束。下一节将详细阐述这种形式化约束工程的方法论。