Anthropic押注形式化验证规模化

Anthropic认为，形式化验证的成本拐点已经出现

Anthropic近日公布的一项研究显示，大语言模型正在让形式化软件验证首次具备大规模落地的可能。这里的形式化软件验证，是指把程序行为写成精确的数学规范，再由Lean等证明助手检查代码是否满足这些规范，而不是依靠有限数量的测试用例去推测程序“大概没有问题”。

这项进展的关键并不是Claude突然变成了不会犯错的数学家，而是LLM能够批量承担过去极其消耗人力的“形式化翻译”工作。开发者负责定义目标和约束，模型负责拆分任务、检索已有定理、补齐证明步骤、处理编译错误，最后由一个确定性的证明内核逐项验收。

Anthropic给出的判断相当明确：当LLM生成的证明可以被独立检查时，模型的不可靠性不再是不可逾越的障碍。普通代码生成依赖开发者阅读差异、运行测试和观察线上表现；形式化证明生成则多了一道更硬的门槛，证明助手只接受逻辑上成立且类型检查通过的结果，不会因为Claude的解释听起来合理就放行。

11天、60亿Token和1300万行代码

Anthropic此次披露的代表性实验，是用多智能体系统推进费马最后定理的完整形式化。费马最后定理早已由安德鲁·怀尔斯在20世纪90年代完成数学证明，但人类可读的论文证明与计算机可逐步检查的形式化证明并不是同一种交付物，后者必须把大量“显然成立”的跳步、依赖关系和边界条件全部展开。

实验最终持续约11天，消耗约60亿Token，并产生约1300万行Lean代码。这个数字首先证明了规模，而不是优雅：Claude能够用机器速度堆出庞大的可检查证明，但它距离人类数学家追求的简洁结构、可读性和可维护性仍有明显距离。

1300万行代码也是这项成果最值得警惕的数据。如此庞大的形式化产物即使能够通过Lean检查，也很难由人类逐行审阅；一旦定义、基础公理或顶层规范写错，后续证明越完整，只会越严格地证明一个错误命题。因此，形式化验证减少的是实现层面的不确定性，并不会自动消除需求和规范层面的错误。

Anthropic还披露了一个更接近日常可用性的对照实验：研究人员使用3个普通Claude Max个人订阅账号，在3天内完成了维诺格拉多夫三素数定理的形式化。这组数据比60亿Token的大项目更有现实意义，因为它说明多智能体形式化并不一定依赖专用超级计算集群，普通研究团队也可能复现较小规模的工作流。

Prove2Me解决的不是智力，而是工程调度

Prove2Me是一个面向大规模形式化任务的多智能体协作框架，它把复杂定理拆成有向无环图中的多个依赖节点，再让不同Claude智能体并行完成可以独立验证的子任务。单个Agent不需要一次记住整套证明，只需要处理当前节点、直接依赖和相关库信息。

这种设计处理了长周期Agent最常见的三个问题：上下文会溢出，失败会反复传播，多个Agent会重复造轮子。Prove2Me通过证明草图先规定“要证明什么”，再把“如何证明”分配给Agent；已经通过Lean检查的中间结论则进入可检索的成果库，供后续节点复用。

有向无环图是Prove2Me能够横向扩展的核心。有向无环图是一种不存在循环依赖的任务结构，上游证明完成后，下游任务才能启动；彼此独立的分支则可以同时交给数十个Agent。它更像持续集成系统中的构建图，而不是让一群聊天机器人在同一个窗口里轮流发言。

证明草图则把自然语言规划与机器证明分成两个层次。研究人员或高层Agent先描述定理结构、关键引理和预期依赖，执行Agent再把草图翻译成Lean能够检查的代码。这样做不能保证一次成功，却能把失败限定在单个节点内，避免整条证明链因为局部错误而推倒重来。

