我们现在有了证明自动化

# 我们现在有了自动证明 来源：https://www.imperialviolet.org/2026/07/26/zstd-lean.html 我一直对依赖类型语言（如 Coq、Rocq 和 Lean）情有独钟。它们提供了一种类型系统，能够编码和强制执行任意微妙的约束。在常规语言中，这类约束最终（最好情况下）只能作为注释存在，并且随着团队规模扩大很快就会被遗忘。然后就会出现微妙的误解，以及各组件之间无法完全匹配的问题。通常，这些组件已经发展到相当大的规模，以至于当问题被发现时，调整其中任何一个都是一件令人疲惫的前景。也许，依赖类型语言会诱人地建议：你可以将这些不变量形式化，然后让机器来检查它们。 （附注：Coq 改名了！我记得多年前在普林斯顿的一次 Coq 会议上，我曾试图建议，在一个英语主导的世界里，有一门叫 Coq 的编程语言是一种障碍。当时听众似乎并不同意。我还开玩笑说，那里的许多演讲听起来像是提利昂·兰尼斯特的演讲，因为到处都是“Coq”和“Hoare”。这个笑话在当时既幽默又应景，尽管它完全冷场了——因为那是在那个剧的最后一季播出之前，而我们现在已经集体淡忘了它。） 问题始终在于：强大的类型系统伴随着巨大的证明工作量。我可以证明：我曾经花了一整天的时间去证明一些相当简单的事情。做证明其实很有趣：它充满挑战、交互性强，并且有明确的目标。但天啊，它确实非常耗时，尤其是如果你像我一样，根本不知道自己在做什么。还有一种令人沮丧的体验：经过数小时的努力后，你意识到你试图证明的目标实际上是*错误的*。经典的例子是 seL4 项目的回顾报告，它发现即使项目足够大，工程师们已经积累了相当多的经验，他们花在证明上的时间仍然是设计和实现的十倍。最终，他们的证明代码行数是 C 代码的 20 多倍。 这种开销使得依赖类型语言的编程变得极其小众。这也促使人们试图通过自动化来消除这一负担。我略知一二的尝试是 F\*，该系统尝试让 SMT 求解器自动处理证明义务。这在简单情况下确实有效，但很容易构造出一些让 SMT 求解器陷入无限循环、运行数小时的情况，让你怀疑它到底能不能结束。我观察到，经常使用这类语言的人必须培养出一种第六感，知道什么能让求解器满意，然后围绕这一点来构造一切。这种方法有所帮助，但在某种程度上，它把问题变成了神秘学：你最终要侍奉一个复杂且反复无常的神明。 一个关键事实是：至少在理论上，一旦命题成立，其证明的内容就无关紧要了：只有它的存在才重要。这并非完全正确，原因有两个复杂因素：第一，seL4 团队所谓的“证明工程”——需要结构化证明，以便在代码变更后减少重新调整证明的工作量。第二，足够复杂的证明甚至可能导致类型检查器崩溃并消耗大量内存。 现在我们有了 LLM，结合证明无关性，它们有望成为一种极其强大的证明自动化形式。有了充分的自动化，也许你就不需要太担心证明工程了。你仍然需要避免使类型检查器崩溃，但根据我有限的测试，LLM 可以避免这种情况。从潜在意义上讲，LLM 突然使依赖类型系统变得极为实用。我想尝试一下，所以在 Lean 中构建了一个 Zstandard 解压缩器，主要是因为我也对 Zstandard 感到好奇。 Zstandard 似乎正在赢得取代 gzip 成为主流压缩工具的竞赛。它是另一种 LZ77 风格的压缩器，但提供了更好的熵编码和精心设计，使其能够实现令人印象深刻的解压速度。它永远不会像 bzip2 那样优雅，但面对显著的实用优势，Burrows–Wheeler 变换的光辉优雅并不太重要： zstdbzip2gziplzma（XZ/LZMA2）5010020050010002000zstdbzip2gziplzma（XZ/LZMA2）70727476788082848664 MiB Lean/mathlib 源代码上的压缩权衡节省空间（%）——越靠右压缩率越高解压吞吐量（MiB/s，对数刻度）——越高越快（测量在标准参考计算机上进行，即作者当时使用的机器。注意 y 轴是对数刻度：gzip 和 Zstandard 属于同一速度等级。这是一台 Apple 机器，Apple 的 gzip 经过了特别优化；在其他平台上 gzip 会更慢。） Zstandard（由 Yann Collet 基于 Jarek Duda 的开创性ANS 工作构建）有一个RFC，但相当简洁。它包含实现解压缩器所需的所有信息，但除非你已经熟悉压缩，否则我认为你需要重读几遍才能理解发生了什么。至少，我不得不将第 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 分之几的形式来近似符号概率。（如果你想要更精确的概率近似，可以使用更多的状态；zstd 实际上从不使用少于 32 个状态。） 状态0123456789101112131415符号AABDABCABCABCAAB位数2124123122112111基线1204028841206048102任何符号后面都可以跟任何其他符号，一个符号可能只有一个状态。因此每个符号必须能够到达每一个状态。看一下状态 3，它是符号 D 的唯一状态。因为是唯一一个，它必须读取 4 位，这足以编码任何其他状态。但如果你看一个像 B 这样的符号，它的状态只要求读取 1 或 2 位。然而，16 个可能的下一个状态被精确地划分给了符号 B 的那些状态。所以，对于任何一个特定状态，符号 B 恰好有一个状态可以到达它。 FSE 解码表单元铺满状态空间一个 16 单元解码表，符号 B 占据状态 2、5、8、11 和 15。箭头将 B 的每个单元连接到其下方的目标范围：状态 11 覆盖下一个状态 0 到 1，状态 15 覆盖 2 到 3，状态 2 覆盖 4 到 7，状态 5 覆盖 8 到 11，状态 8 覆盖 12 到 15。五个范围一起覆盖了全部十六个状态。0123456789101112131415AABDABCABCABCAAB0–11 位2–31 位4–72 位8–112 位12–152 位再次考虑符号 B，我们说过它的概率是 5/16。编码该符号的理想比特数是 -log2(5/16) = 1.68。符号 B 有三个状态读取 2 位，两个状态读取 1 位。这些状态的使用频率并不相同，按照使用频率加权平均后，结果几乎正好等于量化概率的目标值。如果你想更精确地捕获真实符号概率，可以使用更大的表。 核心技巧在于：通过给更常见的符号分配多个状态，编码器不仅仅选择符号：它还选择要落在该符号的哪个状态上，而这个选择将信息向前传递给下一个符号。这就是分数比特信息的去向。但这个熵编码器仍然是基于表的，因此运行得非常快。 麻烦在于你不能正向工作。假设你要编码 C, D。你从哪个 C 状态开始？嗯，D 只有一个状态，所以你必须从能够到达那个状态的 C 状态开始。如果 D 有多个状态，那么你还需要考虑 D 后面是什么，才能知道需要哪一个* C 状态*。FSE 迫使你从序列的末尾开始，逆向工作。（这还不算太糟，因为为了计算符号概率，你通常无论如何都需要知道整个序列。）此外，Zstandard 压缩器因此是反向编码符号，但增量地写入输出，所以解压缩器必须找到块末尾，然后反向读取比特来理顺！这涉及到更广泛的格式细节，我不打算深入讲解；请参见Nigel 的文章。 基本的熵编码器不关心符号间的概率关系。也就是说，它们无法利用字母 Q 在英语中不成比例地后面跟着 U 这一事实。必须通过其他编码来利用这些冗余。在 Zstandard 中，那是传统的 Lempel–Ziv 结构，它要么编码原始字节，要么编码对先前解码数据的反向引用。因此 FSE 主要用于高效编码这些反向引用的偏移量和长度。 ### Lean 我们来谈谈 Lean！上面我说它是一种依赖类型语言，这个概念用例子来说明比用复杂的定义更好。所以，这里有一个函数的类型，它从流中读取 *n* 个字节，如果不抛出异常，则返回一个字节数组，且类型系统知道该数组长度为 *n*。 `` def IO.FS.Stream.readExact (st : Stream) (n : Nat) : IO {ba : ByteArray // ba.size = n} := ... `` 这是一个函数，它返回两个数字和一个字节数组，要求第一个数字是质数，两个数字之和能被 6 整除，并且字节数组的长度至少等于这两个数字中较小的那个。 `` def getResult : IO (Σ a b : Nat, { bytes : ByteArray // Nat.Prime a ∧ 6 ∣ a + b ∧ Nat.min a b ≤ bytes.size }) := ... `` 这并不是任何人都会需要的类型。它只是展示了你可以随心所欲地疯狂使用这种特性。依赖类型语言足以编码即使是非常复杂的数学结构，而 Lean 目前的主要用途是作为陈述和证明数学的形式化语言。最近出版的《代码中的证明》一书，是一本简短、写得很好、讲述了 Lean 是如何诞生的故事的书。作者在几段话中完全歪曲了构造性数学，但除此之外，我很喜欢这本书！ Lean 是一种纯函数式语言，类似于 Haskell，尽管它具有一些可能使其作为编程语言更加方便的特性。首先，Lean 是严格的，而 Haskell 是惰性的。严格意味着函数的参数在调用之前就会被求值，而在 Haskell 中，参数的求值会被推迟到实际需要该值时。因此，在 Haskell 中，你可以毫无代价地编写昂贵的表达式并将它们传递给函数，因为它们只会在最终被使用时才会真正计算。但这也意味着计算可能发生在程序中非常意外的地方。这是一个有争议的话题，但尽管我欣赏惰性的优雅，天啊，它确实让程序的性能很难推理。 其次，Lean 有一些不错的语法糖。它的单子 `do` 记法包含了 for 循环、return 语句和 break 语句。如果你想以命令式风格编程，你可以相当合理地做到这一点！ 最后，Lean 有一个优化：只要对象的引用计数为 1，它就会对其进行原地修改更新。因此，只要你小心不让其他地方有引用，你就可以像命令式语言一样高效地原地修改数组。不幸的是，据我所知，Lean 没有任何线性类型系统的特性，因此它不会帮助你确保值只有一个引用。这是一个双刃剑：代码中看似微小的改动，可能会因为某个不起眼的地方持有对大型数组的引用而完全拖垮性能。但这确实意味着，如果你想优化某事的性能，你有更多工具可用。 以下是我草拟的 zstd 解码器中的一些例子： `` while true do let some blockHeaderBytes ← input.readExactOrEof 3 | break let some blockHeader := BlockHeader.fromBytes blockHeaderBytes frameHeader | throw (.userError "invalid block header") let blockBytes ← input.readExact blockHeader.contentSize match hty : blockHeader.type with | .rle => let b := blockBytes.val[0]'(by rw [blockBytes.property, blockHeader.contentSize_rle hty]; omega) `` 注意第 9 行。有一个数组索引