Lean 证明自动化刚刚从研究走入真实软件

7 月 26 日，Lean 证明自动化跨过了一条实用门槛：安全工程师 Adam Langley 介绍了一款由 AI 辅助、经过形式化验证的 Zstandard 解码器。Langley 称，多款大型语言模型在约 20 分钟内生成了大量证明。随后，Lean 对这些证明进行了检查，且没有接受未完成的占位符。这项实验规模不大，却挑战了一个长期顽固的假设：经过验证的软件，其证明成本或许不再远高于程序本身。

这并不意味着某个 AI 模型从宽泛或哲学意义上“证明”了解码器正确。Langley 选择了要验证的性质，编写了大部分实现，并确认 Lean 接受了最终生成的证明项。他的解码器运行速度也约为标准 zstd 命令的十分之一。真正的进展更聚焦，也更具实际价值：AI 如今已能完成足够多的形式化证明工作，从而改变哪些工程项目在经济上看起来合理。

这让常规测试与形式化验证进入了一场新的较量。测试只抽样覆盖特定执行路径，而形式化证明可以覆盖定理所表示的每一种输入。过去，这种更强的保证往往伴随着极高的人力成本。著名的 seL4 操作系统项目曾报告，其证明工作远超实现工作。如果 AI 能在不进入可信验证路径的前提下压缩这类劳动，那么有证明支撑的软件将不再只是内核和密码学领域的专属选择。

Lean Zstandard 实验究竟改变了什么

关键结果不在于 AI 写了代码，而在于 AI 生成的证明工作通过了独立的机械检查器。

Langley 使用 Lean 构建了一个 Zstandard 解压器。Lean 是一种函数式编程语言，也是交互式定理证明器。Zstandard 通常简称为 Zstd，是一种面向快速无损压缩设计的压缩格式。其解码器必须正确解析紧凑的头部、熵编码符号、长度、偏移量和重复序列。

这些细节恰好会产生普通类型系统难以排除的漏洞。解码出的长度可能与可用输入不一致。数组索引可能越过边界。格式错误的表可能产生本不应存在的状态。开发者通常通过验证、运行时检查、测试、模糊测试和仔细审查来处理这些可能性。

Lean 增加了另一种选择。它的依赖类型系统允许类型包含有关某个值的事实。一个函数可以同时返回字节数组，以及该数组具有所请求长度的机器检查保证。后续代码在访问元素时可以使用这一保证。

Langley 在一个针对游程编码的解码器分支中展示了这种模式。该分支需要从一个块中读取一个字节。Lean 要求证明该块确实包含这个字节。实现将请求读取的长度与一条定理关联起来，该定理表明这种块类型的内容大小始终为一。

这个局部证明很短。更具影响力的例子涉及有限状态熵编码，即 FSE；Zstandard 使用它来高效表示符号。Langley 实现了该格式中描述的建表算法，随后要求 AI 系统证明其输出具有普遍性质。

所要求证明的性质超越了基于示例的测试。它们涵盖表大小、分配给每个符号的条目数量，以及表内的有效状态转换。换言之，这些证明描述的是应在所有被接受的分布中成立的结构规则，而不只是规范提供的三个测试向量。

Langley 报告称，多款 LLM 大约在 20 分钟内完成了这些证明。他还表示，这项工作只消耗了标准月度订阅额度中的一小部分。由于其命令式结构阻碍了 Lean 的证明机制，这些模型修改了他实现的一部分。随后，他确认最终证明通过了类型检查，并且不包含 sorry——Lean 用于标记未完成证明的显式标记。

包括代码摘录和局限性在内的完整说明见原始 proof automation 文章。他没有发布解码器仓库，因此外部开发者尚无法复现每一项主张。这仍是一份经验报告，而非经独立基准测试验证的结果。

不过，该实验确立了一种可信的工作流。人类陈述不变量。AI 搜索证明，并在必要时重塑代码。Lean 检查生成的证明项。模型提供劳动，而检查器决定是否接受。

