AI让给代码写证明更快了,但要证明什么只有你知道

可你没喂过前面带一万个空格的输入，没喂过恰好让中间某一步溢出的那个值。这些你根本喂不完。输入是无限的，用例是有限的，这是测试的死结。

而形式化验证呢，不喂数据，它把你的程序当成一个数学对象，然后推理会不会出问题。

第一步，它要你先写一句话，比如，对任何输入，这个函数要么返回一个在范围内的整数，要么返回错误，绝不产生未定义行为。这句话叫要求，也叫规格。你得用精确的语言写，不能有歧义，不能出现"大概""通常"这种模糊不清的描述。

第二步，你写一份推导，说明你的代码在所有情况下都满足这句话。

第三步，把推导交给一个检查程序。这个程序只做一件事，一步一步核你的推理，每一步都得符合规则。有一步走不通，整个逻辑都作废。就算你写对九十九步，第一百步错一个符号，前面的九十九步都不算。

就这么三件事：写要求、写证明、让机器核。

看起来是不是好像很简单，其实只是说起来简单，做起来一点都不简单。这些证明的代码，动不动就是几十万行。

人写证明，最爱说"显然""易证""同理可得"。这些在形式化验证面前，都不行。你得指出用了哪条规则、在哪一步、代入了什么。人写证明时省略的所有跳跃，在这里都得一步一步的全部写出来。

所以这样一份证明，写起来很细，读起来很笨，不跟你讲道理，只把每一步摊开。这就是形式化验证。

02

谁来检查检查器

前面提到的检查器，是整个验证的核心，几十万行的东西，交给一个程序去核。但是，问题马上就来了。

要是这个检查程序要是错了呢？你那些证明就是一堆废纸。你用一个程序检查另一个程序，谁又来检查它？

长期以来，这个问题的答案，简单得有点粗暴，把检查程序做到极小，小到不太会出问题。

所以，证明工具分为两层。外面那层很庞大，几十万行，负责理解人写的东西、提供便利、自动补一些显然的步骤。但不管外面怎么折腾，最后都要落到最里面那个内核上。内核只认一套极简的规则，它说通过才算通过。

举个例子，著名的形式化验证编程工具Lean，内核就几千行，最新的Lean 4 内核约 5000 行 C++。这几千行，一个人花几天就能读完，能确认它没在背后做手脚。

这条规矩还有一个专门的名字，叫德布鲁因判据。1967年，一个叫德布鲁因荷兰人，做了第一个能检查数学证明的程序Automath。德布鲁因判据不是工程上的优化建议，本质上是回答"信任从哪来"的问题，信任不会凭空产生，它只能停在某个小到人能亲自核对的东西上。

一整套验证系统里，最要紧的其实就是那个最小的部件，小到人能控制。几十万行证明可以外包，可以自动生成，也可以没人读完。但那个几千行的内核不行，得有人真的读懂，敢签字画押。

03

证明成立，是有前提的

一个程序有没有问题，不靠抽检验证，靠系统化的证明。这技术听起来是不是挺硬。不过，别高兴太早，理想很丰满，现实可能会很骨感。

我们再回头看看之前的那个例子。对任何输入，要么返回整数，要么返回错误。它成立是有前提的，编译器没把代码编错，芯片按规范执行指令，你依赖的那个库确实做了它承诺的事。

这些前提，一个都不在证明的范围里。

形式化验证给你的，不是说"这段代码是对的"，是"如果这些前提成立，那么这段代码符合你写的那句话"。

有没有发现点什么。前提是人写的，要求是人写的。机器，只负责执行，它没有额外做任何事，只是把你认为的证明过程，死板的写在代码里了。

04

贵有贵的道理，很多时候不用，不代表真的不用

一个验证程序，动辄就是几十万行，贵也是真贵。

但是意义咱们前面也说了，有用也是真有用。

对于一般的测试，当老板、客户问你的时候，你只能说“我测过了”。但当你做了形式化验证，你就会说"它不会错"。测试是抽样，证明是全称。所谓测试覆盖率百分之九十，真实含义是，还有百分之十的行为，你完全不知道会发生什么。

正是这百分之十，很可能抓到人根本想不到的问题。有些 bug 要极端的输入、极端的内存状态才现形，人眼看不见，随机测试也撞不上。Anthropic 这次找到的 bug 里，有一个只有在输入接近二十兆、而且布局极其特殊的时候才会触发。这种输入，模糊测试跑几年也未必撞得到。而证明不用撞，它是把情况全铺开了来看。

另外，这种验证，还能把责任分开。一旦真出了事，能分清是代码写错了，还是要求提错了。这两件事的后果完全不同，但在只有测试的系统里，它们永远是糊在一起的。

所以，在哪些错一次就完蛋的地方，比如飞控、内核、加密库，就算再贵，也得用，不只是找到问题，也是分清自己的职责。

05

一个“最快”，怎么翻译成数学

首先，你得先写一句精确的话。比如，对任意出发时间、任意路况，这条路线到达的时间，不大于任何其他合法路线。

