我们现在拥有了自动化证明能力

长期以来，我始终对依赖类型语言情有独钟，比如 Coq、Rocq 和 Lean。这些语言提供了一种强大的类型系统，能够精确地刻画并强制执行那些极其微妙的不变式。

在传统编程语言中，这类不变式往往只能勉强被当作注释存在，随着团队规模的扩大，它们很快就会被遗忘，最终导致各种微妙的误解和彼此间难以契合的组件。

很多时候，这些组件已经发展到足够大的规模，以至于一旦发现问题，要将其中任何一个重新调整至正确状态，往往令人倍感疲惫。或许，借助依赖类型这种颇具吸引力的机制，我们完全可以将这些不变式以形式化的方式编写出来，并由机器来完成验证。

(附言：Coq 的名字已经改了！我记得多年前在普林斯顿参加一场 Coq 会议时，曾试着提出这样一个观点：在英语世界里，把一种名为 Coq 的编程语言作为自己的“招牌”，其实是一种不小的阻碍。不过当时我想，听众们大概并不这么认为。我还开玩笑说，那场演讲中许多报告的内容，听起来简直像提利昂·兰尼斯特的演讲——因为现场竟然有那么多 Coq 和 Hoare 的演讲。这个笑话既幽默又切合时宜，尽管它在那部剧的最后一季播出前才被提及，而我们对它的记忆也早已模糊不清，但不得不说，这番玩笑真是恰到好处、妙趣横生。)

问题一直在于：当一个类型系统拥有强大的功能时，其证明工作也会随之变得极为繁重。我完全能证明自己曾耗费整整一天时间，去证明一些极其简单的命题。

事实上，做证明的过程本身相当有趣：它充满挑战性、互动性强，而且目标清晰明确。可天哪，这真的需要花费大量时间——尤其是当你像我一样，根本不知道自己在做什么的时候。

此外，每过数小时的努力之后，你总会迎来一段令人沮丧的时刻：你突然意识到，自己原本想要证明的目标，其实根本就是错误的。经典的 结果 就是 seL4 项目中的一次回顾性分析结果：尽管该项目规模庞大，工程师们也因此积累了丰富的经验，但他们用于证明的时间却比设计与实现所花的时间足足多了十倍。

最终，他们编写的证明代码数量，竟然是 C 代码的二十多倍。

这样的额外开销，让依赖类型语言的编程变得极其小众。这也促使人们开始尝试通过自动化手段来摆脱这一负担。我略知一二的尝试之一是 F*，该系统试图让 SMT 求解器自动履行各项证明义务。

在处理简单案例时，这种方法确实很有效；然而，要精心设计出某种触发条件，让 SMT 求解器“飞向太空”，一跑就是好几个小时，甚至让你不禁怀疑：它到底能不能完成任务？

我见过很多使用这类语言的人，不得不培养出一种第六感，去判断什么才是能让求解器“开心”的时机，然后围绕这一判断来精心构建一切。

虽然这种方式的确有所帮助，但在某种程度上，它反而将问题转化为一种神秘主义：你最终侍奉的，是一个复杂而善变的“神”。

一个至关重要的事实是：至少从理论上讲，一旦某个命题被证明为真，其证明内容便不再重要——真正关键的，只是它的存在本身。然而，这一说法并非完全成立，因为还存在两个复杂的因素：首先，seL4 团队所称的“证明工程”：我们需要对证明进行结构化设计，从而最大限度地减少在代码变更后重新调整证明的代价。

其次，过于复杂的证明，甚至可能让类型检查器崩溃，耗尽大量内存。

如今，我们已经拥有了大语言模型，它们与证明无关性的理念相结合，有望成为一种极具能力的证明自动化工具。只要自动化程度足够高，或许你就再也不必太过担心证明工程的问题了。

当然，你仍然需要避免让类型检查器“爆仓”，不过根据我有限的测试，大语言模型确实能够做到这一点。从长远来看，大语言模型或许会大幅提升依赖类型系统的实用性。