正是这种分工，使这一结果区别于普通的 AI 编码演示。

为什么 Lean 证明自动化对知识工作者很重要

证明自动化之所以重要，是因为它可以将关键假设从文字表述转化为经过检查、可复用的工作成果。

大多数知识工作者不会编写压缩解码器。但他们仍身处由未文档化假设构成的系统之中。一个财务模型假定某一列包含唯一标识符。一个政策工作流假定每一项审批都有明确的责任人。一个研究流程假定每一条引文都保留其来源。

团队往往在文档、注释、入职材料或会议记录中表达这些规则。随着工作跨越工具和部门，这些规则会逐渐弱化。一次字段重命名、一个异常记录或流程变更，都可能使其失效，却不会立即发出警告。

形式化方法在软件中处理的是类似问题。它们将选定的假设转化为足够精确、可由机器检查的陈述。Lean 使用依赖类型，即类型可以依赖于值，因此能够编码输入与输出之间的详细关系。

这种语言并非只是运行一段由 AI 生成的证明脚本，然后相信其结论。Lean 策略会构造证明项，即可独立检查的论证表示。随后，一个小型内核验证每个证明项是否遵循系统的逻辑规则。官方 Lean kernel 文档描述了便捷自动化与可信检查之间的这种分离。

这种架构改变了围绕 AI 的风险计算。语言模型可能会虚构策略、误解定义，或追逐错误目标。多数此类失败会产生被拒绝的代码，而非悄然被接受的定理。模型可以不可靠，但最终验收关口仍然严格。

这并不意味着整个工作流毫无错误。一个有效证明可能证明了错误的陈述。定义可能遗漏现实世界的行为。导入的库可能引入假设。一个经过验证的源代码级函数，仍可能依赖未经验证的编译器、操作系统或处理器。

Lean 自身的 proof validation 指南强调了这些边界。内核接受表明，一个定理可从其定义和依赖项中推导出来。它并不表明该定理准确表达了某个人的意图。

对知识工作者而言，这一区别类似于公式无误、但业务定义错误的电子表格。计算可以内部一致，却回答了错误的问题。形式化将最困难的审查转向规格本身。

这种转变很有价值。与审查数千个机械化证明步骤相比，人类通常更擅长审查意图和上下文。AI 可以承担更多重复性搜索，而人们则审视那些真正必须成立的条件。

同样的模式已经出现在实际的信息工作中。AI 起草摘要、分类、查询和转换。一个负责任的工作流随后会根据一手材料、模式、约束或确定性计算来检查输出。证明自动化将这种模式应用到了严格得多的层面。

它也说明了为什么个人上下文依然重要。模型无法保护它从未见过的不变量。团队需要获取定义正确行为的决策记录、规格、示例和例外情况。维护良好的 personal knowledge base 会成为输入纪律的一部分，即使形式化证明仍是一项专业活动。

眼前的机会并不是将每一份备忘录形式化，而是识别那些已经像隐藏规格一样运作、且代价高昂的假设。这些假设往往位于系统、团队或监管义务之间的边界上。

新的较量是证明成本与验证价值

只有当 AI 降低证明劳动的速度快于它增加规格编写和维护工作的速度时，它才会改变形式化验证。

形式化验证从不缺少令人信服的成果。seL4 微内核就是一个突出例子。其机器检查证明将实现与形式规格连接起来，并覆盖仅靠测试无法确立的性质。

官方 seL4 verification 材料说明，受支持配置具有代码级功能正确性证明。部分配置还将这些保证扩展到二进制代码。该项目展示了：当风险足以支撑持续的专业投入时，形式化方法能够交付什么。

它也说明了为何采用范围始终有限。Langley 引用一份 seL4 回顾报告称，工程师在证明上投入的工作量约为设计和实现的十倍。他还指出，证明代码的规模超过 C 实现的二十倍。

这些比例不应被视作普遍税负。seL4 在复杂操作系统内核上追求了异常强的保障。不同性质、语言和工具链会产生不同成本。但这些数字捕捉到了历史问题：证明工作可能主导交付过程。

