Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering
本文介绍了 Forge，这是一个将模型驱动工程与形式化验证工具相结合的闭环流水线，旨在迭代地完善并认证由大语言模型生成的、针对安全关键系统的“氛围编码”（vibe coded）Java 软件，且无需开发人员手动检查形式化模型。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正在雇佣一位速度极快、极具创意但有些粗心的建筑师（即 AI），为潜艇设计一套生命维持系统。你给出了一个简单的指令：“制造一台能保持氧气水平安全的机器。”
这位建筑师立即在餐巾纸上画出了蓝图。看起来很不错，甚至可能适用于玩具潜艇。但对于真正的潜艇来说，你不能只听信他们的蓝图。如果蓝图隐藏着缺陷，人们可能会丧命。这就是 “氛围编程”（Vibe Coding） 的问题：仅仅基于随意的对话让 AI 编写代码，而不进行严格的检查。这种方式很快也很有趣，但对于涉及安全的关键领域（如飞机、汽车或医疗设备），风险太高，因为 AI 无法为代码提供完美的数学保证。
这篇论文介绍了一种名为 Forge 的解决方案。你可以把 Forge 想象成一个超级严格的质量控制工厂，它位于创意建筑师与最终产品之间。
以下是 Forge 工厂的工作步骤：
1. 草拟（“氛围”部分）
AI 使用 Java（一种现实世界工程师实际使用的语言）生成初始代码（蓝图）。AI 不需要掌握复杂的数学，它只需根据你的自然语言指令编写代码即可。
2. 翻译器（“模型驱动”部分）
这是一个神奇的技巧。Forge 工厂并不要求 AI 编写数学证明。相反，它获取 AI 的 Java 代码，并自动将其转化为三种不同的形式化语言（数学蓝图）。
- 这就像是将一张粗略的草图瞬间转化为三种不同类型的技术图表：一份给结构工程师，一份给电气工程师，一份给安全检查员。
- 开发人员无需阅读这些复杂的图表，工厂会自动完成转换。
3. 三位检查员（“验证”循环）
工厂将这三份数学图表发送给三位极其严苛的检查员（验证器）：
- 检查员 A (Dafny)： 检查每一个函数是否确实履行了它的承诺。这就像是在检查门锁在转动钥匙时是否真的锁上了。
- 检查员 B (FDR4)： 检查整个系统的“死锁”情况。它会询问：“如果系统陷入了某种特定状态，它还能出来吗？”它确保机器永远不会卡死。
- 检查员 C (Isabelle)： 总检查员。它观察整个逻辑结构，以证明该系统在数学上不可能以特定方式崩溃。
4. 反馈循环（“修正”部分）
如果三位检查员中的任何一位发现了缺陷，他们不会只说“失败”。他们会向 AI 发送一份结构化的笔记。
- 示例： “检查员 B 发现，如果机器人在转向时检测到障碍物，它将无法停止。请在转向模式中添加一个‘停止’指令。”
- AI 阅读这条笔记，修复代码，然后将代码再次送回工厂。
- 这个循环会自动重复。AI 会不断完善代码，直到通过所有三位检查员的检验。
结果：这有效吗？
作者在三个真实的机器人场景（地面机器人、水下航行器安全系统和化学检测机器人）中测试了这一点。
- 没有工厂： 如果他们只是让 AI 写一次代码并进行检查，它从未通过。AI 在 100% 的尝试中都犯了错误。
- 有了工厂： 当他们使用这个循环时，每一次尝试最终都通过了所有三项检查。通常只需要 2 到 3 轮修复。
为什么这很重要？
论文认为，我们不应该强迫 AI 去学习复杂的数学语言（因为它在训练中见到的这类语言不够多，所以表现很差），而应该让 AI 做它擅长的事（编写标准代码），并利用我们现有的、经过验证的工程工具（即这个工厂）来检查和修正其工作成果。
简而言之： Forge 将 AI 从一个“变数”转变为一名可靠的绘图员。AI 编写初稿，而工厂的自动化数学检查器充当编辑，强制 AI 重写代码，直到它在数学上达到完美。这为那些失败代价无法承受的领域（如航空、医疗等）提供了认证 AI 生成软件的路径。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。