多智能体框架MAGS实现100%成功率，220个任务全部生成形式化安全保证程序！
MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs
📖 AI 总结
本文提出 MAGS，一个面向 LLM 编码智能体输出安全的多智能体自动形式化框架。针对模糊测试、静态分析和 LLM 验证器难以覆盖全部边界情况、而传统形式验证又依赖大量人工规约与证明工程的问题，MAGS 以 Dafny 作为可验证的中间表示，将经人工审核的 API 与安全需求形式化并冻结，把生成代码翻译为 Dafny，借助验证器反馈修复违规，再将通过验证的程序编译回可执行代码。作者在 100 个 CUDA 内核、100 个终端脚本和 20 个机械臂任务共 220 个样例上评估，全部成功产出针对冻结规约具有非平凡安全保证的程序，成功率达 100%；独立的安全性与功能性评估也显示三个领域均表现良好，同时暴露出当自动形式化语义未能完整刻画目标行为时会出现失败。该工作为智能体生成代码提供了机器可检验的安全保证路径。
🔑 关键词速览
| MAGS | 一种多智能体自动形式化框架，用于生成带有形式化安全保证的可执行程序。 |
| Dafny | 一种支持形式化验证的编程语言和验证器，用作验证感知的中间表示。 |
| 形式化验证 | 使用数学方法证明程序满足特定属性（如安全性）的技术。 |
| LLM编码智能体 | 基于大语言模型、能够自动生成或修改代码的智能体系统。 |
| 冻结规约 | 在验证过程中固定不变、经人工审计的安全需求或API规约。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