写出来，问题就来了。"合法"指什么？不能逆行、不能闯红灯，那临时交通管制算不算？"所需时间"包不包括等红灯？"任何其他路线"，一个城市里可能的路径是天文数字，你怎么把这个集合说清楚？

而且，每回答一个问题，你都得做一个产品决策。这些决策，可能没有一条是从"最快"这两个字里推出来的。

到最后，就算证明完美通过，但是产品可能彻底错了，这就是一个非常尴尬的问题。你证了这条路线在所有合法路线里最快，可用户对“最快”的理解可能是"最省心"，是少变道、少走小路、少被拍。要求里没写，证明就不管。

它不知道你想要什么，只知道你写了什么。

除了要求，前提它也管不着。它只在前提和要求成立的时候成立。而且价格它也解决不了，就是贵。

今天，看起来Anthropic用AI把价格打下来了，但是要求和前提是性质问题，这个变不了，这个我们得分开看。

06

省下的是证明的钱

因为AI，现在可以直接证编译之后的机器码，不用把整份代码改写成另一种语言。以前也能证到机器码，但那是一个团队、几年时间、一个特定系统。现在它变成了流水线，拿个现成的开源库，编译，扔给模型，几周后就能得到一份证明，成本显著降低。

便宜是有边界的，你省下了写证明的钱，但花出去的是挖地基的钱。你每往下推一层前提，成本不是线性涨，是跳着涨的。

更要紧的是，"编译器会不会编错"这条前提确实被划掉了，但前提并没消失，只是换了个地方。

过去，前提是"你的代码之外的一切"，模糊、庞大、你也管不了。现在AI能把这些理清楚，还能缩小到关键的范围，这是真进步。但是范围是小了，可你要相信的东西，一样没少。

这次Anthropic没写新要求，只是把现成的测试用例翻译成了要求。

测试用例是什么？是一群人当年觉得这里得测一下，然后就写下来了。翻译成要求，其实等于承认，我们要证的，还是当年那批人想测的东西。

能证的范围，还是哪些，只是从跑一跑看看变成了可以被机器证明。

而要求这东西，恰恰是最难的，这是深刻的产品判断。技术判断可以外包，但产品判断不行。它决定你证什么，也决定你不证什么。这件事 AI 代替不了，因为它不知道你想要什么。

所以这次AI是把证明的成本打下来了，解决了证不证得起的问题，证明不再是少数公司少数关键能力的专属。可该证什么？这些前提和要求，还是得靠人。

08

冒出来的一个新问题

过去，每一个证明都是人写的，写的人知道自己证了什么。这次不是，AI给出的这一亿八千万行代码，我敢说，没人会去完整的看一遍。Anthropic 自己的说法是，几乎不需要人工审查，检查器会保证这份证明确实满足人提出的那份要求。

不过，这句话得分开看。理论上，模型完全可以让任何定理都成立，只要把程序改成一个永远不会崩的程序。所以，它保证了证明和要求都能对得上，但不是要求和你想要的对得上。

这种暴力解题的方式，和AI一如既往的逻辑一样，题目不会做，但不管怎么凑，总能把答案凑对。你让一个东西去证明一个程序不会崩，它最省事的办法，就是把程序改成不会崩的样子。

当然，Anthropic为了避免这样凑答案的问题，也给AI加了一个限制，不能打太多布丁，所有补丁记录在案，逐一审计。办法不复杂，但它也说明了一件事，现在你信的不再是写证明的人知道自己在证什么，信的是这套流程没让模型偷懒。

所以，要求由谁定，信任就会留在谁身上。而且，以前你至少读得懂证明，知道自己赌的是什么。现在读不懂了，只能赌流程靠不靠谱。

09

AI可以无限证明下去，问题是停在哪里

除了上面提到的信任的位置变了外，还有一个点，证明应该停在哪里。

还是上面的例子，你想证明自家水管不漏，可以证明到房子的管线布局，可以证明到房子的地基，甚至证明到周边的供水系统。

所有论证最后只有三种结局，一直往下沉，沉到无穷；二是绕回来，自己证自己；三是停在某个不再追问的地方。

形式化验证选了第三种。

它没法让你没有疑问，但能让你知道疑问停在哪儿。这一点挺难得的，大部分技术都在假装自己没有前提。

AI也没有改变这个结构，写证明、写代码、找反例，这些过去必须由人来的地方，现在能批量生产。但是决定在哪儿停，还是得有人来定，并且为这个停止负责。

而且停在哪里只是表象，背后其实是你想要什么。可以把证明、检查、写代码都外包给AI，唯独"想要什么"外包不出去。而且一旦外包，你验证的就是别人的意图，而且验证得越完美，很可能错得越彻底。

10

写在最后

就像前面说的，形式化验证，这技术听起来是挺硬，不过，理想很丰满，现实很骨感。

在AI的加持下，证明的确是变得更便宜了。不过，需要注意的是，就算不贵，你也只能证明你写得出的东西，相信你选定的东西。

技术能把“相信”的成本压到很低，但压不到零。

剩下那一份想要什么的前提和要求，还得我们自己签字画押。