Synth Daily

Claude有时也能“实锤”

Favicon   ·  

Anthropic 的 AI 编码代理 Claude Code 在交互式定理证明（ITP）方面展现出惊人的能力，尽管它并非为此专门设计。目前，它仍需人类“项目经理”的指导，并且效率低于专家。但它能独立完成复杂的证明步骤，预示着一个未来：形式化方法将变得更加普及和自动化，AI 将可能改变整个领域，使过去只有少数专家才能完成的工作变得大众化。

交互式定理证明（ITP）为何如此困难？

交互式定理证明工具（如 Lean）功能强大，可用于验证操作系统、编译器等关键系统，但使用起来极为困难。即使是专家也觉得这个过程耗时且容易出错。

  • 认知要求高： ITP 需要同时具备多种能力，包括抽象数学思维、处理复杂约束的意愿，以及大多数人难以忍受的、对细节的极度较真。
  • 工具不友好： 传统的 ITP 工具界面混乱、文档稀少、错误信息难以理解。尽管 Lean 等工具正在快速改进，但学习曲线依然陡峭。

我很少像刚开始使用 Coq 的那几周一样，感到如此愚蠢和沮丧。

过去，完成复杂的 ITP 证明主要依赖于“痛苦的研究生集群”（Proof Search by Miserable Graduate Students）——由极少数顶尖人才通过数年枯燥乏味的工作，逐个攻克定理。这种高昂的成本严重限制了 ITP 的应用范围。

定理证明远不止是“证明定理”

实际工作中的定理证明更像是 “证明工程”（proof engineering），它涉及一系列相互关联的任务，而不仅仅是证明单个定理。专门为证明定理而设计的 AI 模型帮助不大，因为真正的工作流程包括：

  • 概念数学： 思考理论需要哪些概念和定理。
  • 映射到 Lean： 将概念转换为 Lean 的语法和类型。
  • 分解定理： 将大的性质分解为更小、更易于管理的部分。
  • 证明定理： 使用 Lean 的策略语言来证明单个定理。
  • 调试失败： 找出形式化被 Lean 拒绝的原因。

这些任务之间常常相互影响。例如，在证明一个定理时发现它不成立，可能需要回溯修改之前选择的数据类型，并重构整个形式化方案。最令人沮丧的经历往往不是证明本身，而是之前的某个决策意外地造成了阻碍。

Claude Code 是什么？

Claude Code 是一个 AI 编码代理，与一次性问答的聊天机器人不同，它可以将一个复杂请求分解为多个子任务并依次执行。这对于软件工程类的任务尤其有用。

例如，当你要求它修复一个无法证明的定理时，它可能会执行以下步骤：

  1. 为自己创建一个任务清单。
  2. 在代码库中搜索相关文件。
  3. 阅读定理的上下文。
  4. 运行构建命令以确认错误。
  5. 查找并阅读相关类型的定义。
  6. 思考可能的解决方案。
  7. 提出修复方案并请求用户许可。
  8. 重新运行构建以检查修复是否成功。

这个过程的关键在于，像 Lean 这样的严格工具能为 AI 提供详细的反馈。AI 犯错后，可以通过分析错误信息来自我纠正。这表明，为 AI 设计的工具可能需要更严格的规则和更丰富的错误反馈，而不是像为人类设计那样尽量避免失败。

Claude Code 的实际表现

作者使用 Claude Code 对一篇 15 年前的旧论文进行 Lean 形式化。他扮演“项目经理”的角色，指导 Claude 完成工作，自己几乎不编写任何 Lean 代码。

结果令人惊讶：该项目成功推进了约 50%，生成了 2,535 行 Lean 代码，其中约 1,232 行为证明代码。Claude Code 能够处理“证明工程”中的所有不同层级任务，甚至完成了复杂的重构工作。

但并非一帆风顺

一个致命的警告是：使用 AI 进行形式化的速度远慢于作者自己手动完成。作者的体验分为几种情况：

  • 奇迹（罕见）： AI 一次性正确完成了复杂的任务。
  • 缓慢进展（中位数）： AI 方向正确，但需要多次迭代和人类指导才能完成。
  • 原地打转（常见）： AI 卡在某个错误上，反复尝试相似的无效策略。
  • 浅层持续性错误（较少见）： AI 犯了简单的错误（如解析错误）且无法自行修复。
  • 深层持续性错误（罕见但致命）： AI 犯了概念性错误，但代码本身没有报错。这种错误难以发现，因为 AI 会将错误的理解写入注释，并在后续工作中信以为真，导致修复成本极高。

正是这些罕见但代价高昂的深层错误，导致整个项目耗时比手动操作更长。此外，对于 AI 生成的定义部分，其正确性也缺乏足够信心，需要繁琐的人工审计。

真正的惊喜与未来展望

Claude Code 的成功令人震惊，因为它并非为定理证明而设计。它的能力似乎源于其在代理能力、长期规划、任务分解和软件工程等相关领域的综合实力。

就在去年，如果你想用 Lean 形式化一篇论文，你的选择只有：(1) 去读研究生并自学，(2) 希望少数专家对你的问题感兴趣，或者 (3) 放弃。根本不存在一个 AI 正在取代的次优工具；这种能力在以前根本不存在。

尽管目前的 AI 代理还无法完全自主地完成长任务，但其能力正随着模型迭代而迅速提升。即使 AI 的智能水平不再提高，仅仅是提升运行速度就能让它变得更有用，因为当前管理 AI 的过程充满了等待的无效时间。

“苦涩的教训”（the bitter lesson）正在降临形式化方法领域。就像在图像识别和语言翻译中发生的那样，由通用 AI 驱动的、没有特定领域知识的工具，可能会让许多我们当前推崇的、巧妙而细致的工作变得过时。但这或许是值得的，因为它指向一个 定理证明被彻底解决 的未来——廉价、充足且自动化。