约束验证：独立于对齐的人工智能安全性保障
Containment Verification: AI Safety Guarantees Independent of Alignment
Royce Moon, Lav R. Varshney
arXiv (Cornell University) · 2026-05-09
开放获取对齐与安全大模型与语言检索增强与智能体影响因子 ≈0.2
摘要
智能体框架是人工智能代理在世界中开展活动的软件层。现有安全方法会对模型进行干预，因此仍依赖于无法验证的学习行为属性。我们提出了约束验证方法，将安全保障机制嵌入智能体框架本身。在混乱预言机语义下，人工智能被建模为对框架内类型化动作空间的无约束预言机，而经过验证的约束层必须对人工智能所能输出的每个类型化动作值执行边界策略。对于基于建模的边界事件、动作参数及状态所表述的可约束属性，我们通过前向模拟精化证明了其普遍适用性，并将其在Dafny语言中予以实现。我们以极简主义的智能体大语言模型框架PocketFlow为例进行验证，借助智能体合成流程，在防止规范冗余的信息屏障下生成了相关规范、运行模型及精化证明。据我们所知，这是对智能体框架的首次演绎式形式化验证。该保障机制独立于对齐过程，因为它针对的是框架的类型化动作边界而非模型行为。
本摘要由 AI（Hy-MT2-Pro）翻译生成，仅供参考，请以原文为准。
AI 综述
基于全文生成- 主要观点
- 论文针对智能体在高后果场景中直接作用于外部系统所带来的安全风险，提出containment verification范式，主张把安全保证的落点从模型侧移到中间层的智能体框架（即containment layer）本身，理由是既有对齐训练、机制可解释性、忠实思维链监控与对抗防御等方法均为oracle-level，统一条件依赖于无法形式验证的学习行为属性。其核心论断是：在havoc oracle semantics下把AI建模为对框架typed action space取值无约束的oracle，验证义务即归结为「containment layer对AI可能发出的每一个typed action value都执行boundary policy」，由此得到不依赖模型能力、训练过程与动作选择策略的universal guarantee。该保证只覆盖boundary-enforceable属性，即定义在modeled boundary events、action arguments与state上的谓词，不诉诸AI推理的自然语言语义；truthfulness、non-deception等内容层属性被明确排除在范围之外。作者以sleeper agents在标准安全训练后仍存活、chain-of-thought不忠实、对抗防御协议降低但未消除攻击成功率等经验反例，论证oracle-level方法的保证上界仅为empirical或distributional，并给出S(Empirical)⊆S(Distributional)⊆S(Universal)的强弱排序。论文以PocketFlow为见证实例，验证其dispatch loop相对于NoAction、ReadPathAction(path)、ToolCallAction(tool)、StepAction四变体动作接口，要求read事件仅限workspace root下路径、tool call仅限allowlist、step事件不超出loop bound，并自称这是首个对agentic framework的演绎形式验证。
- 研究方法
- 方法主体是演绎形式验证加定理证明与工具内机械化：把抽象边界安全规范建成labeled transition system TM，把具体containment layer建成TI，定义boundary-event refinement的三项条件（R1初始状态匹配、R2 step simulation、R3 safety preservation），据此证明Theorem 3.2（Containment Verification Soundness）及其Corollary 3.3（Deployed Boundary Safety）。机械化按IronFleet惯用法在Dafny中完成，用关系式转移谓词Next(c,v,v’,evt)取代确定性步函数，PocketFlow实例通过RefinementInit与RefinementNext两个refinement lemma放电，并由ContainmentVerificationSoundness组合TraceRefinesSpec、SpecSafetyAlongTrace、SpecSafetyLiftsToImpl三个引理。形式规范构件（TM、TI、ΠM、ΠI、R、Q）由一条七阶段agentic流水线合成，阶段为ContainmentSpec、InterfaceContract、GenerateSpec、ValidateSpec、Verify、ClassifyFailure、ProofRepair，其中GenerateSpec用Claude Sonnet 4.6做代码库探查、Claude Opus 4.7做规范与证明合成。流水线设有architectural information barrier以从结构上排除同义反复规范，并以resolution、vacuity、discrimination三道gate筛除空洞或无判别力的规范，ClassifyFailure把证明失败分类后回馈ProofRepair，再进入ValidateSpec，迭代至Dafny不动点。部署环节由Dafny编译器从已验证源码生成Python运行时，并在同时包含permitted与non-permitted动作值的动作序列上运行，以确认运行时只记录permitted事件、拒绝会产生out-of-policy boundary event的动作。
- 学术贡献
- 理论层面，论文把AI安全机制的locus从oracle-level改置到container-level，提出containment verification范式，并给出按adversarial scenario覆盖集排序的保证强弱层级（empirical ⊆ distributional ⊆ universal）与配套的soundness定理，明确oracle-level方法的上界为distributional、只有container-level的containment verification达到universal。方法层面，论文把抽象规范、操作模型、细化关系与不变量交给七阶段agentic合成流水线自动生成，并用信息屏障、三道validation gate与带分类的proof repair构成闭环，回应了Dalrymple等所指认的规范工程瓶颈。材料与实例层面，论文给出PocketFlow dispatch loop的端到端验证与可部署Python产物，将typed action space固定为四变体datatype Action，并把安全事件策略的三条状态不变量（read路径均为workspace rooted、tool call均在allowlist、step counter有界）作为该事件策略的推论在Dafny中放电。领域定位层面，论文以VeriGuard、AgentSpec、CaMeL为邻近但验证对象为AI周边工件（生成策略代码、运行时DSL监控器、信息流受控解释器）的对照工作，以BEAVER、C3LLM、Lumos为作用于LLM输出分布的概率界工作，并将containment verification与Bubblewrap、Firecracker、Docker、Podman等操作审计型sandbox区分，主张二者分层互补。论文还给出trusted base清单：ΠI、定义R与Q的抽象与事件关系、连接concrete event与部署外部效果的effect-faithfulness边界、Dafny验证器与编译器以及提供任意typed action的extern shim，而AI模型、prompting流程、训练过程与动作选择策略均不在信任基内。
- 存在局限
- 保证的有效性以effect exclusivity/effect-faithfulness为条件：凡是未经modeled event interface中介的部署外部效果，包括Python运行时、操作系统、sandbox、内核与硬件层缺陷（论文以潜伏近十年的Linux内核提权漏洞Copy Fail为例），均落在Theorem 3.2的量化范围之外，只能交由隔离机制处理。属性覆盖范围被明确限定为boundary-enforceable，论文承认truthfulness、non-deception等内容层属性不在范围内，且把ΠI未能捕捉意图安全策略的property-completeness gap仅列为三类潜在失败来源之一，未给出判定该gap是否存在的形式化判据或检验程序。实例化只落在PocketFlow这一极简框架的dispatch loop上，动作接口仅有NoAction、ReadPathAction、ToolCallAction、StepAction四个变体；论文在引言中列举LangChain、OpenAI Agents SDK、OpenClaw、Hermes Agent等生产框架，但材料中未提及在这些框架上的验证结果，跨框架、跨动作接口规模的可迁移性缺少证据。规范合成由LLM承担，其质量审计依赖三道gate与Dafny的证明义务，属于经验性把关；材料中未报告合成规范的数量、gate拒绝率、ProofRepair的迭代次数或任何量化评估，因而流水线的成功率与稳定性无法从材料中判断。部署验证仅在「包含permitted与non-permitted值的动作序列」上被exercise，材料未说明用例规模、覆盖判据，也未说明是否接入真实LLM agent进行端到端测试。
- 进一步研究方向
- 其一，把Theorem 3.2的实例化从PocketFlow推进到论文点名但未验证的LangChain、OpenAI Agents SDK、OpenClaw与Hermes Agent，对每个框架分别构造TM、TI、(ΠM,ΠI)、(R,Q)，并统计七阶段流水线在各框架上的Dafny放电成功率、ClassifyFailure的失败类别分布与ProofRepair迭代次数，用以检验框架规模与dispatch复杂度对规范合成成本的影响。其二，针对effect-faithfulness做运行时层面的实证：构造把部署侧外部效果（系统调用、网络出口、文件写入、数据库提交）与modeled boundary event接口逐一对齐的记录与检查机制，并用故意注入的内核级或运行时级绕过手段测量保证失效的触发条件与漏检比例。其三，对property-completeness gap给出形式化处理：定义ΠI相对意图边界策略的完备性判据，用针对边界策略的变异测试或反例搜索枚举ΠI未覆盖的策略空间，从而把该gap从失败来源清单提升为可度量的验证目标。其四，设计对照实验评估信息屏障与三道gate的实际效力：在同一Flow输入上比较启用与关闭information barrier时LLM生成规范的同义反复率、resolution与discrimination结果，检验屏障是否真正阻断了从实现反推规范的后验弱化。其五，开展containment verification与sandbox的分层联合评估：在Bubblewrap或Firecracker之上叠加已证containment layer，分别统计边界层拦截与下层隔离各自承担的失败案例数，以确定两层机制在真实攻击面上的分工边界。
本综述由 AI（deepseek-flash）阅读开放获取全文自动生成，仅供参考，不代表原文作者观点，请以原文为准。
参考文献
相关论文
话题：Formal Methods in Verification