传统证明自动化能减轻其中一部分负担。化简器、判定过程、SAT 求解器和 SMT 求解器可以完成许多目标。然而，开发者往往仍需围绕每种求解器擅长处理的内容来组织代码和引理。

Langley 将这描述为培养一种让求解器满意的第六感。一个不在有利片段内的目标，可能让自动搜索走向无效路径。工程师随后要花时间将问题转换成工具可解的形式。

LLM 带来了一种不同的能力。它们可以阅读周围定义、检查错误信息、尝试策略、引入中间引理，并修改实现。它们并不要求每个问题都适配某一种固定的判定过程。

这种灵活性使 AI 成为现有证明工具之上的编排层。模型可以在合适之处调用确定性策略，在其他地方编写显式论证，并利用 Lean 的反馈修复失败。模型搜索证明策略，而内核提供严格的验收测试。

Langley 的经历也揭示了一项重要成本。他的 AI 助手修改了建表代码，因为他使用了过多的 Id.run，这是一种在 Lean 中表达命令式计算的方法。原始代码或许可读且可执行，但对证明而言并不友好。

这就是证明工程：通过组织程序和引理，使证明保持可行且易于维护的工作。AI 可能降低成本，但不会消除其根本张力。为人类熟悉度、运行时性能和证明简洁性优化的代码，并不总能共享同一种形态。

因此，经济问题随之改变。团队不再只问：“我们能证明这一点吗？”而是问：“当开发者快速迭代产品时，AI 能否同样快速地维护证明及其支撑结构？”

这更有利于边界稳定、明确的软件。解析器、授权策略、协议状态机、金融计算和数据转换通常具有清晰的属性，其失效模式也更值得投入更强的保障。

AWS 通过其授权策略语言 Cedar 提供了一个颇具参考价值的生产实践案例。AWS 在 Rust 实现旁维护可执行的 Lean 模型，并将证明与差分测试结合使用。公开的 验证开发 案例说明，Cedar 的发布要求模型、证明和测试均保持最新。

Cedar 并不证明每个应用都应该迁移到 Lean。它表明，形式化产物可以融入真实的发布流程。AI 辅助证明搜索或许能扩大能够持续采用这种流程的团队范围。

近期最有力的模式很可能仍是混合式的。工程师使用主流语言实现生产代码，在 Lean 中形式化高价值行为；测试比较两种实现，而证明则确立模型的属性。

Langley 采取了更直接的路径：直接用 Lean 实现解码器。这让代码与定理之间建立了紧密联系，但也带来了显著的性能代价。经过验证的模型与经过验证的生产代码之间如何取舍，仍是核心问题。

证明未能证明什么

经内核检查的证明可以消除一类不确定性，但规范、实现边界和运行环境仍可能存在未知。

“我们现在已经拥有证明自动化”这个标题本就是有意挑衅。实验在实践意义上支持这一说法，但仅限于已明确的范围之内。它并不能证明 LLM 能够独立验证任意生产软件。

首先，源代码并未公开。Langley 表示，他验证了这些证明能够通过类型检查，且不含未完成的占位符。读者可以评估他的推理和示例，但无法复现完整构建过程。

其次，这项工作涉及的是一个玩具解码器。Zstandard 是一种严肃的格式，FSE 表构建也并不简单。但该项目无需面对多年功能变更、多团队协作、向后兼容、恶劣的集成环境，或生产事故压力。

第三，这个解码器比标准命令行实现慢约十倍。这个差距不可忽视。软件不能仅因其证明优雅，就牺牲核心运行要求。

Langley 曾探索经过验证的汇编是否能解决性能问题。他考虑使用 AWS 的 LNSym 框架，证明优化后的 AArch64 汇编与 Lean 函数一致。小型示例能够运行，但该方法在他的测试中无法扩展。一个使用 bv_decide 的小示例——这是一种用于有限位向量命题的策略——所需内存就超过了他的机器容量。

