将智能体指令自动形式化为 Policy-as-Code

# 代理指令的自动形式化为策略即代码

来源：https://arxiv.org/html/2606.26649

###### 摘要

在高风险领域中，代理安全需要正式的策略执行，但现有方法要么依赖概率性护栏（微调分类器、基于提示的引导）而无法提供正式保证，要么依赖手动编码的符号执行而无法扩展到真实策略规范的广度。我们提出了一种自动形式化流水线，利用基于LLM的生成器-评判器循环，将代理提示、MCP工具描述和自然语言策略文档翻译为经过正式验证的策略。生成的策略使用Cedar策略语言编写。在MedAgentBench基准测试中，我们的自动形式化策略覆盖了比先前工作中手动编码的符号执行多得多的源自然语言规范。

自动形式化、策略即代码、Cedar、代理安全

{NoHyper}

## 1 引言

参见图1：策略生成流水线。系统提示、MCP工具定义和（非结构化的）策略语料库通过生成器-评判器循环自动形式化为一组经过验证的Cedar策略，该循环将硬性、确定性的评判器（Cedar解析器检查语法、架构不匹配、矛盾和空策略）与软性评判器（作为评判者的LLM进行语义对齐和基于评分标准的定性评估）配对。如果策略通过两个评判器，则生成器-评判器循环结束。生成的策略集在运行时由外部策略引擎执行。

大型语言模型（LLM）已从被动的文本生成器演变为能够感知环境、规划多步轨迹、并通过LangGraph或Amazon Strands等框架操作外部工具的自主代理。然而，AI代理在安全性与实用性之间存在强烈权衡：为了让代理自主完成复杂任务，它们通常需要提升的权限，而提升的权限意味着更高的攻击面。赋予AI代理提升的权限尤其危险，因为基于LLM的代理容易受到提示注入等对抗性技术的影响。当前保障代理行为的行业实践主要依赖微调的安全模型（如Llama Guard（Inan等，2023））或基于提示的引导，通过系统指令来指导行为。然而，基于分类器和提示的护栏往往无法满足安全关键型应用的需求，因为它们无法提供正式保证。在本文中，我们描述了一种替代性的护栏方法，即使用自动形式化和策略即代码（PaC），这为代理行为提供了强有力的保证。我们的系统通过一个外部的确定性策略引擎来管理代理行为，该引擎根据正式规则评估代理行为，以决定这些行为是否被允许。

### 1.1 贡献

我们提出了一种分层自动形式化架构，称为**验证三明治**，用于将自然语言代理指令翻译为正式策略语言。在运行时，这些正式策略通过代理封装器强制执行，以管控代理的行为。为了评估我们的方法，我们引入了一个开源的策略封装器，用于使用Cedar策略语言（Cutler等，2024）实现的代理框架，并公开发布了此实现以及定制的Python版Cedar语言绑定。¹¹¹https://github.com/sondera-ai/sondera-harness-python

该架构的核心是一个策略生成流水线，它自动将代理卡（包含指令和工具架构）转换为经过验证的授权策略。这项工作借鉴了LLM Modulo框架（Kambhampati等，2024）和神经符号AI的思想。

1.  1.**基础层**（底层）作为约束候选生成的基础。它提取实体，识别工具架构（例如OpenAI JSON架构），并定义主体-资源-行为本体。此层确保代理在结构化环境中运行，其中每个潜在行为都映射到现实世界实体和有效的系统标识符。
2.  2.**模型层**（中间层）利用最先进模型的生成能力对输入进行推理并生成候选策略。它利用其参数化知识来解释指令并提出反映预期代理逻辑的候选策略。
3.  3.**安全层**（顶层）对候选策略应用硬性（程序化、可确定性验证的）评判器和软性（基于LLM的）评判器。硬性评判器可以使用Cedar内置的静态分析工具检查语法错误或空策略等问题。软性评判器可以检查与原始自然语言表述的语义对齐度，以及评分标准中定义的其他定性问题。

### 1.2 先前工作

#### 1.2.1 自动形式化

