Lean 证明自动化已经到来。难点只是换了地方

7 月 26 日，Adam Langley 介绍了如何使用大语言模型验证一个可用的 Zstandard 解码器，Lean 证明自动化由此跨过了一条重要门槛。这个成果并非基准测试中的定理，也不是经过精心打磨的厂商演示，而是一个普通的软件项目：其中包含复杂的不变量、生成的证明，以及能够拒绝错误答案的编译器。

这种组合改变了关于 AI 可靠性的常见讨论。语言模型依然可能产生幻觉、误解需求，或生成无效语法。然而，Lean 会通过一个小型验证内核检查最终证明，因此信心并不依赖于对模型文字表述的信任。

因此，真正的较量并不是 AI 生成的代码与人类编写的代码之间的较量，而是未经检查的生成与机器检查的生成之间的较量。对知识工作者而言，这一区别指向了一种更广泛的模式：AI 创建产物，而确定性系统验证那些关键主张。

Langley 的实验并不能证明形式化验证已经变得廉价、简单，或适用于所有生产系统。他没有发布该解码器，而且其性能结果并不理想。不过，这项实验提供了一个具体信号：验证的经济性正在发生变化。

一个 Zstandard 解码器成为证明自动化测试

Langley 的实验之所以重要，是因为 LLM 在可识别的软件实现中处理了证明义务，而不只是解决孤立的数学练习。

Langley 是知名的安全工程师，以密码学和互联网协议领域的工作著称；他用 Lean 构建了一个 Zstandard 解压器。Lean 既是一门函数式编程语言，也是一种基于依赖类型理论的交互式定理证明器。

依赖类型能让程序的类型表达有关特定值的事实。例如，一个函数可以返回一个数组，其类型记录该数组的确切长度。另一个函数则可以要求提供索引位于数组范围内的证明，Lean 才允许访问。

这些保证能够编码传统软件通常只写在注释、测试或开发者记忆中的假设。官方 Lean reference 描述了一个小型内核：其他工具生成证明项后，由该内核进行检查。生成与检查之间的这种分离，是这个故事的核心。

Langley 选择了通常被称为 zstd 的 Zstandard 作为测试对象。Zstd 是一种无损压缩格式，其内部复杂度足以让验证具有意义。它将 LZ77 风格的匹配与 Huffman 编码及有限状态熵（FSE）结合使用。

该格式公开的 compression specification 定义了帧、块、熵表、序列码及解码行为。其 FSE 部分描述了状态表，而这些状态表的构建必须在各种可能输入下保持多种关系。

常规实现可以针对已知输出测试选定的表。Langley 的 Lean 版本还可以对表构建函数陈述普遍性质。这些性质包括表的必需大小、符号计数，以及表项转换的有效性。

这正是 LLM 的贡献变得重要的地方。根据 Langley 的 proof automation account，多个模型在大约 20 分钟内生成了相关证明。他表示，这项工作只消耗了标准月度订阅额度中的一小部分。

这些模型没有留下 Lean 在开发期间常用的逃生出口 sorry，它允许暂时接受未完成的证明。Langley 表示，他确认这些证明通过了类型检查，且不含此类缺口。

这并不能独立验证有关该解码器的每一项主张。Langley 没有发布其源代码，因此外部审阅者无法复现该项目或检查其完整规范。他的报告仍是一项第一人称实验，而非同行评审的评估。

不过，所声称的验证步骤与普通聊天机器人的回答具有不同地位。如果 Lean 的内核接受了一个针对正确表述定理的证明，就无需信任模型的私有推理过程。检查器会评估最终的形式化对象。

这是证明无关性在实践中的体现。对于许多命题，软件最终需要的是有效证明，而不是对发现证明过程的优雅解释。只要内核接受，一个笨拙的机器生成证明同样可以认证该定理。

该解码器也暴露了证明程序与打造优秀产品之间的边界。Langley 报告称，他的实现运行速度约为命令行 zstd 实现的十分之一。验证并不会自动带来生产级性能、可维护性或完整的格式覆盖。

这项有价值的结果更为有限。一名开发者使用通用 LLM，在一个并不简单的程序中完成了复杂的证明义务。实验表明，曾经是主导成本的证明劳动，正越来越可能成为机器生成的工作。

为什么 Lean 证明自动化改变了成本方程

Lean 证明自动化并未消除形式化验证的成本，但它冲击了使这些成本令普通软件团队难以接受的劳动类别。

形式化验证长期以来提供了测试无法提供的能力。测试检查的是选定的执行过程，而形式化证明可以在其模型覆盖的所有情形下确立某项已声明的性质。

这种区别在高保证系统中带来了显著成果。seL4 微内核拥有机器检查的证明，可在受支持配置上将规范与经验证的实现连接起来。其项目文档称，自 2009 年完成该证明以来，已验证代码中未发现功能正确性缺陷。

