事件概述

2026 年 7 月 26 日，ImperialViolet 博客发表了一篇题为 “We have proof automation now” 的文章。作者长期关注依赖类型语言（如 Coq / Rocq 和 Lean），这类语言借助强大的类型系统能够编码并自动检查程序中的复杂不变量。然而，代价是巨大的证明工作量——例如 seL4 项目中，工程师在证明上的时间投入是设计与实现的 10 倍，证明代码行数超过 C 代码 20 倍。现在，作者观察到 LLM（大语言模型）与证明无关性（proof irrelevance）结合，可能极大地降低证明开销，使得依赖类型系统变得实用。为验证这一想法，他选用 Lean 语言实现了一个 Zstandard 解压器，并在文章中分享了 Lean 与 Zstandard 熵编码的技术细节。

关键技术点

1. 依赖类型与证明自动化

  • 依赖类型语言（如 Lean）允许在类型中编码任意精度的约束，编译器可自动检查。但以往需要大量人工证明，且证明代码维护困难（“proof engineering”）。
  • LLM 的优势：由于证明无关性（只要存在证明，不论其构造方式），LLM 可自动生成证明草稿，减少人工编写时间。作者初步测试表明 LLM 生成的证明能避免类型检查器爆炸（blow up），大幅降低实践门槛。

2. Zstandard 解压器实现

  • Zstandard（zstd）是一种现代压缩算法，旨在替代 gzip，核心采用 LZ77 和 ANS 熵编码（FSE）。
  • 作者在 Lean 中完整实现了 Zstandard 解压器，重点介绍了 FSE（Finite State Entropy）状态机：
    • 传统 Huffman 编码只能使用整数字位，当概率对数非整数时存在效率损失。
    • FSE 通过多状态分配，使每个符号占用非整数比特的平均位数（例如 1.5 比特可通过一半状态读取 1 位、另一半读取 2 位实现），从而逼近理论熵极限。
  • 作者引用同事 Nigel Tao 的 Zstandard 解释作为更优参考，自己仅聚焦最有趣的熵编码部分。

3. LLM 辅助证明的实践

  • 作者提到，使用 LLM 可以避免传统的 “proof engineering” 问题：当代码变更后，证明需要调整；而 LLM 能快速重新生成匹配的证明，降低重构成本。
  • 但需注意类型检查器仍可能因复杂证明而耗尽内存，不过作者的测试显示 LLM 可以避免此类情况。

对数据科学或 AI Agent 落地的意义

  1. 形式化验证与 Agent 安全：AI Agent 的可靠动作需要基于严格的逻辑保证。依赖类型 + LLM 自动证明，可以低成本地验证 Agent 的行为规范（如不越权、资源约束等），提升安全性。
  2. 低代码验证：传统形式化验证需要高深的证明技能，LLM 能将此过程平民化，使更多数据科学家和工程师能够在项目中引入形式化验证，减少运行时错误。
  3. 压缩算法与数据存储：Zstandard 的高压缩比、解压速度优势，在数据管道和 AI 训练数据存储中具有重要价值。Lean 实现的解压器虽然不一定用于生产，但展示了用形式化方法保证压缩实现正确性的可行性。

我的技术点评

这篇文章敏锐地捕捉到了 LLM 时代形式化验证的拐点。过去，依赖类型语言的最佳实践是 “写证明到不想写”，现在 LLM 提供了一条 “让机器帮我们写证明” 的路径。尽管 LLM 生成的证明可能不够优雅，但证明无关性保证了正确性优先于美观。

不过，文章包含几个原文未详细阐述的潜在问题：LLM 生成证明的正确性仍需人工核验（或借助 Isabelle 等自动化工具检验）；LLM 对大型项目的证明生成是否存在上下文窗口限制；以及验证环境中 LLM 的推理成本。作者仅在有限测试后便得出结论，缺乏系统性基准，因此该方案的实际落地还需更多实验数据支撑。

此外，Lean 本身是活跃发展的证明助理，社区已积累大量数学和工程的证明库（mathlib）。结合 LLM 的补全能力，或许能催生新一代 “AI 辅助证明” 的开发范式，这对 AI Agent 的自我验证、自主编程都有启发性。

总体而言，这是一篇兼具工程实践与前瞻思考的优秀文章，值得关注形式化验证与 AI 结合的读者仔细阅读。

原文链接