💻 computer science

AI for software engineering: from probable to provable

该论文针对“氛围编程”面临的需求定义困难和幻觉问题，提出将人工智能的创造力与形式化规范及程序验证技术相结合，以实现从“概率性”到“可证明”的软件工程转变。

原作者： Bertrand Meyer

发布于 2026-04-24

📖 1 分钟阅读☕ 轻松阅读

原作者： Bertrand Meyer

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇文章由软件工程领域的泰斗 Bertrand Meyer 撰写，标题是《从“可能”到“可证明”：人工智能在软件工程中的角色》。

简单来说，这篇文章在讨论一个很火的话题：AI 会取代程序员吗？ 作者的答案是：不会直接取代，但如果想让它真正帮上大忙，必须给它套上“紧箍咒”——也就是数学逻辑和形式化验证。

为了让你轻松理解，我们可以把这篇文章的核心观点拆解成几个生动的比喻：

1. 历史的“既视感”：AI 不是第一个来“抢饭碗”的

文章开头提到，从 60 年代的 COBOL 语言到现在的“低代码/无代码”，每隔几年就会有人喊：“以后不需要程序员了，AI/工具会自动写代码！”

比喻：这就像每次有人发明了一种更高级的“自动炒菜机”，大家就喊“以后不需要厨师了”。结果呢？炒菜机确实能帮人切菜、调味，让做饭变快了，但没人能完全替代厨师。因为做饭不仅仅是把菜扔进锅里，还需要知道客人想吃什么（需求）、怎么搭配营养（设计）、以及确保菜没毒（测试）。
现状：现在的"AI 编程”（作者戏称为“氛围编程”Vibe coding）确实很酷，能帮你快速生成代码，但它还没能取代整个软件工程。

2. 最大的两个拦路虎：提需求太难，AI 爱“胡扯”

作者指出，想用 AI 写代码，面临两个巨大困难：

困难一：提需求比写代码还难。
- 比喻：很多人以为只要对 AI 说“我要一个像微信一样的软件”，AI 就能变出来。这就像你对厨师说“我要一顿好吃的”，厨师却问你“具体是什么口味？辣的还是甜的？几个人吃？”。把模糊的想法变成精确的指令（提示词工程），本身就是最难的工作之一，甚至比写代码本身还难。
困难二：AI 的“幻觉”（Hallucination）。
- 比喻：现在的 AI 就像一个博学但有点自负、爱吹牛的大学生。它读过很多书，说话很流利，态度也很诚恳，但它并不懂逻辑。它给出的答案通常是“看起来最像对的”，而不是“绝对对的”。
- 后果：在翻译或看图时，AI 偶尔错一点没关系（比如把“猫”翻译成“狗”，人类能看出来）。但在写代码时，如果 AI 编造了一个不存在的函数，或者逻辑有细微漏洞，整个程序就会崩溃，甚至引发安全灾难。

3. 软件的特殊性：要么完美，要么垃圾

这是文章最核心的观点。

比喻：
- 医疗 AI：如果 AI 看 X 光片，100 次里有 99 次看对了，1 次看错了，它依然是个伟大的工具，因为它比人眼快，且错误率更低。
- 软件代码：软件是非黑即白的。一个程序要么能跑（有用），要么就是垃圾（没用）。你不可能说“这个软件 99% 是对的，剩下 1% 是错的，大家凑合用吧”。如果核心功能有个小 bug，整个系统就废了。
数学陷阱：软件是由成千上万个模块组成的。如果每个模块有 99.9% 的概率是对的，那么 1000 个模块连在一起，整个系统完全正确的概率就只剩下 37% 了。如果 AI 只是“大概率”正确，那么拼起来的系统几乎注定是错的。

4. 解决方案：给 AI 配一个“数学警察”

作者认为，AI 和软件工程要想“幸福地生活在一起”，不能只靠 AI 的“创造力”，必须引入形式化验证（Formal Verification）。

