我们现在拥有证明自动化了
Hacker News 摘要原标题：We have proof automation now
作者长期以来一直对 Coq（现已更名为 Rocq）和 Lean 等依赖类型语言深感兴趣。这类语言的类型系统能够编码并强制执行极其微妙的不变量。在普通编程语言中，这些细节往往只能写在注释里，并随着团队规模扩大而遗失，最终导致组件之间出现难以调和的误解。依赖类型则提供了一种诱人的可能性：让机器来正式检查这些不变量。
证明自动化的挑战与突破
虽然依赖类型功能强大，但其代价是巨大的证明成本。作者曾为了证明一些简单的事情耗费数天。著名的 seL4 项目回顾显示，工程师在证明上花费的时间是设计和实现时间的 10 倍，证明代码量更是达到 C 代码的 20 倍。这种高昂的开销使得这类语言一直处于小众地位。
此前，如 F* 等系统尝试利用 SMT 求解器自动完成证明，但这往往需要开发者具备某种“直觉”去迎合多变的求解器。现在，LLM 的出现为证明自动化带来了新的希望。LLM 结合“证明无关性”，可以极大地降低证明工程的负担。
在 Lean 中实现 Zstandard 解压器
为了实验这一想法，作者用 Lean 编写了一个 Zstandard（简称 zstd）解压器。zstd 正在逐渐取代 gzip，它是一种 LZ77 风格的压缩算法，提供更好的熵编码设计，且解压速度极快。虽然在压缩率曲线上它不如 bzip2 优雅，但在实用性上具有压倒性优势。
熵编码：Huffman 与 FSE
zstd 使用了 Huffman 编码和 FSE（有限状态熵）编码。
• Huffman 编码：通过构建二叉树产生最优前缀码。缺点是每个符号必须占用整数个位。
• FSE 编码：这是一种状态机。每个状态包含符号、要读取的位数和基准状态值。其精妙之处在于，如果一个符号理想情况下需要 1.5 位，FSE 会让一半的状态读取 1 位，另一半读取 2 位，从而在平均意义上达到目标。这种编码方式运行极快，但必须从后往前反向处理。
Lean 语言的特性
Lean 不仅是证明工具，也是一种实用的编程语言：
• 严格求值：与 Haskell 的惰性求值不同，Lean 是严格求值的，这使得程序性能更容易推理。
• 语法糖：拥有类似命令式语言的 do 语法，支持循环、return 和 break。
• 原地更新优化：当对象的引用计数为 1 时，Lean 会执行原地变异更新，效率媲美命令式语言。
在解压器的代码中，作者利用 Lean 在编译阶段证明了数组索引不会越界。例如，在处理 RLE（游程编码）块时，通过证明其内容大小必然为 1，从而安全地访问数组首元素，而无需在运行时进行边界检查。
LLM 助力高级证明
作者为 FSE 表构建算法编写了一系列复杂的数学定理，包括：
1. 生成的表大小必须正确。
2. 给定符号的状态数量必须符合其概率分布。
3. 所有状态转移后的结果必须是有效的状态编号。
4. 对于任何目标状态，存在且仅存在一个前置状态可以到达它。
这些复杂的定理如果靠人工证明需要极大的工作量，但现在的 LLM 可以在大约 20 分钟内自动完成。虽然作者为了配合 LLM 调整了部分实现代码（减少了命令式风格的使用），但最终证明全部通过了类型检查且没有使用 sorry（跳过证明的占位符）。
验证汇编代码的尝试
作者还提到了亚马逊 AWS 开发的 LNSym，这是一个 AArch64 的语义模拟器。理论上，我们可以利用 LLM 生成极其高效的汇编代码，然后证明它与 Lean 实现的功能等价。虽然目前的工具（如 SAT 求解器）在处理复杂函数时仍会遇到内存不足等性能瓶颈，但对于微小函数，这种自动化验证已经可行。
总结
尽管作者编写的 Lean 版解压器比传统的 C 语言版本慢 10 倍，但证明自动化的成熟预示着一种全新的编程范式。通过结合强类型系统和 LLM，开发者可以更实际地追求软件的正确性，这不仅改变了数学证明的现状，也正在改变日常的软件工程。