自然语言索引进一步降低了复用门槛。传统证明库要求使用者熟悉准确的定理名称、命名空间和类型签名，而LLM可以根据“我需要一个关于有限和交换次序的结论”去寻找可能匹配的已有结果，再交给Lean确认类型是否真正兼容。

Lean才是可信根，Claude不是

Lean是一个交互式定理证明器和函数式编程语言，其核心价值是用很小的可信内核检查证明项是否合法。在Anthropic展示的流程里，Claude负责提出候选证明，Lean负责作出接受或拒绝的最终决定，两者的角色不能倒置。

LLM与证明助手的组合，本质上把概率模型放在了搜索层，把确定性系统放在了验收层。Claude可以猜错定理、调用不存在的库函数，甚至生成语法正确但方向完全错误的证明；只要Lean内核、基础定义和信任边界没有被绕过，这些错误就无法伪装成已经完成的证明。

这种结构比“让模型写代码，再让模型审查代码”更可靠。两个LLM即使给出一致结论，也可能共享相同盲点；Lean不会理解Claude的语气和理由，只会根据形式规则重放证明。这相当于把代码审查从同行意见升级为可重复执行的逻辑检查。

| 方法 | 能回答的问题 | 覆盖范围 | 主要盲区 | 适合场景 | |---|---|---:|---|---| | 单元测试 | 给定输入是否得到预期输出 | 有限样例 | 未覆盖路径、错误测试预期 | 业务逻辑、快速回归 | | 模糊测试 | 随机或变异输入能否触发异常 | 大量输入样本 | 无法穷尽状态空间 | 解析器、协议、内存安全 | | 静态分析 | 代码是否违反预设规则 | 全代码扫描 | 误报、规则表达能力有限 | 常见缺陷、合规检查 | | 模型检查 | 有限状态系统是否满足性质 | 可枚举状态空间 | 状态爆炸 | 协议、并发状态机 | | 交互式形式化验证 | 程序是否满足数学规范 | 理论上覆盖全部输入 | 规范成本、证明成本、规范可能写错 | 密码学、内核、关键基础设施 | | LLM辅助形式化验证 | 能否自动生成并修复可检查证明 | 取决于拆分、算力和证明库 | 代码冗长、成本高、仍需人类定义规范 | 扩大形式化验证覆盖面 |

从数学证明走向软件验证，还差关键一步

数学定理形式化成功，并不等于任意大型软件都能立刻获得完整证明。数学任务通常拥有相对稳定的命题和公理体系，而真实软件会持续改需求、调用外部服务、依赖编译器和硬件，并包含网络超时、并发调度、权限配置等难以完全建模的因素。

软件形式化的第一道难题仍然是规范。模型可以证明排序函数输出的是一个有序序列，但开发者必须先准确说明元素是否允许重复、比较器是否满足传递性、异常输入如何处理，以及性能和内存是否属于需要证明的性质。规范遗漏的行为，不会因为证明通过而自动变正确。

软件形式化的第二道难题是信任链。一个完整结论通常同时依赖证明助手内核、编译器、运行时、硬件模型、第三方库和构建配置；如果证明针对的是抽象实现，生产环境运行的却是另一份经过优化或手工修改的代码，形式化保证就会在交付过程中断裂。

软件形式化的第三道难题是增量维护。一次性生成1300万行证明可以展示能力，但软件团队更关心修改20行代码之后需要重新证明多少内容、失败能否定位到具体提交、证明是否能在持续集成时间窗口内完成，以及后续工程师能否理解生成物。

因此，Anthropic成果更像是证明了“吞吐量可扩展”，还没有证明“软件工程成本已经足够低”。当Agent可以持续运行并并行搜索时，原先需要数月的人力工作可以压缩到数天；但60亿Token、复杂调度和巨量生成代码仍是一笔真实成本，不能仅用日历时间缩短来替代总资源核算。

最先受益的不会是普通Web应用

密码学实现、共识协议、编译器优化、芯片设计和安全关键基础设施最可能率先采用这套方法。这些领域的单次缺陷成本足够高，规范相对明确，已有形式化工具和证明库也更成熟，因此能够承受前期建模成本。