比喻：
- AI 是那个充满创意、天马行空的“嬉皮士”画家，它画出的草图很美，但可能透视不对，或者颜色搭配不符合物理定律。
- 形式化验证 是那个严肃、一丝不苟的“数学警察”。它不关心画得美不美，只关心逻辑是否严密。
- 合作模式：AI 负责画草图（生成代码和初步需求），数学警察负责拿着尺子和圆规去检查（形式化验证）。只有当警察说“这完全符合几何公理”时，这幅画（软件）才能挂出来。
具体做法：
1. 用数学语言精确描述你想要什么（形式化规范）。
2. 让 AI 生成代码。
3. 用计算机工具（证明器）去数学证明这段代码是否严格符合你的描述。
4. 如果证明通过，那就是100% 确定的；如果没通过，就修改，直到通过。

5. 未来的工作流：从“氛围编程”到“契约编程”

作者提出了一个未来的工作场景：

过去：我们靠“氛围编程”（Vibe coding），凭感觉让 AI 写代码，然后人工去试错、修 bug。
未来：我们要搞“契约编程”（Vibe-contracting）。
- 人类和 AI 一起写“契约”（精确的数学规则）。
- AI 生成代码。
- 工具自动证明代码符合契约。
- 如果不符合，AI 自动修正，直到证明通过。

总结

这篇文章的核心思想是：不要指望 AI 能像变魔术一样直接变出完美的软件。

AI 确实很强大，但它本质上是基于概率的（猜得准不准），而软件工程要求的是确定性（必须是对的）。
唯一的出路，是把 AI 的“创造力”和数学逻辑的“严谨性”结合起来。让 AI 当“创意助手”，让数学工具当“质量守门员”。只有这样，我们才能从“大概能跑”的概率世界，走向“绝对正确”的可证明世界。

一句话总结：AI 可以帮你写代码，但只有加上数学证明的“紧箍咒”，它写出来的东西才敢真正用在关键的地方。

论文技术总结：AI 赋能软件工程：从“概率”到“可证明”

作者：Bertrand Meyer (苏黎世联邦理工学院)
来源：Communications of the ACM (预计 2025 年 8-10 月刊)

1. 研究背景与核心问题 (Problem)

本文针对当前备受推崇的"Vibe Coding"（即利用 AI 技术直接生成代码，仅需模糊提示）在软件工程领域面临的根本性挑战进行了批判性分析。作者指出，尽管 AI 在代码生成方面展现了惊人的能力，但要将其真正应用于专业软件工程，存在两个主要障碍：

需求定义的困难（提示工程即需求工程）：
- 向 AI 清晰描述“需要什么”（Prompt Engineering）本质上等同于需求工程（Requirements Engineering, RE），这是软件工程中最具挑战性的领域之一。
- 传统的“足够好”的需求（允许模糊、依赖常识）在 AI 生成代码的场景下不再适用。因为 AI 会严格（但可能错误地）执行模糊的指令，导致生成的代码与真实意图偏差。
幻觉现象（Hallucination）与“恶魔案例”：
- 概率性本质：现代 AI（基于统计和概率的 LLM）生成的是“最可能”的答案，而非“逻辑正确”的答案。
- 幻觉循环（Hallucination Loop）：AI 生成的错误代码往往看起来非常可信（“恶魔案例”）。开发者在迭代过程中容易陷入 AI 的自信建议中，不断修正错误的方向，导致项目无法推进。
- 软件的特殊性：与医疗诊断或机器翻译不同，软件系统通常只有两种状态：能工作的和无用的。对于关键任务（A 类）和大多数商业软件（B 类），微小的错误可能导致系统完全失效，因此“统计上足够好”的答案在软件工程中是不可接受的。

2. 方法论与核心主张 (Methodology & Core Thesis)

作者提出，要实现 AI 与软件工程的成功融合，不能仅依赖 AI 的创造力，必须将其与**形式化规范（Formal Specification）和形式化程序验证（Formal Program Verification）**相结合。