自动形式化是指将非正式的自然语言翻译成可由机器推理处理的、可验证的正式陈述的过程。长期以来，人们一直对使用数学表达式对计算机行为进行建模感兴趣（Baier & Katoen，2008）。先前的数学研究集中使用LEAN（de Moura & Ullrich，2021）等正式语言来推理机器输出的正确性。不幸的是，这些函数式编程语言在每次描述时都需要冗长的规范级别，使其使用起来很繁琐。LLM的最新进展使得自动化这种翻译变得可行，降低了历史上限制形式化方法采用的规范负担。与我们用途特别相关的是，自动形式化能够数学性地验证非确定性的LLM生成输出（Weng等，2025）。

#### 1.2.2 上下文感知代理策略

随着AI代理具备在循环中自主控制和调用工具的能力，定义上下文感知策略来管理其行为的需求应运而生（Tsai & Bagdasarian，2025）。先前的研究探索了使用上下文决策策略来修改AI模型行为（Seraj等，2025）。其他作者探索了从这些策略生成运行时护栏（Kholkar & Ahuja，2025）或通过挖掘代理轨迹来学习策略（Abaev等，2026）。

#### 1.2.3 Cedar策略语言

为了实施这些类型的代理策略，策略语言提供了多种有吸引力的特性，包括人类可读的语言（Amazon Web Services，2025）和策略、通过定理证明器提供的逻辑正确性保证、用于捕获语法和表达式错误的验证，以及编译后的速度。我们对现有策略语言进行了评估，本研究选择了Amazon Web Services开源的Cedar授权语言（Cutler等，2024）。Cedar虽然性能高效，但也易于非领域专家阅读和编写（Kaoudis & Smith，2024）。

## 2 方法

我们应用自动形式化，将系统指令、MCP工具定义和自然语言策略文档中的自然语言意图转换为用Cedar策略语言编写的正式策略即代码。这些策略随后用于控制运行时代理行为。自动形式化过程的流水线如图1所示。

Cedar语言允许可选地强制使用架构，我们发现这对于检查自动生成的策略很有用。我们通过编程方式从MCP工具定义生成此架构。然后，我们将Cedar架构与代理系统提示、工具定义和策略文档一起提供给生成器-评判器循环（图1）。生成器-评判器循环首先使用LLM生成一组候选策略，然后由硬性评判器和软性评判器进行检查：

1.  1.**硬性评判器**：此组件对Cedar策略语法执行严格的、确定性的检查，强制架构合规性，并检查逻辑矛盾（即由于策略冲突而永远无法满足的策略集）。
2.  2.**软性评判器**：作为评判者LLM，软性评判器根据预定义的评分标准评估策略的语义对齐度。它确保正式逻辑准确反映原始指令和策略文档的精神。

软性和硬性评判器的反馈被提供给策略生成器，此生成器-评判器循环迭代进行以优化候选策略。一旦策略集达到硬性评判器步骤中确定的某个质量阈值，最终Cedar策略集即被输出。这些阶段共同实例化了**验证三明治**：基础层生成Cedar架构，模型层是策略生成器，安全层是硬性-软性评判器对。

## 3 评估

我们根据Hong等人符号护栏工作（Hong等，2026）中的MedAgentBench实验来评估我们的方法。MedAgentBench（Jiang等，2025）是一个用于使用工具的电子病历（EMR）代理的能力基准测试，本身不包含安全策略。因此，Hong等人撰写了一份包含88条规则的合成自然语言策略（由GPT-5.2起草并通过STPA危险分析扩展），并为其中23条规则手工编写了符号护栏。我们将相同的策略输入我们的自动形式化流水线以生成Cedar策略，评估重点放在执行覆盖范围上，而非代理实用性。除了使用自然语言策略通过我们的自动形式化流水线生成Cedar规则外，我们还使用Claude Opus 4.7从Hong等人的参考MCP服务器（Hong等，2026）转录额外的快速医疗互操作性资源（FHIR）约束到Cedar规则中。这些额外规则无法仅从策略文本中推导出来，因此对于与Hong等人进行公平的正面比较是必需的。我们对每条Cedar规则标注了来源注释以标记其溯源，从而将规则分为两个桶（policy.md或MCP）。我们不编码特定的基准测试实例或数据特定常量，仅旨在与MCP实现的狭窄性达成对等。我们使用ETL流水线摄取并规范原始MedAgentBench数据集中的轨迹，以便通过我们的Cedar策略引擎重放它们进行评估。