这提醒我们，检查并非没有成本。证明项可能让内核处理起来非常昂贵。自动化搜索也可能耗尽内存或时间。理论上成立的工作流，仍可能无法满足构建预算。

第四，模型需要修改实现。这本身并非坏事。证明可以揭示，程序结构掩盖了它所依赖的关系。朝着显式不变量进行重构，或许会提高可维护性。

然而，AI 生成的重构也可能改变行为或降低性能。最终定理只保护其所陈述的属性。对于这些属性之外的一切，工程师仍需要测试、基准测试、代码审查和威胁建模。

第五，人类制定的规范仍是最敏感的环节。如果一个解码器定理证明了表的良构性，却遗漏了其他位置的整数溢出，那么已验证的属性依然为真，但并不完整。如果形式化的 Zstandard 行为与实际格式不同，Lean 也会忠实地验证错误的模型。

相关压缩格式记录于 RFC 8878，但将文字标准转化为定义仍涉及解释。歧义不会在进入定理证明器后消失，而会成为一种建模决策。

当非专业人士依赖 AI 同时生成命题和证明时，这种风险会进一步增加。模型可以通过弱化主张，让某项结论更容易被证明；它可以选择一种方便的定义，排除棘手输入；它可以满足检查器，却偏离审查者的意图。

这意味着证明审查需要一种不同的界面。审查者应能看到每个定理的自然语言解释、其假设、导入的公理、覆盖的代码路径以及排除的行为。仅有一个绿色勾选远远不够。

组织还需要建立业务决策与形式化定义之间的可追溯性。政策变更时，必须有人知道哪条定理编码了该政策；实现变更时，系统必须识别哪些保证需要重新审视。

这正是 AI 辅助能够超越编写策略而发挥作用的地方。智能体可以检索相关规范，将代码变更映射到受影响的不变量，并总结未满足的义务。一个可搜索的知识库可以将设计背景与形式化产物连接起来。

这些限制都不会否定这一成果。它们界定了要将其从一个引人入胜的实验，推进为可靠工程实践所需完成的工作。

Lean 证明自动化正在对 AI 编程工具施加压力

一旦模型既能生成代码，也能生成可检查的证明，“测试通过了”便开始显得是不完整的质量主张。

当前，AI 编程产品围绕任务完成能力、代码库理解、工具使用、基准分数和开发者体验展开竞争。它们的质量门槛仍类似于传统开发流程：智能体运行测试、代码检查工具、类型检查器、安全扫描器以及人工审查工作流。

这些检查很重要，但大多数无法确立普遍行为。单元测试只能证明：在某次运行中，一个选定输入产生了一个预期结果。模糊测试通过生成输入扩大覆盖范围，但它仍然是在抽样执行。静态分析可以覆盖更广泛的类别，但每种分析器都在既定近似条件下工作。

定理可以表述：每个被接受的输入都满足某个选定属性。如果 Lean 检查了该证明，那么这种保证就不依赖于对生成证明的模型的信任。对于智能体式编程系统而言，这是一个极具吸引力的产品差异化点。

这种压力会首先出现在狭窄任务中。AI 智能体或许会生成一个解析器，并附带证明：成功解析绝不会越过输入边界；它或许会实现一条访问控制规则，并提供排除未授权状态转换的定理；它也可能创建数据库迁移，并在形式化模型中证明模式不变量得以保持。

主流工具无需向每位用户暴露 Lean 语法。它们可以将形式化验证作为一种额外验证模式提供。界面可以要求开发者以自然语言确认属性，展示其形式化翻译，并返回已检查的证明或具体反例。

决定性功能不会是纯粹的定理证明分数，而是集成能力。证明自动化必须能够与代码库上下文、构建系统、规范、性能测试和代码审查协同工作。

Langley 的实验提供了一个有益的产品启示。这些模型以交互方式工作：它们遇到难以证明的代码，修改其结构，并持续推进，直到检查器接受结果。这更像一个工程智能体，而不是自动补全系统。

