用专家评审检验自动形式化，发现模型能补漏洞却不会设计好定义和接口。
Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization
- 通过半自动方式形式化格罗滕迪克消失定理，再经专家评审发现问题。
- 初版无遗漏（no sorries），但定义、通用性与接口设计均存严重缺陷。
- 适合关注自动化证明质量与可复用性的形式化研究者参考。
大型语言模型能有效填补交互式定理证明器中的证明空缺，但验证过的定理并不等于可复用的库贡献。我们通过一项详尽的案例研究探讨这一差异：半自动形式化格罗滕迪克消失定理。初始版本无遗漏（no sorries），但专家评审发现定义不当、定理泛化不足、文件组织混乱及接口设计不合理等问题。随后进行基于评审反馈的重构与压缩，再次获得专家评审。对比前后结果表明：智能体能良好适应局部、机械可验证的反馈，但在选择定义与设计接口方面仍表现薄弱。我们认为，自动形式化应不仅以是否闭合‘遗漏’（sorries）来评估，更需考察其成果能否通过专家评审。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。