Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization
本文认为，成功的自动形式化必须通过专家对定义质量和 API 设计的评审来进行评估，而非仅仅通过是否存在未证明的缺口（“sorries”），并通过对格罗滕迪克消亡定理的案例研究证明，尽管 AI 智能体能够有效地进行局部机械式的修复，但在高层概念设计方面仍显乏力。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正在雇佣一名非常快、非常热心的学徒来为你盖房子。你给了他们蓝图（一个数学定理）和一本解释如何建造它的教科书。
学徒没日没夜地工作。他们铺设砖块、搭建框架、安装屋顶。当他们完成时，房子屹立不倒。检查员（计算机）说：“干得好！这座房子结构稳固。”
这篇论文讨论的是接下来会发生什么。
论文作者提出了这样一个问题：“仅仅因为房子立住了，它就是一座‘好房子’吗？其他人能住在里面吗？他们以后能轻松加盖二层吗，还是必须先把墙拆掉？
以下是他们实验的分解，使用了简单的类比：
实验：建造一座“数学之屋”
团队要求一个人工智能（大型语言模型）将一个复杂的数学定理——**格罗滕迪克消亡定理（Grothendieck's Vanishing Theorem）**进行形式化。你可以把这个定理想象成一个非常特定、高端的建筑挑战。
他们给了 AI：
- 目标（定理陈述）。
- 教科书式的证明（指令）。
- 一条规则：“你必须仅使用我们现有工具箱中已有的标准工具（数学库）。”
第一阶段：“通过”状态（状态 A）
AI 努力工作并生成了没有错误的程序代码。在数学软件的世界里，错误被称为“sorry”（意为“抱歉，我还无法证明这一点”）。AI 成功地将“sorry”的数量降到了零。
- 结果： 房子立起来了。计算机很满意。
- 问题： 一位人类专家建筑师（数学家）看着这座房子说：“这是一场灾难。”
专家评审：为什么“立着的房子”失败了
人类专家发现，虽然房子没有倒塌，但它建得非常糟糕。以下是他们发现的具体问题，已转化为日常用语：
1. “定制工具”问题（定义）
- AI 的做法： AI 针对每一个微小的任务都在发明自己的定制工具。如果它需要测量一面墙，它就会为那一面墙专门造一把奇特的卷尺。
- 为什么不好： 在一个真实的库（library）中，你希望使用大家都能理解的标准工具。如果 AI 为每项工作都造一个定制工具，未来的建造者就无法使用这座房子，因为他们不知道如何操作 AI 发明的那些奇怪玩意儿。
- 结论： AI 非常擅长“使用”工具，但非常不擅长“设计”工具。它创建了 62 个自定义定义，其中 61 个都是无用或令人困惑的。
2. “杂乱蓝图”问题（API 设计）
- AI 的做法： AI 没有构建一个简洁的接口（用户手册）。相反，它只是在有人想做某事时，不断地拆开墙壁展示里面的原始砖块。
- 修复方案： 专家要求 AI 构建一个“用户界面”（API），以便人们可以与数学进行交互，而不必看到混乱的内部构造。
- 结果： AI 确实构建了一个接口，但它很混乱。它为了当前的证明添加了 24 条特定的“规则”，而不是创建一些优雅、通用的规则。这就像是为每一个灯泡都安装了一个独特的、复杂的开关，而不是安装一个标准的灯开关。
3. “目光短浅”问题（定理陈述）
- AI 的做法： AI 只证明了完成当前任务所必需的内容，仅此而已。这就像一个木匠只根据当前的缝隙来切割木板，而不是切好一块以后可以用于其他缝隙的木板。
- 结论： AI 非常擅长解决眼前的谜题，但完全无法思考：“我如何让这件东西在五年后对别人有用？”
“前后对比”测试
团队并没有放弃。他们根据专家的反馈要求 AI 进行修复。
- AI 修复得好的地方： 它擅长局部修理。如果专家说“重命名这个文件”或“修改这个特定的数字”，它能完美完成。它可以清理混乱。
- AI 无法修复的地方： 它仍然无法弄明白如何从头开始设计一座好的房子。即使在评审之后，其定义仍然笨拙，其“用户界面”仍然臃肿。
核心教训
论文以一个简单而有力的观点结束：
“填补空白”（让代码编译通过）是容易的部分。
难点在于设计。
- AI 就像一个出色的砖匠： 如果你告诉它要把砖头放在哪里，它能把砖铺得完美无缺。
- AI 并不是建筑师： 它无法决定房子应该是什么样子的，房间该如何流动，或者未来的住户需要什么样的工具。
总结：
我们不应仅仅问：“AI 是否解决了这个数学问题？”我们需要问：“AI 是否构建了一个人类真正可以使用的东西？”
目前，AI 可以解开谜题，但它无法构建库（library）。要获得真正有用的结果，人类专家仍需介入，承担起设计和组织方面的大量工作。难点不在于证明定理，而在于确保这个证明是送给未来的礼物，而不是一个负担。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。