MAGS：多智能体自动形式化确保智能体输出的安全性

# MAGS：多智能体自动形式化确保智能体输出的安全性
来源：https://arxiv.org/html/2609.19391
Albert Wu Nicholas Roberts Tzu\-Heng Huang Haoran Lin††通讯作者:[twu376@wisc\.edu](mailto:[email protected])\.†工作于威斯康星大学麦迪逊分校期间完成\.Gil Friedman Sungjun Cho Gabriel Orlanski Frederic Sala所属机构:威斯康星大学麦迪逊分校所属机构:普林斯顿大学

###### 摘要

大型语言模型（LLM）编码智能体现在能生成复杂的程序，其规模使得彻底的人工审查变得日益困难，从而增加了安全和安全漏洞的风险。常见的方法，包括模糊测试、静态分析和LLM作为验证器，能检测到许多故障，但难以覆盖所有可能的边缘情况。形式化验证通过提供针对指定属性的机器可检查保证来解决这个问题，但传统上需要大量的手动规范和证明工程。我们引入了一个统一的多智能体框架MAGS，该框架生成具有形式化安全保证的可执行程序，使用Dafny作为验证感知的中间表示，其中安全属性可以通过机械方式检查。MAGS形式化并冻结经过人工审查的API和安全要求，将生成的代码翻译成Dafny，使用验证器反馈修复违规，并将已验证的程序编译回可执行代码。我们在100个CUDA内核、100个终端脚本和20个机械臂任务上评估了MAGS。在全部220个示例中，它在生成针对冻结规范具有非平凡安全保证的程序方面实现了100%的成功率。独立的安全性和功能性评估进一步显示在所有三个领域都具有强大的性能，同时揭示了当自动形式化语义未能完全捕捉目标行为时会发生失败。

## 1 引言

LLM编码智能体现在负责编写日益增多的生产软件，但默认情况下，生成的代码没有安全或正确性的保证。依赖AI编码助手的开发人员报告说，验证和纠正生成的输出，而不是编写它，已成为他们工作努力集中的地方（Liang等人，2024年）。与此同时，推理成本在两年内下降了大约两个数量级（Xiao等人，2025年），因此在给定预算内可以生成的未验证代码量远大于这些漏洞率首次被测量时的情况。一个生成的函数可能通过测试套件中的每个测试，但仍然在套件从未执行过的输入上违反安全或安全属性。由于智能体也被用于单元测试生成（Zhang等人，2026年），开发过程中遗漏的边缘情况也可能通过传统测试无法被发现。因此，为了节省开发人员的时间并确保更安全的代码，健全的保证是必要的。我们研究的是在异构目标领域中生成具有机器可检查安全保证的可执行代码的问题，而无需人类手动形式化和证明每个生成的程序。

这样的保证并非随着LLM能力的提升而自然获得。先前的工作表明，被判断为功能正确的程序仍可能包含可被利用或不安全的行为，并且通过功能测试提供的安全证据有限（Vero等人，2025年；Nie等人，2025年）。测试和模糊测试可以暴露故障，但无法保证其不存在。形式化方法原则上可以填补这一空白：演绎程序验证提供机器可检查的证明，证明程序在所有建模输入上都满足其规范，而不仅仅是在测试套件恰好执行的那些输入上。然而，历史上，这需要大量的手动规范和证明工程。最近将LLM应用于验证已使这一成本大大降低（Yang等人，2025年；Sun等人，2024年；Loughridge等人，2025年），但现有方法通常在单一验证设置内运行，并未提供从生成的代码到跨现代编码智能体所针对的多样化领域的已验证可执行程序的统一路径。

