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

摘要

arXiv:2609.19391v1 Announce Type: new Abstract: LLM coding agents now generate complex programs at a scale that makes thorough human review increasingly difficult, raising the risk of safety and secur...

and safety programs the failures all guarantees MAGS 100 LLM

2026-09-18 1 阅读约1分钟阅读 Albert Wu, Nicholas Roberts, Tzu-Heng Huang, Haoran Lin, Gil Friedman, Sungjun Cho, Gabriel Orlanski, Frederic Sala

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

订阅66必读