LLM 让 Lean 证明自动化成为现实
We have proof automation now
我一直对 Rocq 和 Lean 这类依赖类型语言情有独钟，它们能将微妙的不变量编码进类型系统，避免团队协作中的理解偏差。但过去，强大的类型系统意味着巨大的证明成本，像 seL4 项目那样，证明代码量是 C 代码的二十倍，耗时更是设计实现的十倍。F* 等尝试用 SMT 求解器自动化，却常陷入不可预测的等待，迫使开发者像侍奉神灵般揣摩求解器喜好。如今，LLM 的出现结合证明无关性理论，让证明自动化变得极具潜力。我尝试用 Lean 编写了一个 Zstandard 解压缩器，发现 LLM 能有效规避类型检查器崩溃，让依赖类型系统突然变得实用。Zstandard 凭借 FSE 熵编码器在压缩率和速度上超越 gzip，而 LLM 或许能让我们不再为繁琐的证明工程而头疼。
一旦陈述正确，其证明的具体内容其实无关紧要，唯有证明的存在本身才真正重要。
HN 评论区
104- m1el
非常赞同作者的观点。未来的编程语言必将把定理证明器原生嵌入到类型系统中，这样 LLM 就可以通过形式化证明来验证其生成的实现是否符合规范，从而省去大量测试工作。编写形式化规范恐怕是未来程序员完成工作所需的核心技能。
Verus（https://github.com/verus-lang/verus）是 Rust 生态的一个良好开端，但它目前本质上仍是一门独立语言（拥有自定义语法和类型系统）。
- el_pollo_diablo
作为一个关于该话题的元评论，我注意到大家对于“在项目中如何使用定理证明器”仍存在困惑。前几天我看到 Paradigm（一家如今似乎已被 AI 洗脑的加密领域风投）发的一条推文。他们的一位 LP 用 Lean 4 对以太坊虚拟机进行了形式化。推文中声称，如果用 LLM 完成这项工作，将花费约 15 万美元的 API Token 费用（“将花费”意味着他们大概是免费获取的），且 LLM 需要一周的推理时间。我不知怎么被吸引去仔细看了看代码，发现其中的定理其实寥寥无几。该项目也没有使用 Batteries 或 Mathlib，而这两者恰恰是我个人使用 Lean4 的最强动力之一。也就是说，我通常更倾向于依赖他人把范畴论和代数结构搞对，然后我只需承担证明我的“玩具模型”与之对应的证明义务。在这种情况下，我很乐意使用 LLM 进行证明搜索，这和我使用 SMT 求解器的方式非常相似。但我发现，必须强行逼迫语言模型去使用这些库，否则模型更倾向于过拟合，并在 3 分钟的推理任务中过度宣称已找到解决方案，而不是花 3 个小时去履行证明义务。当我需要说服 LLM（我用的是 Claude）说履行证明义务是为了“学术练习”或是被迫为之时，我感到一阵恶心，否则它就会……