同一份 seL4 evidence 也说明了形式化方法为何始终较为专门化。其验证工作涉及大量规范、证明脚本、辅助工具和专家劳动。Langley 引用的一项回顾性估计显示，证明工作耗费的精力约为设计和实现工作的十倍。

他还指出，证明代码的规模超过 C 实现的二十倍。确切比例会因项目和验证目标而异。但更广泛的结论依然明确：更强的保证在历史上意味着需要大量第二层技术工作。

这种工作并不像传统编程。工程师必须将非正式需求转化为精确陈述，把困难目标拆分为可管理的引理，并引导证明系统完成缺失步骤。微小的代码改动也可能迫使人们大规模修复证明。

自动化求解器已经减轻了其中一部分负担。诸如 F* 的系统可以将合适的义务交给可满足性模理论求解器，后者会在受支持的逻辑理论中搜索证明。不过，面对复杂目标时，求解器的行为可能变得难以预测。

有经验的用户往往会学习如何表述定义，才能让自动化成功。这种专业能力仍然很有价值，但它会将精力转向迁就求解器。一个小小的建模选择，就可能让快速得出的结果变成消耗大量时间的搜索。

LLM 提供了另一种自动化形式。它们可以读取本地定义、理解编译器错误、提出引理、重写代码，并尝试另一种证明策略。它们并不要求每项义务都适配固定的判定过程。

研究已经显示，将生成与形式化检查器配对的重要性。一种编译器引导系统在 APOLLO paper 中有所描述：它利用 Lean 的反馈修复生成的证明，并隔离失败的子问题。其报告结果表明，迭代验证可以优于无引导采样。

Langley 的项目让这一模式更接近日常软件工程。模型不再只是解决为基准测试挑选的定理，而是面对由解析字节、构建解码表和强制数组边界所产生的证明义务。

这种差异对采用至关重要。大多数组织不会雇用数学家来证明竞赛题目，但会雇用工程师维护解析器、授权规则、财务计算、同步逻辑和数据转换。

这些系统包含无数团队已经视为不变量的陈述。一个请求属于已认证账户。发票的行项目与总额相符。解析器绝不会读到缓冲区之外。一个工作流不能批准其自身受限的操作。

团队目前通过类型、测试、评审、监控和运营控制的组合来保护这些陈述。每种方法都能捕捉重要故障，但每种方法都留有缺口。需求变化时，这些假设也会发生漂移。

Lean 证明自动化提供了一条路径，可让选定假设变得可执行、可检查。LLM 承担部分转化和证明劳动，Lean 则阻止不符合形式化规范的产物。

这种安排也改变了 AI 置信度的角色。传统编码助手可能在审阅有限上下文窗口后声称某个解析器是安全的。能够生成证明的助手则必须提供一个产物，让 Lean 针对明确主张予以接受。

模型可以保持概率性，因为验收闸门是确定性的。这种架构比任何单一模型的基准分数都更重要。更好的模型会提高速度和覆盖范围，而检查器则守住信任边界。

对组织而言，经济问题变得更具体。团队不再需要问每位工程师是否都应成为证明专家，而可以问哪些代价高昂的故障值得使用形式化陈述和 AI 辅助证明。

这条更窄的采用路径类似于静态类型、自动化测试和持续集成的普及。这些实践并未消除缺陷，却让某些检查的成本低到足以在日常开发中运行，而非只在例外审计时进行。

新对手是未经检查的生成

核心冲突并不在于人类还是模型能写出更好的代码，而在于生成的工作是否面对可靠的验收测试。

大多数生成式 AI 工具运行在验证较弱的领域。模型起草报告、总结会议、提出预测或编辑政策。产出往往在任何人知道其是否正确之前，就已经显得可信。

人工审查仍是默认防线。然而，审查者同样面临促使人们采用自动化的时间压力。一份流畅的草稿可能隐藏着缺失的来源、颠倒的条件或缺乏支持的结论。

软件比大多数知识工作提供更多自动化反馈。编译器会拒绝语法和类型错误。测试套件会运行已知案例。Linter 会识别选定模式。生产监控会揭示逃过先前关卡的故障。

这些机制通常都无法证明广泛的语义主张。通过测试不能确立每个有效压缩流都会保持在数组边界内。类型检查器也无法强制这一性质，除非相关关系出现在类型系统中。

Lean 改变了这一契约。开发者可以在程序类型中，或以定理形式，表达一项主张。随后，内核会检查所提供的证明是否能从已接受的假设中确立该确切主张。

LLM 不再是权威，而是候选证明的生成者。它可以反复失败，而不会削弱最终保证。失败的候选证明会在进入可信产物之前被拒绝。