我们引入了MAGS，一个统一的多智能体框架，通过验证感知的中间语言来生成具有机器可检查安全保证的代码。关键思想是将程序执行的语言与其安全性被证明的语言分离。MAGS使用Dafny作为共享表示，程序、API和特定领域的安全策略都在其中表达并进行形式化检查，尽管该框架可以与其他类似的验证语言一起工作。形式化是每个领域的成本，只需支付一次：对于每个领域，该框架在人工审查下自动形式化相关的库、API和安全要求，然后生成的核心规范被冻结。之后，该领域的每个任务无需进一步的人工输入即可运行。该框架将生成的代码嵌入Dafny，注入冻结的规范，通过Dafny的Boogie编码到Z3 SMT求解器来消除证明义务（Leino，2010年；Barnett等人，2006年），并在验证器反馈下修复违规。已验证的程序随后被编译回目标语言，并通过确定性的符号映射连接到相应的实际API。

我们在100个CUDA内核、100个终端程序和20个机器人控制任务上评估了MAGS。两个独立的预言机提供了对自动形式化语义和生成的安全证书的深入评估：特定领域的安全检查（CUDA compute-sanitizer、SecCodePLT安全测试用例、以及MuJoCo引擎中的碰撞和越界指标），这揭示了我们的语义未能捕捉的安全属性；以及在验证前后运行的保留功能测试套件，这揭示了通过过度限制程序行为而获得的空洞保证。

我们做出以下贡献：

贡献•具有自动形式化安全规范的实用跨领域生成：一个多智能体框架，从特定领域的人工编写的逻辑抽象到已验证的功能输出。通过在中间表示而非目标语言上进行验证，同一框架适用于CUDA、终端程序和机器人。•安全性、功能性和验证开销的评估：我们通过测试生成的程序是否满足冻结的规范、保留预期功能并通过独立的特定领域安全检查，来评估自动形式化语义的质量和覆盖范围，同时刻画验证器指导生成的成本。•LLM辅助验证的设计决策：我们报告了关于可扩展性和严谨性的选择——分离代码编辑和规范编辑智能体、冻结核心规范、以及在符号与实际API直接对应的语义嵌入上进行验证——并提供了支持每个选择的证据，包括它们不足之处。

## 2 相关工作

迭代修复。Self-Refine建立了模型在不进行额外训练的情况下批评和修改自身输出的模式（Madaan等人，2023年），Self-Debugging通过将执行跟踪反馈给生成器，将其专门化用于代码（Chen等人，2024年）。两项结果限制了该方法：模型在唯一反馈是自身判断时并不能可靠地改进（Huang等人，2024年），并且它们只有在被告知错误所在后才能修复错误（Tyen等人，2024年）。这两种失败模式都源于有一个有缺陷的预言机；通过单元和模糊测试并不能保证正确性。先前的工作同样表明，功能正确性提供的安全证据很少：在BaxBench上，针对大约一半原本被判断为功能正确的程序，端到端的攻击取得了成功（Vero等人，2025年），在SecCodePLT中也观察到了类似的模式（Nie等人，2025年）。MAGS保留了迭代修复循环，但用演绎验证器反馈替代了基于启发式或测试的反馈，该反馈识别违反明确的安全规范的情况。

演绎验证。形式化方法原则上可以填补这一空白：演绎程序验证提供机器可检查的证明，证明程序在所有输入上都满足其规范，而不仅仅是在测试套件恰好执行的那些输入上。然而，历史上，这曾是代价高昂的。seL4微内核需要大约200,000行的Isabelle证明来对应8,700行的C代码，以及大约20人年的工作量（Klein等人，2009年）。Dafny在源语言中允许前置条件、后置条件和循环不变量，并通过Boogie将其交付给SMT求解器进行消除（Leino，2010年；Barnett等人，2006年）；Why3将验证器的前端与其求解器后端解耦（Filliâtre和Paskevich，2013年）。最近将LLM应用于验证已使这一成本大大降低：AutoVerus在Verus错误反馈下修复Rust证明（Yang等人，2025年）；DafnyBench在恢复被剥离的注释方面对模型进行评分（Loughridge等人，2025年）；Clover检查代码、规范和证明之间的一致性（Sun等人，2024年）。要达到智能体编写代码的领域意味着一次一个领域——GPUVerify通过将内核简化为在两个任意线程上的顺序程序来证明CUDA和OpenCL无竞态条件和无发散（Betts等人，2012年），但仅适用于手工提供不变式的人工编写的内核。在这条线索中，形式语义是从系统外部为每个程序提供的，并且验证语言就是程序必须已经用其编写的语言。MAGS相反，从一个小的人工编写的逻辑基础和安全规范开始，自动形式化每个领域API对共享抽象状态的影响，在人工审查下冻结这些语义，并通过语义嵌入来验证生成的程序，因此目标语言和验证语言无需相同。