它还暗示了一种新的问责形式。AI 代码生成常常造成一种不对称：模型生成代码的速度快于人类审查代码的速度。能够生成证明的智能体，可以为选定主张附上机器可检查的证据。

这种证据并不会让审查变得可有可无。它让审查者可以少花时间模拟机械行为，更多审视主张本身。核心问题变成：“这是否是我们需要的属性？”而不是：“模型是否在某个索引边界情况上漏掉了什么？”

竞争者可以通过多种路径应对。他们可以直接集成 Lean，将模型连接到其他证明助手，为专用求解器生成证书，或将形式化模型与传统代码结合。最终胜出的方式可能因领域而异。

Lean 的优势在于，它在同一环境中支持编程、定理证明、元编程和广泛的自动化能力。其内核也提供了清晰的信任边界。但对于性能敏感的软件，Lean 并不必然是正确的部署语言。

因此，能够生成证明的 AI 将与具备证明检查能力的开发流水线竞争，而不只是与其他 LLM 竞争。可靠的单位是整个系统：模型、形式化陈述、证明工具、内核、编译器假设、测试和审查者。

对于购买 AI 产品的知识工作者而言，这带来了一个比询问供应商模型是否准确更好的问题：哪些输出获得确定性验证，哪些主张拥有可检查的证据，哪些仍依赖概率性判断？

证明自动化提供了这种模式的最强版本。它不会适用于每项任务，但会提高人们对任何可被形式化描述的输出的期待。

三个信号将表明这是否会成为常规工程实践

下一阶段取决于可复现性、变更下的维护能力，以及日常开发工具中的证明支撑功能。

第一个信号，是一个可公开复现、与 Langley 实验相当的软件代码库。开发者需要能够检查定义、提示词或智能体轨迹、证明项、公理、构建时间和硬件要求。独立团队应能够重新运行该过程，并测试替代模型。

可复现性将增强这样一种主张：当前 LLM 能够承担实质性的证明工作。若无法复现，则会将结论收窄为一位熟练工程师的设置与判断。无论哪种结果，都会改善现有证据。

第二个信号，是面对变化中的代码时的表现。一次性证明可能掩盖大量人工指导。更严格的测试是：在现实的实现变更后，智能体能否修复证明，同时不弱化定理，也不扭曲程序。

团队应衡量证明修复时间、人工干预、计算成本、定理变更和性能回归情况。他们还应追踪：失败的证明究竟多常揭示真实缺陷，而非无害的结构变更。

如果修复在数月开发过程中依然迅速，AI 就降低了证明工程的维护负担。如果每次变更都触发大规模重构，形式化验证仍将局限于稳定且高价值的组件。

第三个信号，是产品集成。应关注那些将经内核检查的属性作为标准输出的编程智能体，尤其是在解析器、策略引擎、协议实现和数据处理代码等领域。

可信的产品应将定理生成与定理检查分离。它应展示假设、拒绝未完成的证明、保留验证日志，并在代码变更使某项保证失效时发出警告。它还应将测试和基准测试保留在工作流中。

如果这些功能出现在主流工具中，Lean 证明自动化就已超越定理证明演示。如果它们仍局限于研究代码库，那么生产力收益尚未克服集成成本。

对知识工作者而言，务实的应对是准备更完善的规格说明。记录界定正确行为的决策。保留源材料。识别那些一旦被误解就会导致高昂代价的关键不变量。明确例外情况。

随后，对每个 AI 工作流提出一个更精准的问题：哪些输出能够接受可信、独立的核验？

Langley 的解码器并不能证明所有软件都可以得到形式化验证。它表明，AI 已开始攻克成本门槛，而 Lean 仍保留着严格的最终关卡。这已足以改变路线图。

不远的未来并不是由永不犯错的模型编写的软件，而是由可能出错的模型提出、受更好规格说明约束，并由不在乎模型听起来多么自信的系统进行检查的软件。