LLM 开始替 Lean 写证明：形式化验证最贵的一步可能正在自动化
作者：林岚｜OC 开发者生态编辑
林岚
ImperialViolet 作者 Adam Langley 用 Lean 实现了一个实验性的 Zstandard 解压器，并让多个 LLM 为其中的复杂性质自动生成证明。他确认这些证明能够通过类型检查，且没有用 sorry 跳过证明。
一句话结论：LLM 没有让形式化验证变得免费，但它可能正在消除大量“结论已经正确、只是证明太费时间”的机械工作。
依赖类型语言允许程序把复杂约束写进类型。例如，读取 n 个字节后，不只是返回一个字节数组，还要证明数组长度确实是 n。普通语言通常把这类条件留在注释、测试或运行时检查中；Lean 则要求机器在编译阶段接受证明。
代价一直很高。seL4 项目的回顾显示，验证工作量远高于实现本身，证明代码规模也远大于被验证的 C 代码。自动求解器可以处理简单目标，但复杂问题可能长时间不收敛，工程师还得学习如何把代码写成求解器容易接受的形状。
Langley 的实验把角色拆开：LLM 负责探索证明路径，Lean 内核只接受能够形式化检查的结果。模型可以胡说，但错误证明不能通过类型检查。这与普通 AI 编程不同，验证器不是另一位“看起来同意”的模型，而是一套确定的规则。
实验中的 FSE 表构造证明覆盖了表大小、符号状态数量、状态跳转范围和可达性等性质。多个模型大约 20 分钟完成证明，但也修改了原有实现，让代码更适合证明系统。这里的自动化不是对任意旧代码按一下按钮，而是代码和证明一起迭代。
边界同样明显：这个解压器是学习项目，没有公开成生产实现，速度约比命令行 zstd 慢十倍；作者尝试把方法扩展到 AArch64 汇编等价证明时，也很快撞上内存和规模限制。
关键事实
- 实验对象：Lean 编写的 Zstandard 解压器
- 自动化内容：由 LLM 生成并修正形式化证明
- 验证方式：Lean 类型检查器确认，不使用
sorry - 已知限制：实现较慢、规模较小、汇编验证尝试难以扩展
OC 判断
这项实验最有价值的不是“AI 会证明定理”，而是把模型输出放进一个不能靠语气蒙混过关的验证闭环。形式化方法能否普及，仍取决于证明维护成本和大型系统扩展能力。
为什么重要
- 对开发者：关键不变量可能从注释和测试升级为机器可检查契约。
- 对企业：密码学、解析器和系统软件会最先受益，但需要专业审查。
- 对 AI 工具：生成速度只有和确定性验证结合，才真正降低错误风险。
评论
围绕这篇文章补充信息、提出问题或分享观察。