Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization

📄 arXiv: 2606.13925v1 📥 PDF

作者: Vasily Ilin, Brian Nugent

分类: cs.AI, math.AG

发布日期: 2026-06-11

💡 一句话要点

提出半自主形式化方法以解决定理验证中的可重用性问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 自动形式化 定理证明 专家评审 API设计 重构过程

📋 核心要点

  1. 核心问题：现有的自动形式化方法在生成可重用库贡献方面存在不足，尤其是在专家评审中常常暴露出问题。
  2. 方法要点：论文提出了一种半自主形式化的方法，通过专家评审反馈进行重构，提升形式化的质量和可用性。
  3. 实验或效果：经过重构后，形式化的质量显著提高，专家评审的反馈显示出明显的改进，尤其在定义和API设计方面。

📝 摘要（中文）

大型语言模型在交互式定理证明器中能够填补证明空白，但经过验证的定理并不等同于可重用的库贡献。本文通过对Grothendieck消失定理的半自主形式化进行详细案例研究，探讨了这一区别。初始版本没有错误，但专家评审发现定义、定理一般性、文件组织和API存在严重问题。经过评审驱动的重构和压缩过程后，进行第二次专家评审。前后对比显示，代理能够很好地适应局部、机械可检查的反馈，但在选择定义和设计API方面仍显不足。我们认为，自动形式化的评估不仅应关注错误数量，还应关注最终形式化是否能通过专家评审。

🔬 方法详解

问题定义：本文旨在解决大型语言模型在交互式定理证明器中生成的形式化定理缺乏可重用性的问题。现有方法在专家评审中常常暴露出定义不清晰和API设计不合理等痛点。

核心思路：论文的核心思路是通过专家评审反馈来驱动形式化的重构过程，以提高形式化的质量和可用性。这样的设计旨在确保最终的形式化不仅能通过机械检查，还能满足专家的要求。

技术框架：整体架构包括初始形式化生成、专家评审、重构与压缩、以及再次评审四个主要阶段。每个阶段都旨在逐步提高形式化的质量。

关键创新：最重要的技术创新在于将专家评审反馈系统地整合进形式化过程，强调了形式化不仅要关注错误数量，还要关注其在实际应用中的有效性。

关键设计：在重构过程中，特别关注了定义的选择和API的设计，确保这些元素能够更好地支持后续的使用和扩展。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，经过重构后的形式化在专家评审中表现出显著的改进，尤其是在定义的清晰度和API的设计上。具体而言，重构后的版本在专家评审中获得了更高的认可度，显示出形式化质量的提升。

🎯 应用场景

该研究的潜在应用领域包括数学定理的自动验证、形式化证明的教育工具以及软件开发中的形式化方法。其实际价值在于提高定理证明的可重用性和可靠性，未来可能对自动化推理和形式化验证领域产生深远影响。

📄 摘要（原文）

Large language models can often close proof gaps in interactive theorem provers, but a verified theorem is not the same thing as a reusable library contribution. We study this distinction through a detailed case study: a semi-autonomous formalization of Grothendieck's vanishing theorem. The initial version compiles with no sorries, but an expert review found serious problems in definitions, theorem generality, file organization, and the API. We then ran a review-driven refactor and compression process and obtained a second expert review. The before-and-after comparison shows a sharp split: agents adapted well to local, mechanically checkable feedback, but remained weak at choosing definitions and designing APIs. We argue that autoformalization should be evaluated not only by closed sorries, but by whether the resulting formalization survives expert review.