核心论点：成功的解决方案是将 AI 的创造力与形式化方法的严谨性相结合，利用现代证明工具支持这一过程。
技术路径：
1. 形式化规范：使用数学语言（如 B、Alloy）或嵌入验证就绪编程语言（如 Eiffel、Dafny）中的“契约（Contracts）”来精确描述系统行为。
2. 自动验证：利用证明工具（如 AutoProof, Dafny Verifier, Boogie 引擎）对生成的代码进行静态分析，生成数学证明，确保代码严格符合规范。
3. 迭代开发流程：
  - 摒弃“一次性完美”的幻想，采用迭代过程：少量规范 + 少量实现 $\rightarrow$ 尝试验证 $\rightarrow$ 发现不满足的属性 $\rightarrow$ 修正规范或代码 $\rightarrow$ 重复。
  - 这类似于传统的调试（Debug），但将动态的“测试执行”转变为静态的“逻辑证明”。
4. AI 的双重角色：
  - 生成实现：辅助编写代码。
  - 生成规范：辅助编写形式化契约（如循环不变式、类不变式），解决人工编写这些注解困难的问题。

3. 关键贡献 (Key Contributions)

对"Vibe Coding"的批判性反思：
- 明确指出 AI 无法替代专业软件工程师，特别是在处理 A 类（关键任务）和 B 类（商业）软件时。
- 揭示了软件模块化带来的错误累积效应：即使每个模块有 99.9% 的正确率，在数千个模块的系统中，整体正确的概率也会趋近于零。概率性的 AI 无法保证大规模系统的可靠性。
提出"Vibe-Contracting"（振动契约）概念：
- 作为"Vibe Coding"的补充，主张利用生成式 AI 辅助生成形式化规范（契约）。
- 倡导一种“规范与实现同步开发”的新范式，利用人类洞察力结合 AI 能力，并通过证明工具在每一步检查一致性。
重新定义 AI 在软件工程中的定位：
- 将 AI 从“代码生成器”重新定位为“形式化验证流程中的辅助工具”。
- 强调形式化验证（Formal Verification）是解决 AI 幻觉问题、将软件从“概率正确”提升到“可证明正确”的必经之路。

4. 结果与现状 (Results & Current State)

现状评估：
- 形式化验证已在 A 类（高安全性）系统中有一定应用，但在学术界和工业界（特别是 B 类）尚未普及。
- 目前的 AI 工具（LLM）在生成代码时表现优异，但在处理复杂逻辑和避免幻觉方面存在本质缺陷。
- 现有的证明工具（如 AutoProof, Dafny）虽然强大，但使用门槛高，且难以处理大规模系统的自动验证。
实验观察：
- 在涉及 LLM 辅助编程的实验中，当 AI 提供看似合理但错误的建议时，开发者容易陷入“幻觉循环”，最终导致项目失败。
- 学生使用 LLM 生成代码后，往往无法理解或修改代码，表明缺乏对底层逻辑的掌握。

5. 意义与展望 (Significance)

理论意义：
- 打破了"AI 将取代程序员”的简单叙事，提出了 AI 与软件工程深度结合的复杂路径。
- 强调了数学逻辑和形式化方法在现代 AI 时代的重要性，认为这是解决 AI 不可靠性的唯一途径。
实践意义：
- 为构建高可靠性、大规模的商业软件系统提供了一条可行的技术路线：AI 生成 + 形式化验证。
- 指出了未来工具开发的方向：需要更强大的证明工具来降低形式化规范的门槛，同时利用 AI 辅助生成这些规范。
最终愿景：
- 通过结合 AI 的创造力（生成想法、代码、规范草案）和形式化方法的严谨性（数学证明、逻辑验证），实现从“概率性（Probable）”到“可证明（Provable）”的跨越。
- 作者呼吁避免 AI 与软件工程“离婚”，而是通过这种混合方法实现“幸福婚姻”，确保软件系统的正确性和安全性。

总结：Bertrand Meyer 认为，单纯依赖 AI 进行“提示即编程”是危险的，因为它无法解决软件对绝对正确性的要求。未来的软件工程必须走向**"AI 辅助的形式化验证”**，即利用 AI 生成代码和形式化契约，并利用数学证明工具确保其正确性，从而在保持创新速度的同时，确保系统的可靠性。