为了进一步探索这一领域，我在 Lean 中实现了一个 Zstandard 解压器——主要是因为我同样对 Zstandard 感兴趣。

Zstandard 似乎正逐渐赢得取代 gzip、成为标准压缩工具的竞赛。它同样是基于 LZ77 算法的压缩器，但其熵编码效率更高，且经过精心设计，能够实现极为惊人的解压速度。

它永远无法达到 bzip2 那般精妙绝伦，然而，在诸多实际优势面前，Burrows–Wheeler 变换那闪耀而优雅的美感，也显得微不足道：

(测量数据均来自标准参考计算机，也就是当时作者所使用的设备。请注意纵轴的对数刻度：gzip 和 Zstandard 分别属于各自的速度类别。这是一台苹果电脑，而且苹果的 gzip 经过特别优化；在其他地方，gzip 的速度可能会慢一些。)

Zstandard（由 Yann Collet 所作，基于 Jarek Duda 的开创性 答： 工作）拥有 一个橄榄球俱乐部，但其结构相当简洁。它包含了实现解压器所需的所有信息，不过如果你对压缩技术还不太熟悉，我认为你可能需要反复阅读几遍，才能真正理解其中的原理。

至少对我而言，我花了将近六次阅读第 4.1 节，才终于觉得对它的理解有了不错的把握。等到过程进行到后期，我才发现我的同事 Nigel Tao 已经撰写了 对Zstandard的更好介绍——而我本来打算自己完成的。

所以，如果你想真正理解 Zstandard，不妨先读一读那篇文档。接下来，我只想简单解释其中最有趣的部分——熵编码器，并顺便用一点关于 Lean 的“福音”来加以补充。

熵编码器的任务，是在给定一组概率不均的符号时，用最少的比特数对这些符号序列进行编码。经典的熵编码器是哈夫曼编码器。哈夫曼编码器会在叶节点上构建一棵二叉树，而哈夫曼证明：一种极其简单的算法就能生成最优的前缀树：你只需将符号列表整理好，找出概率最低的两个符号，然后以这两个符号为子节点，构建出一棵树节点。

这棵树节点的概率，等于其两个子节点概率之和；接着，你再用更少的符号重复这一过程，只不过这一次，树节点中加入了更多符号。显然，这一算法的每一步都会使元素集合的大小缩小一个单位，因此它最终会终止，并且还能生成一颗最优的树。

哈夫曼树之所以运行得非常快，是因为你可以建立一张表，以接下来 n 位作为索引（n 是最长编码的长度）。表中的每一项，都告诉你已经解码出了哪个符号，以及还需要读取多少比特。

哈夫曼树的缺点在于：它每次只能为每个符号使用整数比特数。如果有一个符号的 -log2(p) = 2.3，那么理想情况下，你应该用 2.3 比特来编码它。

然而，哈夫曼编码器却迫使你要么向上取整到 3 比特，要么向下取整，而这又会导致其他符号被迫消耗更多的比特。

Zstandard 使用的是哈夫曼树，但它还配备了一种压缩率更高的熵编码器，名为 FSE。FSE 是一种状态机。状态的数量多于符号的数量，而每个符号所对应的州份数，恰好与其在流中出现的概率相匹配。

因此，如果某个符号预计会出现 50% 的概率，那么它所对应的州份数大约也是 50%。每个状态都有三个值：该状态的符号、在该状态下从比特流中读取的比特数，以及一个基准状态编号——该编号会与这些比特相加，从而确定下一个状态。

回想一下，哈夫曼树的问题在于：它们只能使用整数比特数，而这些状态也同样需要读取整数比特数。不过，诀窍在于：如果你希望为某个符号读取 1.5 比特，那么一半的状态会读取 1 比特，另一半则会读取 2 比特。

这样一来，你平均来说就能达到目标。状态表并不会被传输。RFC 规定了从符号概率列表中构建状态表的算法，因此只需要传输概率即可。

让我们来举个例子。假设我们有四个符号，要使用 16 个状态。因此，我们必须将符号的概率近似为 16 分之一。（如果你想获得更精确的近似值……）