这一模式的意义远不止于定理证明，值得广大知识工作者关注。许多专业产出本就包含可以依据结构化证据核查的断言。难点在于，将这些断言与仍需结合具体情境作出的判断区分开来。

以一位正在准备每周更新的产品经理为例。AI 助手可以通过一个可搜索的知识库，收集项目笔记、决策、客户反馈和交付指标。它起草叙述内容的速度，可以快过一个人回顾并还原这一周的工作。

不过，组织仍然需要设置关卡。每一条引用的客户陈述，都应对应一份录音或笔记。每一项已发布功能，都应对应一条已获接受的发布记录。每一个指标，都应包含其定义和报告周期。

就目前形式而言，这些并不是定理证明任务。但它们共享同一种架构：生成过程提出一个产物，独立系统则依据明确规则和证据核查其中的主张。

金融分析师可能要求，生成备忘录中的每个数字都能追溯到一份申报文件或获批准的数据集。研究人员可能要求，每条引文都必须支持其所在句子的表述。合规团队则可能把政策条件编码为可由机器检查的工作流。

形式语言为这类检查提高了上限。它们能够表达简单验证脚本难以清晰表述的关系。随后，LLM 可以帮助用户编写规范、衔接不同格式，并构造所需证据。

这带来了一种更有用的可信 AI 定义。信任并不来自要求模型保持谨慎，而是来自设计一套流程，使缺乏支持的工作无法跨越重要边界。

这种方法也明确了人类判断仍不可或缺的地方。Lean 检查的是某人写下的定理；它并不决定该定理是否准确涵盖用户的实际需求，或组织面临的全部风险。

一份被完美证明的规范，仍然可能规定了错误的行为。关于数组边界的定理，并不能证明一个解码器覆盖了生产服务所需的所有特性。安全证明也可能遗漏现实中的攻击者能力。

因此，AI 辅助验证将人类工作重心转向规范本身。人们必须决定哪些属性重要、哪些假设可以接受，以及证明覆盖的是哪个系统边界。

这种转变类似于电子表格对会计工作的影响。自动化减少了算术劳动，却提高了选择正确模型和输入的重要性。毫无瑕疵的计算，仍可能回答了错误的商业问题。

最强的团队不会把生成的证明当作装饰品。他们会以如今审查架构和安全边界时同样的严谨程度，审查定理陈述、假设与接口。

Zstandard 实验未能证明什么

经过检查的证明可以有效，但周边软件仍可能缓慢、不完整、规范不佳，或不适合投入生产。

最直接的限制是可复现性。Langley 没有发布其实现，因为他将其视为学习项目，而不是参考解码器。这一选择使得外部无法独立测试代码、证明结构和模型工作流。

因此，读者应将所报告的 20 分钟证明生成结果视为一份经验报告。它表明，这套工作流曾在一名熟练工程师的一个项目中奏效。它并不是通用性能测量。

模型在寻找证明时也修改了一些实现代码。Langley 曾使用 Id.run，这是 Lean 中一种可表达局部命令式计算的机制。他表示，这种写法使证明工具更难分析代码。

这一细节比一个一帆风顺的成功故事更具启示性。AI 证明自动化并非只是认证任意实现；它还推动了让程序更易于形式化推理的改动。

这类改动可能改善结构，但也可能扭曲工程优先级。开发者可能因为当前证明工具难以处理而避开高效的数据表示。他们也可能为了更快完成验证而接受更慢的代码。

据报道，Langley 的解码器运行速度约为成熟命令行实现的十分之一。这个差距并不否定证明的有效性。它表明，正确性、覆盖范围和性能仍是彼此独立的维度。

证明工程也并未消失。大型项目会组织引理和抽象，使证明能在代码变化后继续成立。如果 LLM 能以较低成本重新生成证明，某些维护策略的重要性会下降；另一些策略仍不可或缺，因为证明搜索本身可能变得昂贵。

关于证明状态快照的最新研究说明了这一基础设施问题。作者报告称，重复重建状态可能主导 Lean 自动搜索的成本。他们提出的复用机制，在选定基准上带来了显著加速。

这提醒我们，证明自动化依赖的不只是模型智能。它还需要快速的编译器反馈、依赖管理、相关引理检索、受控搜索和可复现环境。

规模带来了另一层不确定性。压缩解码器具有受约束的规范和易于识别的算法。企业系统则混合了数据库、网络、用户界面、外部服务、可变权限和不完整的业务规则。

将这些边界形式化的成本，可能高于证明局部函数。只有当身份数据、服务行为和部署配置符合模型假设时，有关授权规则的定理才有帮助。

