Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs

By Albert Qiaochu Jiang, Sean Welleck, J. Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, Guillaume Lample. 2022

338 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Information Systems, Natural Language Processing, Prompting & Reasoning

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Information Systems

In Natural Language Processing

In Prompting & Reasoning

Citations in the corpus

Llemma: An Open Language Model For Mathematics (2023, methodology): “Due to high computational costs of search, language models applied to this domain have traditionally been small, but recent work has demonstrated promise in the use of larger models (First et al., 2023; Jiang et al., 2023).”
DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models (2024, methodology): “• Formal Mathematics : We evaluate DeepSeekMath-Base using the informal-to-formal theorem proving task from (Jiang et al., 2022) on miniF2F (Zheng et al., 2021) with Isabelle (Wenzel et al., 2008) chosen to be the proof assistant.”
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023, methodology): “In Jiang et al. [2022b], the authors demonstrate a method for autoformalizing proofs in Isabelle.”
Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning (2023, background): “However, they have demonstrated a notable ability to comprehend textual inputs and translate them into formal programs, such as mathematical equations (He-Yueya et al., 2023) or Python codes (Gao et al., 2023).”
CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquing (2023, neutral): “, 2022), use mathematical prover to prove mathematical theory (Jiang et al., 2023), or use multiple tools automatically (Schick et al.”
OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problems (2024, background): “…across various tasks such as text generation (Zhao et al., 2023), code generation (Zan et al., 2023) and mathematical reasoning (Lu et al., 2023; Zhou et al., 2023), gar-nering significant attention from both academia and industry (Wei et al., 2022; Zhao et al., 2023; Bubeck et al., 2023).”
Large Language Models (2023, methodology): “A system which uses hierarchical planning for mathematical theorem proving was developed in [62].”
Parsel: A Unified Natural Language Framework for Algorithmic Reasoning (2022, background): “In addition, Jiang et al. (2022) proposed a framework to generate formal proofs in formal theorem-proving languages from informal proofs by ﬁrst generating an intermediate natural language proof sketch.”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, background): “Finally, MiniF2F is available in multiple proof assistants [18, 69, 70].”
A Survey of Deep Learning for Mathematical Reasoning (2022, positive): “Jiang et al. (2022a) explore translating provided (or generated) informal proofs into formal proofs.”
Faith and Fate: Limits of Transformers on Compositionality (2023, background): “[29] Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu.”
Baldur: Whole-Proof Generation and Repair with Large Language Models (2023, methodology): “The Draft, Sketch, and Prove method (DSP) [39] presents a hybrid between theorem proving and autoformalization, which, similar to our approach, makes use of LLMs for theorem proving.”
A Survey of Large Language Models (2023, positive): “To tackle it, several studies utilize LLMs to convert informal statements into formal proofs for augmenting new data [144] or generate drafts and proof sketches to reduce the search space of the proofs [373].”