资讯
MAGS：多 agent 自动形式化，为 agent 产出提供可机检安全保证
一句话：9 月 16 日 arXiv 论文 MAGS 提出统一多 agent 框架，生成带形式化安全保证的可执行程序：以 Dafny 作为可验证中间表示，冻结人工审计的 API 与安全需求，把生成代码翻译为 Dafny、用验证器反馈修复违规，再编译回可执行代码。
背景
- LLM 编码 agent 生成复杂程序使人工审查愈发困难，模糊测试、静态分析与 LLM-as-Verifier 难覆盖所有边界；形式验证提供机检保证，但传统上需大量手工规约与证明工程。
核心要点
- 提出 MAGS 统一多 agent 框架：冻结人工审计的 API 与安全需求，将生成代码翻译为 Dafny 验证感知中间表示。
- 用验证器反馈修复违规，再把已验证程序编译回可执行代码，实现「生成 + 形式化保证」闭环。
- 在 100 个 CUDA 核、100 个终端脚本、20 个机械臂任务共 220 个样例上，对冻结规约达成 100% 非平凡安全保证成功率。
- 独立安全与功能评估显示三域均强，但也揭示当自动形式化语义未完全捕获目标行为时会失败。
为什么重要
- 把形式化验证从「重手工」变为「agent 可自动化」，为编码 agent 的高风险产出提供可机检护栏。
- 冻结规约 + 自动修复，使安全保证可规模化应用于真实代码生成。
关键事实速记
- 论文：arXiv 2609.19391（2026-09-16）
- 框架：MAGS（多 agent 自动形式化）
- IR：Dafny 验证感知
- 成功率：220 例 100% 安全保证
📂 原文链接：查看原文 →
← 返回资讯列表
AI8899 · 内容仅供学习参考