非常强的类型也可能将变更扩散到整个程序。当一个数据结构新增不变量时，每个构造或转换它的函数都必须满足更强的要求。这种传播很有价值，但也可能增加迁移成本。

LLM 可以修复受影响的证明，但不一定能从代码中推断产品意图。重新生成的证明可能延续昨天的陈述，而业务实际上需要的是新的陈述。自动化使维护过时的正确性变得更容易。

工具链也存在安全问题。Lean 内核缩小了可信计算基，即为了信任证明而必须正确运行的软件范围。不过，构建系统、解析器、编译器和部署流水线仍然围绕着内核。

证明还依赖于已声明的假设和公理。团队需要制定政策，拒绝未完成的占位符、意外引入的公理，或针对错误依赖版本生成的证明。仅凭编辑器中的绿色状态提示，并不足以构成治理。

对非技术决策者而言，风险在于过度解读“证明”一词。形式验证是在明确假设下，建立某项已定义属性。它并不认证整体质量、伦理行为、可用性、法律合规性或商业价值。

这种精确性应被视为优势。团队可以准确检查证明了什么，以及哪些内容仍在边界之外。另一种选择往往是由零散测试和自信措辞支撑的宽泛保证声明。

因此，Langley 的成果作为方向性信号最具说服力。LLM 可以降低形式证明构建的劳动密集度。剩余瓶颈则转向规范、系统边界、性能与集成。

三个信号将表明证明自动化是否会普及

下一阶段取决于可复现的软件案例、具备证明意识的开发工具，以及经验证系统在真实变更后仍可维护的证据。

第一个信号，是发布围绕 AI 生成 Lean 证明构建的完整、常规软件项目。基准测试仍然有用，但无法捕捉需求演变、依赖升级、性能调优或生产环境调试。

一个有说服力的项目应公开其源代码、定理陈述、提示词或代理工作流、模型版本、证明检查命令和局限性。独立团队应能够在不信任托管模型的情况下，复现被接受的证明。

如果解析器、密码学代码、金融逻辑和协议实现等领域出现多个项目，Langley 的结论将更有分量。如果案例仍然很小或未公开，常规采用的理由就会减弱。

第二个信号，是融入主流开发工作流。证明自动化需要更像代码审查、持续集成或编辑器的类型检查器，而不是一个研究环境。

重要功能将包括从本地库中可靠检索、短反馈循环、可解释的失败原因，以及对未完成假设的严格检测。团队还需要可进行版本管理的证明产物，以便与代码变更一同审查。

工具应突出显示被证明陈述的变化，而不只是证明主体的变化。一个悄然弱化定理的模型，可能把艰难的失败变成误导性的成功。审查界面必须让这种操作一目了然。

组织还应关注供应商如何将非正式需求连接到形式陈述。生成证明只是工作流的一半。系统必须保留从人类决策到机器检查属性的可追溯性。

这正是知识管理成为运营基础设施的地方。在助手能够负责任地形式化之前，需求、决策、例外情况和源证据需要具备持久的上下文。一个个人知识系统可以支持这种上下文，尽管正式验收仍需要专门的验证工具。

第三个信号，是发生重大变更后的维护成本。一次性证明或许能打动审查者，却可能在下一次发布时成为负担。更相关的指标是：团队修改行为后，恢复已验证状态的速度有多快。

研究人员和工程团队应发布面向变更的评估。他们应修改数据结构、加强规范、替换算法并升级依赖项，然后衡量人工投入、模型尝试次数、检查时间和性能回退。

如果 AI 能在保留经过明确审查的陈述的同时修复证明，形式方法就会更适配迭代式软件开发。如果每次变更都会触发失控搜索或大范围重写，采用范围仍将集中于高保障的细分领域。

知识工作者也应在自己的 AI 系统中观察同样的模式。持久的优势不会来自产出更多草稿，而会来自构建这样的验收关卡：在文档、政策、数据和团队变化时，它们仍然可靠。

Lean 证明自动化提供了一个异常清晰的例子，因为生成与验证承担着不同角色。LLM 可以富有创造力、前后不一，也偶尔出错；内核仍然要求有效的形式化产物。

这种设计并不能解决 AI 生成工作周围的所有问题。但它确立了一个更好的默认原则：让模型提出建议，让明确的系统进行检查，让人类拥有规范。

下一个更实际的问题，不是每个工作场所是否都应采用 Lean，而是哪些反复出现的主张值得得到比一段自信的文字或一次简单测试更严格的验证。找出一个代价高昂的假设，将其与证据关联起来，并思考在采取行动前，可以通过什么确定性关卡来检验它。这个练习会揭示 AI 能够在何处安全地加速工作，以及哪些地方仍完全依赖人工审查。Lean 证明自动化让目标更加清晰可见，但组织仍必须决定哪些主张值得被证明。