Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
Albert Q. Jiang1,2, Sean Welleck3,4,† Jin Peng Zhou5,6,† \ANDWenda Li2 Jiacheng Liu3 Mateja Jamnik2\ANDTimothée Lacroix1 Yuhuai Wu5,7, Guillaume Lample1,‡ \AND1Meta AI 2University of Cambridge 3University of Washington 4Allen Institute for AI 5Google Research 6Cornell University 7Stanford University Equal contributions as leading authors. Correspondence to: contributions as senior authors.
Abstract
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.
中文速览
把数学竞赛题的非正式证明（informal proof）自动转化为机器可验证的形式化证明（formal proof），一直是个难题，因为正式的形式化语料极为稀缺、门槛极高。研究者提出了"起草—素描—证明"（Draft, Sketch, and Prove，DSP）三步流程：先获取或用大语言模型生成非正式证明，再让大语言模型将其翻译成保留关键推理骨架、省略低层细节的形式化"证明草图"（formal proof sketch），最后用自动定理证明器（Sledgehammer）补全草图中留空的子目标，从而得到完整的可验证证明。在数学竞赛题基准集 miniF2F 上，这一方法将自动证明的成功率从 20.9% 大幅提升至约 39%，无论是人类撰写的非正式证明还是模型自动生成的都能带来显著增益。这项工作的重要意义在于，它首次系统地把海量非正式数学知识与形式化验证体系打通，为弥补形式化数据稀缺、提高数学推理可靠性提供了一条可行路径。
原文 arXiv:2210.12283;中英对照 + 大白话阅读 https://aha.fim.ai/paper/2210.12283v3