**实验设置。** 这些实验中使用的自动形式化流水线实现如下。候选生成器是Gemini 3 Pro，提示中包含代理的系统指令、工具定义和自动生成的Cedar架构。硬性验证器调用Cedar参考工具（Rust `cedar-policy` CLI）进行语法和架构检查，并执行静态分析以标记空策略和冲突规则，在生成器反馈验证错误后最多重试三次。软性评判器是一个两阶段的评判器→验证器流水线（均为Gemini 2.5 Flash，温度分别为0.3和0.1）。我们的累积结果如表1所示。

测试了三种条件。在**原始**条件下，代理使用原始的HTTP GET/POST工具（MedAgentBench默认）。在**基线**条件下，每个HTTP端点被封装在类型化的MCP工具中。在**护栏**条件下，Hong等人的符号护栏被添加在基线之上。**对抗性**数据集将良性任务替换为旨在操纵代理违反策略的提示。

| 数据集 | 条件 | Hong等人不安全率↓ | Cedar拦截率↑ |
| :--- | :--- | :--- | :--- |
| 原始 | 原始 | 39.0% | 30.3% (91/300) |
| 原始 | 基线 | 23.0% | 57.7% (173/300) |
| 原始 | 护栏 | 0.0% | 55.7% (167/300) |
| 对抗性 | 原始 | 78.0% | 72.0% (36/50) |
| 对抗性 | 基线 | 62.0% | 82.0% (41/50) |
| 对抗性 | 护栏 | 0.0% | 85.7% (42/49) |

表1：MedAgentBench上的策略违反率

Cedar拦截率持续高于Hong等人的不安全率，因为我们的自动形式化流水线比Hong等人的手动实现覆盖了更多的策略。Hong等人为合成策略中88条规则中的23条手工编码了符号护栏；我们的流水线自动为这88条规则中的更多规则生成了Cedar策略。Hong等人的“不安全率”列统计了他们23条已实现规则的违反情况；Cedar拦截率统计了我们更广泛的自动形式化规则集的违反情况。护栏行的情况最为清晰：Hong等人的0%在其23条规则范围内是构造性的，而Cedar的55.7%（原始）和85.7%（对抗性）衡量的是剩余策略的违反情况。Cedar拦截率列中括号内的数字指的是轨迹：91/300意味着该分割中的300条轨迹中有91条被Cedar拦截。轨迹级别的拦截率低估了更强的底层结果。许多MedAgentBench任务仅涉及检索，从不发出写入操作（即从不发出POST请求）；由于Cedar可以拒绝工具调用但不能拒绝仅对话行为，因此没有写入尝试的轨迹在构造上是无法拦截的。按轨迹是否包含任何写入尝试进行分解：

| 数据集 | 条件 | 含POST的轨迹数 | Cedar拦截率 |
| :--- | :--- | :--- | :--- |
| 原始 | 原始 | 300 | 89 | 100.0% (89/89) |
| 原始 | 基线 | 300 | 84 | 94.0% (79/84) |
| 原始 | 护栏 | 300 | 86 | 98.8% (85/86) |
| 对抗性 | 原始 | 50 | 34 | 100.0% (34/34) |
| 对抗性 | 基线 | 50 | 33 | 100.0% (33/33) |
| 对抗性 | 护栏 | 49 | 32 | 100.0% (32/32) |

表2：按写入尝试分解的Cedar拦截率。Cedar拦截率的分母是至少有一个POST请求的轨迹数。

在对抗性护栏条件下，Cedar“遗漏”的七条轨迹均无POST写入尝试：其中五条由于代理在碰到护栏前内在拒绝而根本没有工具调用，另外两条则仅是通过GET请求进行检索。49条对抗性轨迹绕过了MCP服务器的硬门控，但Cedar额外的拒绝覆盖拦截了其中42条（85.7%；表1）。完整的Cedar策略可在附录的补充材料中找到。

## 4 讨论

**确定性安全 vs. LLM非确定性。** 此架构的稳健性源于将策略执行与LLM的推理上下文解耦。在传统的代理工作流中，安全指令通常嵌入系统提示中，或通过外部安全模型实现。我们的发现表明，通过将这些逻辑提取到Cedar策略中，我们降低了越狱和间接提示注入的风险。由于策略位于上下文窗口之外，并由确定性策略评估器强制执行，攻击者无法“说服”安全层忽略其规则。此外，故障关闭强制执行机制的实施确保