普通Web应用短期内不会全面转向Lean。电商页面、内部管理系统和营销工具的需求变化速度通常高于证明维护速度，单元测试、类型系统、静态分析和运行时监控仍然更符合投入产出比。LLM辅助形式化更现实的进入方式，是先验证权限模型、计费规则、数据一致性协议等少数不能出错的核心模块。

AI生成代码反而会提高形式化验证的价值。当Agent每天能够产生远超人类审查能力的代码量时，传统代码评审会成为瓶颈，而由另一个LLM给出“看起来没问题”的意见并不能建立可信度。可由小型内核机械检查的证明，提供了一条不依赖人工逐行阅读的验收路径。

这也解释了Anthropic为什么把形式化验证视为LLM时代的软件基础设施，而不只是数学演示。模型负责放大生产能力，验证器负责守住正确性底线；如果代码生成速度持续增长，测试覆盖率和人工审查却没有同步扩展，团队得到的只会是更快累积的技术风险。

这项突破真正改变了什么

Anthropic真正展示的是一种可扩展的“生成—验证—修复”闭环。Agent生成候选证明，Lean返回精确错误，Agent根据错误继续修改；通过的节点进入依赖图并被其他Agent复用。每个环节都可以并行，失败也有明确的机器反馈，不需要人类持续守在终端前纠正方向。

这套闭环可能重塑代码模型的评价标准。今天的编程模型主要比较基准题通过率、补全接受率和修复Issue的数量，未来更有价值的指标可能是：模型能否为关键代码同步生成规范、证明义务和可重放证明，以及代码变更后能否自动修复失效证明。

开发者的职责也不会因为自动证明而消失。人类需要决定哪些性质值得证明、抽象边界放在哪里、允许信任哪些组件，并审查规范是否对应真实业务意图；这些工作比补齐数千个机械证明步骤更接近软件工程的核心判断。

IBM此前对代码LLM的讨论指出，过度依赖自动生成可能造成基础能力和调试能力的“认知萎缩”。形式化验证提供了一部分制衡：开发者可以不逐行相信生成代码，但必须保留理解规范、识别错误假设和判断系统边界的能力，否则团队只会从“盲信代码”转向“盲信绿色对勾”。

判断：可行不等于普及，但门槛确实变了

Anthropic的结论值得重视，但“可行”与“经济可用”仍是两个阶段。11天完成过去可能需要多年协作的形式化工程，说明LLM已经显著压低劳动成本；60亿Token和1300万行代码则说明，这项技术距离轻量、优雅和普遍部署仍有距离。

这次进展最重要的不是Claude证明了一个著名定理，而是多智能体系统找到了一种可被确定性工具约束的工作方式。LLM不需要变得绝对可靠，只要它能快速提出候选方案，并把最终判断交给更可信的验证器，就可以在错误率不为零的情况下完成大规模工程。

未来两三年内，更现实的产品形态不会是给整个代码库按下“证明正确”按钮，而是把形式化验证嵌入代码托管和持续集成流程：高风险模块变更时自动生成证明义务，Agent并行修复失败节点，合并请求同时展示测试结果与机器证明状态。

Anthropic已经把问题从“LLM能不能写出证明”推进到了“组织能否用LLM持续维护证明”。前一个问题主要考验模型能力，后一个问题还取决于规范质量、工具链集成、增量构建、成本控制和团队治理；只有后者解决，形式化验证才会真正从研究项目进入主流软件生产。

参考来源

• IT之家：Claude仅用11天完成费马大定理首个完整计算机验证证明：介绍实验周期、形式化目标及Lean验证方式。
• Lean 4 GitHub仓库：Lean编程语言与定理证明器的官方开源实现，可用于核对其内核、语言及工具链设计。
• mathlib4 GitHub仓库：Lean 4的社区数学库，展示形式化证明如何组织、复用和接受持续集成检查。