多智能体编排。VeriGuard离线合成行为策略，根据陈述的约束对其进行验证，并在线将其作为监视器运行，以筛选智能体提出的每个行动（Miculicich等人，2026年）；保证附加在策略上，因此只要未验证的代码的行动通过了监视器，它仍然可以执行。更接近我们的是，AutoVerus在Verus错误反馈下修复Rust证明注释，其中代码和规范作为输入是固定的（Yang等人，2025年）；ProofWright将智能体注释修复与VerCors和Rocq结合，为74%的KernelBench Level-1内核验证了安全属性（Chatterjee等人，2025年；Ouyang等人，2025年）。两者都局限于单一目标语言，都始于一个已经编写的程序，并且都终止于消除的证明义务而非可执行制品；两者都未报告控制可扩展性和验证严谨性的设计选择。MAGS相反，将安全策略贯穿到一个已验证的程序中，在一个跨三个领域的共享表示中重复使用。

## 3 MAGS：多智能体自动形式化保证安全框架

我们的目标是生成具有机器可检查安全保证的可执行程序，而无需人类手动形式化每个程序。MAGS通过两个阶段实现这一点：语义构建和程序验证。我们首先构建和冻结可重用的领域语义，然后根据这些规范翻译、修复和验证程序。这种分离防止证明生成智能体削弱安全定义，以使特定的基准实例更容易验证。本节逐步介绍每个阶段；图1和图2给出了完整流程的概述。

### 3.1 多智能体语义生成

在验证单个程序之前，MAGS构建可重用的语义，定义一个领域中程序被允许做什么。图1显示了这个语义构建流程。生成的语义定义了在整个验证过程中使用的抽象程序状态、API行为和安全属性。构建始于一个小的人工编写的逻辑基础，智能体用API语义扩展它，然后在任何验证之前进行审查、测试和冻结。

图注：MAGS中的语义构建。人工定义的核心逻辑由智能体生成的API语义扩展，由批评者和人工审查，并使用独立生成的安全和不安全探针进行评估。#### 核心逻辑基础。

每个领域都始于一个小的人工编写的逻辑基础，定义其抽象状态和推理原语。对于CUDA，我们使用基于分数权限的分离逻辑（Bornat等人，2005年）：完全权限允许独占写，而分数权限允许共享读。该基础还定义了要执行的顶层安全属性，包括无越界访问、无竞态条件和无屏障发散。一旦确定，基础就被冻结。

#### 自动形式化。

LLM智能体从官方文档中推导出API语义来扩展核心逻辑。批评者检查每个规范是否忠实、一致和模块化，同时保留源级API结构以提高可读性、求解器效率和错误定位。

我们随机审计了20%的生成语义，检查结构错误、过强的前置条件、未检查的安全条件、过度简化的规范以及偏离核心逻辑的情况。每个语义库也使用三个安全和三个不安全的探针程序进行测试，这些探针程序独立于语义生成。在库用于程序验证之前，所有安全探针必须验证通过，所有不安全探针必须被拒绝。

### 3.2 多智能体证明生成

一旦领域语义被冻结，MAGS就针对它们验证单个程序。图2显示了此流程。智能体被沙箱隔离于基准测试，仅针对形式化规范操作。该系统在必要时扩展语义，将程序翻译成Dafny，规划和执行证明策略，在需要时修复代码，并将已验证的结果编译回可执行形式。仅在之后运行保留测试以评估规范覆盖范围和预期功能的保留情况。

图注：程序验证