形式化证明专家审查案例：自动补全并非最难环节
速览
本文通过格罗滕迪克消失定理的半自动形式化案例，探讨大语言模型在交互式定理证明器中的实际表现。尽管初始版本无错误，但专家审查揭示了定义、定理通用性及API设计等严重问题。研究表明，智能体虽能良好适应局部机械反馈，但在高层架构设计上仍显薄弱，形式化质量应以专家审查结果而非仅有无错误来评估。
AI 深度解读
Sorries Are Not最难的部分：半自动形式化验证的专家审查案例研究
背景
在计算机科学与人工智能的交叉领域，交互式定理证明器（Interactive Theorem Provers, ITPs）如 Lean、Coq 和 Isabelle 等，已成为构建数学和软件形式化验证库的核心工具。近年来，大型语言模型（LLMs）在辅助形式化验证方面展现出巨大潜力，特别是在填补证明间隙（proof gaps）方面。
然而，学术界和工业界逐渐意识到一个关键区别：一个能够编译通过且没有 sorry（占位符/未证明项）的定理，并不等同于一个可复用的高质量库贡献。 sorry 在 Lean 等系统中通常表示“此处假设成立，跳过证明”，虽然现代 LLM 能有效地消除这些占位符，但这仅解决了“可证明性”问题，并未解决“可维护性”、“通用性”和“工程规范性”问题。
本文基于 arXiv 上的一篇最新研究（提交于 2026 年 6 月 11 日），通过一个具体的案例研究——格罗滕迪克消失定理（Grothendieck's vanishing theorem）的半自动形式化，深入探讨了这一区别。研究旨在回答：当 AI 生成的形式化代码通过机器检查后，它是否真的达到了人类专家可接受的专业标准？
核心内容
本研究以格罗滕迪克消失定理的形式化为切入点，详细记录并分析了从“AI 初始生成”到“专家审查与重构”的全过程。
1. 初始阶段：看似完美的“零 Sorry”版本
研究团队首先利用半自动化工具链生成了格罗滕迪克消失定理的形式化版本。初步结果显示，该版本在编译器中能够成功编译，且内部不包含任何 sorry 占位符。从机器验证的角度看，这是一个“完成”的工作。
2. 专家审查：暴露深层缺陷
随后，研究团队邀请领域专家对该版本进行严格审查。尽管证明逻辑在技术上是正确的，但专家指出了四个严重问题，这些问题是仅靠 sorry 计数无法发现的：
- 定义问题（Definitions）： 关键数学概念的定义过于具体或冗余，缺乏抽象性，导致难以在其他上下文中复用。
- 定理通用性（Theorem Generality）： 定理的表述过于狭窄，限制了其在更广泛数学场景中的应用价值。
- 文件组织（File Organization）： 代码结构混乱，模块划分不合理，增加了阅读和维护成本。
- API 设计（API）： 暴露给用户的接口设计不佳，不符合形式化库的最佳实践，阻碍了其他开发者的使用。
3. 重构与压缩：基于审查的迭代
针对专家反馈，团队执行了“审查驱动的重构与压缩”流程。这一过程不仅仅是修复错误，更是对代码结构、定义抽象层级和接口设计的全面优化。重构后的版本再次接受了专家审查。
4. 前后对比：AI 的强项与弱项
通过对比审查前后的版本，研究揭示了当前 AI 在形式化验证中的能力边界：
- 强项： AI 代理（Agents）非常擅长处理局部的、机械可检查的反馈。例如，修复语法错误、补全证明步骤或调整局部逻辑，这些任务具有明确的对错标准，AI 表现良好。
- 弱项： AI 在定义的选择和API 的设计上依然表现薄弱。这些任务需要宏观的架构思维、对数学本质的深刻理解以及对未来复用场景的预判，目前 AI 难以胜任。
关键要点
- 可编译 $\neq$ 可用： 消除
sorry只是形式化验证的第一步。一个没有sorry的定理如果定义糟糕、结构混乱，在工程上等同于废品。 - 专家审查的必要性： 自动化工具无法替代人类专家对代码质量、抽象层次和库整体架构的评估。专家审查是确保形式化成果具备“库级”质量的关键环节。
- AI 的能力边界：
- 擅长： 局部逻辑补全、机械性错误修复、证明间隙填补。
- 不擅长： 宏观架构设计、定义抽象、API 规范化、代码可维护性优化。
- 评估标准的转变： 研究主张，对自动形式化（Autoformalization）的评估不应仅局限于“是否闭合了所有
sorry”，而应引入“是否通过了专家审查”作为核心指标。 - 半自动化的价值： 尽管 AI 在顶层设计上有缺陷，但“AI 生成初稿 + 专家审查 + 人工/半自动重构”的协作模式，显著提升了形式化工作的效率和质量。
意义与影响
这项研究对形式化验证和 AI 辅助软件工程领域具有深远影响：
- 重新定义成功标准： 它挑战了当前以“证明覆盖率”或“
sorry数量”为主要指标的评估体系，推动社区关注形式化代码的长期可维护性和复用价值。 - 指导 AI 工具开发： 对于开发形式化 AI 助手的研究者而言，这意味着未来的改进方向不应仅集中在证明生成能力上，更需加强代码重构、抽象推理和架构设计能力。
- 促进人机协作范式： 研究证实了“人类专家主导架构，AI 执行细节”的半自动化模式的有效性。这种模式既利用了 AI 的效率，又保留了人类在高层设计上的判断力，是当前技术条件下最可行的路径。
- 提升库建设质量： 随着数学和软件形式化库的日益庞大，代码质量直接影响整个生态系统的稳定性。引入专家审查机制，有助于构建更健壮、更标准化的形式化库，降低后续开发者的使用门槛。
总之，sorry 的消除只是形式化验证的“及格线”，而通过专家审查、具备良好设计和可复用性，才是迈向“卓越”的关键一步。