DeepMind用AlphaProof Code验证Signal代码

太棒了，真是 AI 的一个绝佳用例。我感觉在大型科技公司中，Google 在有用贡献和对其 AI 系统的控制方面是最干净的。如果我没理解错的话，这个新的证明代理似乎并没有挑战规格说明（spec），只是挑战了实现。

我一直在想，也许人机交互的未来，本质上就是通过 LLM 这个“正门”，利用一套众所周知的形式化验证工具，这些工具可以组合使用（想想 UNIX 管道和重定向），并且能够即时编写和形式化验证新工具。就计算能力而言，我们还差得很远，但我怀疑我们的孙辈看我们人类程序员，就像我们看当年的计算尺使用者一样……

我预计很快，也许就在未来两三年内，我们会觉得在我们的系统上运行任何未经验证的软件简直是疯了，就像现在觉得我们曾经使用 Telnet 或明文 HTTP 一样疯狂。

今年早些时候，我在对一个旧项目进行重大重构。当时编码代理（coding agents）正迅速崛起，你可以越来越信任它们完成更自主的工作，所以我很兴奋想试一试。

它完成了重构，运行了好几个小时，最后还主动提供了一套广泛的测试用例。所有测试全部通过（全绿）！

我印象深刻，直到我仔细看了看。它把整个东西都反向实现了，这种方式不仅毫无意义（没有达成任何既定目标），而且让情况比之前更糟！

在那一刻之前，我对形式化验证在 AI 时代的潜力非常看好。但看到这一团糟后，我意识到，它就算为它写的代码写了一个数学证明，那个证明也会通过，但代码依然是错的！

我一直在尝试利用 AI 编写 Lean 代码的便捷性（https://metamagic.substack.com/p/beyond-the-proof-dump-lean-...），并总结了一些教训：

1. AI 生成的 Lean 并不完美，由于是 AI 自己在写 Lean，它很容易作弊。对于任何尝试 AI 生成 Lean 代码的人，至少需要另一个对抗性的提示（adversarial prompt）来审查 AI 生成的 Lean。

2. 在论文中我注意到，他们重新引入了一些 bug 来验证系统能否捕捉到，但他们似乎没有发现任何 bug。也许 Signal 本身就非常出色，经过了多双眼睛的审查，但对我们其他人来说，真正的故事是：如果你开始用 AI 将代码转换为 Lean，其价值在于它能发现哪些假设。即使对于我认为逻辑非常严密的东西，Lean 也发现了一些我不得不修复的小问题。这类似于模糊测试（fuzzing），每当我把模糊测试引入代码库时，从未不发现过 bug，我预计将规格说明转换为 Lean 也会有同样的效果。

3. 能够通过 AI（廉价地）生成 Lean 是一项非常有趣的解锁。从规格说明到 Lean 再到代码，利用 Lean 作为逻辑守门人，这种能力有望在日常生活中得到更广泛的应用，而不仅仅局限于研究。

太棒了。我记得去年我曾想，随着人们将更多工作交给 AI，软件可能会变得更充满 bug，但像这样的工具让我看到希望，也许软件的未来实际上会安全得多。

小白问题：除了这些加密系统，为通用软件构建这些证明有用吗？具体来说：

1. 有人将其应用于 AI 代理处于生产环境关键路径的软件系统吗？也就是说，可能会发生非确定性动作（尽管有恢复机制）的场景？

2. 在什么场景下从一开始就有 Lean 证明是合理的？比如，我想象如果你想构建一个对 ACID 有一定保证的数据库系统，那么从一开始就有这个可能会更好。但对于构建一个由 API 支持的服务来说，可能就没那么有用了。