现有数学证明的形式化是一个众所周知的困难过程。尽管在自动化和证明助手方面进行了数十年的研究，编写形式化证明仍然艰巨且只有少数专家能够掌握。以往自动化形式化的研究侧重于强大的搜索算法，但没有人尝试利用现有的非形式化证明。在这项工作中，我们引入了 Draft, Sketch, and Prove (DSP)方法，该方法将非形式化证明映射为形式化证明草图，并利用这些草图通过将搜索引导到更简单的子问题来指导自动化证明器。我们研究了两种相关设置，其中非形式化证明由人类编写或由语言模型生成。我们的实验和消融研究表明，大型语言模型能够生成结构良好的形式化草图，这些草图遵循与非形式化证明相同的推理步骤。用这些草图指导自动化证明器，在一组数学竞赛问题上的性能从 20.9%提升到了 39.3%。
The formalization of existing mathematical proofs is a notoriously difficult process. Despite decades of research on automation and proof assistants, writing formal proofs remains arduous and only accessible to a few experts. While previous studies to automate formalization focused on powerful search algorithms, no attempts were made to take advantage of available informal proofs. In this work, we introduce Draft, Sketch, and Prove (DSP), a method that maps informal proofs to formal proof sketches, and uses the sketches to guide an automated prover by directing its search to easier sub-problems. We investigate two relevant setups where informal proofs are either written by humans or generated by a language model. Our experiments and ablation studies show that large language models are able to produce well-structured formal sketches that follow the same reasoning steps as the informal proofs. Guiding an automated prover with these sketches enhances its performance from 20.9% to 39.3% on a collection of mathematical competition problems.
核心贡献 · Key contributions
提出 Draft, Sketch, and Prove (DSP) 方法，将非形式证明映射为形式证明草图以引导自动证明器。 Introduces Draft, Sketch, and Prove (DSP), a method that maps informal proofs to formal proof sketches to guide automated provers.
证明大型语言模型能生成遵循非形式推理步骤的结构良好的形式草图。 Demonstrates that large language models can generate well-structured formal sketches following informal reasoning steps.
在 miniF2F 上使用 Isabelle 达到最先进性能，使用人类编写的证明将成功率从 20.9% 提升至 39.3%。 Achieves state-of-the-art performance on miniF2F with Isabelle, increasing success rate from 20.9% to 39.3% using human-written proofs.
表明语言模型生成的非形式证明在引导形式证明器方面几乎与人类编写的同样有效。 Shows that language-model-generated informal proofs are nearly as effective as human-written ones in guiding formal provers.
通过消融研究确认了草拟非形式证明、用注释标注草图以及使用自动证明器的重要性。 Provides ablation studies confirming the importance of drafting informal proofs, annotating sketches with comments, and using automated provers.
发布与 miniF2F 形式陈述对齐的非形式陈述和证明的精选数据集。 Releases a curated dataset of informal statements and proofs aligned with miniF2F formal statements.
局限 · Limitations
方法仅在 miniF2F 的高中竞赛问题上评估，限制了向高等数学的泛化能力。 Method is evaluated only on high-school competition problems in miniF2F, limiting generalizability to advanced mathematics.
依赖大型语言模型（如 Codex、Minerva），由于 API 成本可能无法访问或复现。 Relies on large language models (e.g., Codex, Minerva) which may not be accessible or reproducible due to API costs.
性能受限于自动证明器填补空白的能力；复杂猜想可能仍无法证明。 Performance is bounded by the automated prover's ability to fill gaps; complex conjectures may remain unprovable.
语言模型生成的非形式证明可能不正确，但仍能产生成功的形式证明，表明潜在不可靠性。 Informal proofs from language models can be incorrect, yet still lead to successful formal proofs, indicating potential unreliability.
该方法需要手动准备少量示例用于自动形式化，可能无法扩展到多样化领域。 The method requires manual preparation of few-shot examples for autoformalization, which may not scale to diverse domains.
论文章节 · Sections（共 19）
摘要Abstract
1 引言1 Introduction
2 背景与相关工作2 Background and Related Work
3 方法3 Method
3.1 起草非形式化证明3.1 Drafting informal proofs
3.2 将非形式化证明映射为形式化草图3.2 Mapping informal proofs into formal sketches
3.3 证明草图中的开放猜想3.3 Proving open conjectures in the sketches