Source-linked AI summary
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, Guillaume Lample
TL;DR
Formalizing existing mathematical proofs is difficult, while prior formalization methods do not capitalize on abundant informal proofs. DSP maps informal proofs into formal proof sketches and uses automated provers to fill their gaps, raising miniF2F success from 20.9% to 39.3% in the reported settings.
Problem
Formal proof writing is difficult and formal data is scarce, while existing automation has not leveraged the abundant body of informal mathematical proofs.
Method
DSP drafts or receives informal proofs, maps them into formal proof sketches that preserve high-level reasoning, and uses automated provers to close open conjectures.
Results
20.9% to 39.3%: DSP raises the proportion of miniF2F problems solved by an automated prover, reaching up to 39.3% with human-written informal proofs.
Takeaways & Limitations
Formal proof sketches that mirror informal reasoning can guide automated provers toward state-of-the-art miniF2F performance with Isabelle.
Takeaways & Limitations
The computational cost of the autoformalizer is a bottleneck, motivating more efficient generation of high-quality proof sketches.
Abstract
from arXiv · showhide
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.
1 INTRODUCTION
DSP addresses the scarcity of formal proof data by leveraging abundant informal proofs to guide formalization. It combines proof sketches with automated proving and improves miniF2F performance in both human- and model-generated proof settings.
- Motivation: Formal proof automation remains difficult because formalizing proofs is accessible to few experts and available formal corpora are scarce.The largest Isabelle corpus contains less than 0.6 GB, far smaller than common vision or language datasets.
- Approach: DSP translates informal mathematical proofs into formal proof sketches that guide automated provers.The approach targets the gap between abundant informal mathematics and logically rigorous formal systems.
- Evaluation: The evaluation uses manually curated informal statements and proofs aligned with formal statements in miniF2F.Experiments cover settings with either human-written proofs or language-model-generated proofs.
- Results: 20.9% to 38.9%: automated-prover success on miniF2F with language-model-generated informal proofs.The success rate reaches up to 39.3% when the informal proofs are written by humans.
- Ablations: Ablations show benefits from drafting informal proofs, annotating sketches with informal segments, and automatically closing open conjectures.These components are evaluated as contributors to proof autoformalization performance.
2 BACKGROUND AND RELATED WORK
Formal theorem provers provide kernel-checked mathematical verification, while machine-learning approaches seek to generate proof steps from formal states. Informal mathematical data offers a larger resource, but language models can produce plausible yet incorrect proofs that are difficult to detect automatically.
- Interactive theorem proving: Interactive theorem provers verify theorems against formal logical foundations implemented by their kernels.Formal proofs iteratively simplify stated theorems into subgoals until they reduce to previously proven facts.
- Machine learning for formal proof synthesis: Formal proof synthesis methods commonly use sequence-to-sequence models to generate the next proof step from the current formal proof state.These approaches combine machine learning with interactive theorem provers.
- Machine learning for informal reasoning: Informal mathematical data is abundant, but language models may generate correct answers with incorrect proofs.Such false positives are difficult to identify without human inspection.
- Autoformalization: Few-shot autoformalization studies show that language models can translate informal mathematical statements into formal statements using a small number of examples.Prior work established statement-level feasibility before DSP targets proof sketches.
3 METHOD
DSP drafts or receives an informal proof, maps it to a structured formal proof sketch, and uses automated provers to fill its remaining gaps. The sketch preserves high-level reasoning while leaving low-level details as open conjectures.
- Pipeline: DSP consists of drafting informal proofs, mapping them into formal sketches, and proving the sketches’ remaining conjectures.The pipeline assumes both an informal and a formal statement for each problem.
- 3.1 DRAFTING INFORMAL PROOFS: The drafting stage uses either a human-written ground-truth proof or language-model-generated proof candidates.The model-based setting can produce multiple alternative solutions when human proofs are unavailable.
- 3.1 DRAFTING INFORMAL PROOFS: Figure 2 illustrates the inequality example 10a ≤ 28a^2 + 1 as an informal proof paired with a formal sketch.The sketch rewrites the original statement as c0 and proves it through five intermediary conjectures, c1 through c5.
- 3.2 MAPPING INFORMAL PROOFS INTO FORMAL SKETCHES: A formal proof sketch preserves high-level solution structure while leaving low-level details for later automated proving.An autoformalizer uses few-shot informal-proof/formal-sketch pairs to generate the sketch.
- 3.3 PROVING OPEN CONJECTURES IN THE SKETCHES: Open conjectures in each sketch are passed to off-the-shelf automated provers that produce formally verifiable proofs.The final formal proof is accepted only when all gaps are closed and checked against the problem specification.
4 EXPERIMENTS
DSP evaluates informal-proof-guided formalization on miniF2F using Isabelle, comparing human and language-model drafts against proof-search baselines. The method combines sampled informal proofs, formal sketches, and automated completion of open conjectures.
- Dataset and evaluation: The evaluation uses miniF2F’s 488 competition problems, split evenly into validation and test sets, with Isabelle as the formal prover.Proofs count as valid only when Isabelle verifies the formal statement without cheating keywords.
- Drafting and sketching: DSP samples 100 informal proofs per problem from Codex and Minerva models, then autoformalizes them into formal sketches using few-shot demonstrations.The demonstrations cover algebra and number theory and exclude the problem being solved.
- Drafting and sketching: Open conjectures in each formal sketch are completed with Sledgehammer plus heuristics, producing proofs that Isabelle can verify.The automated prover runs on every open conjecture in the sketch.
- Baselines: 20.9% is the Sledgehammer-plus-heuristics test-set success rate, while Thor and Thor with expert iteration reach 29.9% and 35.2%, respectively.The heuristic prover improves Sledgehammer from 10.4% to 20.9% on miniF2F-test.
- Results: 39.3% is DSP’s test-set success rate with human-written informal proofs, compared with 37.7% for Minerva 62B and 38.9% for Minerva 540B.With human proofs, DSP solves 200 of 488 problems; Minerva 62B and 540B each solve 199.
5 ANALYSIS
The analysis tests DSP components, compares human and Minerva-generated informal proofs, and examines proof correctness, scaling, and memorization concerns. Ablations and case studies show that sketches, informal guidance, and automated proving each affect performance, while some flawed drafts can still support successful formal proofs.
- Ablation scaling: DSP reaches a plateau after 70 autoformalization attempts, whereas removing in-line comments plateaus around 50 attempts and solves 181 miniF2F problems.The no-informal-proofs ablation plateaus around 70 attempts and solves 178 problems.
- Ablation scaling: 154 problems are solved without formal proof sketches, compared with 181 without in-line comments and 178 without informal proofs.The comparison isolates the contribution of sketching from the other DSP components.
- Human versus Minerva proofs: Minerva-generated informal proofs solve one IMO problem that the human proof does not, possibly because human proofs leave gaps too difficult for automated provers.The successful example is imo 1959 1, shown with its formal proof in Figure 4.
- Informal-proof correctness: Among 50 Minerva proofs converted successfully to formal proofs, 29 are entirely correct, 16 contain an identifiable incorrect step, and 5 are nonsensical.Thus, successful formalization does not require every informal draft to be correct.
- Informal-proof correctness: Of 21 incorrect informal proofs, automated proving ignores 13, while autoformalization corrects errors in the other 8 cases.This analysis examines how flawed drafts can still guide successful formal proofs.
- Detecting correct drafts: Filtering out problems solvable directly by the automated prover identifies correct Minerva proofs with 77.8% precision and 72.4% recall.The filtered set contains 27 proofs: 21 completely correct and 6 with small errors.
6 CONCLUSION
DSP synthesizes formal proofs by using proof sketches that mirror informal reasoning, while differing from prior work in its use of informal proofs and whole-structure construction. The authors identify symbolic proving and autoformalization cost as important boundaries for future expansion.
- Conclusion: DSP uses formal proof sketches that mirror the high-level reasoning structures of informal proofs.The automated prover fills the gaps between intermediate conjectures.
- Conclusion: Unlike prior approaches focused on proof search, DSP constructs the entire formal proof structure from an informal proof in one decoding operation.This simplifies the prover’s task to filling gaps between intermediate conjectures.
- Conclusion: DSP benefits from informal proofs rather than operating exclusively on formal data.This distinguishes its data source from existing approaches to formal proof synthesis.
- Conclusion: The current system uses a purely symbolic automated prover to close proof-sketch gaps.The authors plan to investigate more powerful mechanisms to broaden the scope of provable theorems.
- Conclusion: The autoformalizer’s computational cost is a bottleneck, motivating more efficient generation of high-quality proof sketches.The authors also report that the number of generations is crucial for performance.
CODE AND DETAILED RESULTS
The experiment-reproduction code and additional main-experiment result details are available in the project repository.
- Code and detailed results: The code for reproducing the experiments is available at github.com/albertqjiang/draft sketch prove.The repository is identified as the location for experiment-reproduction materials.
- Code and detailed results: Additional result details for the main experiments are available in the same repository.The passage directs readers to the repository for expanded results.
- Code and detailed results: The repository serves both experiment reproduction and access to further main-experiment results.Both resources are explicitly located in the same project repository.
FUNDING DISCLOSURE
The paper reports ERC Advanced Grant ALEXANDRIA support for AQJ and WL, with additional Peterhouse Graduate Studentship support for AQJ.
- Funding disclosure: AQJ and WL are supported by the ERC Advanced Grant ALEXANDRIA.The grant is identified as Project GA 742178.
- Funding disclosure: AQJ is additionally supported by a Peterhouse Graduate Studentship.This support is reported separately from the ERC grant.
- Funding disclosure: The funding disclosure names both grant support and an additional studentship for AQJ.WL is named only in connection with the ERC Advanced Grant ALEXANDRIA.
LIST OF CONTRIBUTIONS
The contributions cover idea conception, pipeline construction, autoformalization, informal proofs, alignment improvements, case analyses, dataset work, experiments, and writing.
- List of contributions: AQJ conceived the proof-sketch idea and conducted the experiments.WL contributed to writing the final autoformalization work.
- List of contributions: SW constructed the first pipeline version and initial autoformalization prompts.JPZ produced the Minerva informal proofs and helped conduct autoformalization experiments.
- List of contributions: GL proposed inline comments in formal proof sketches to improve alignment.JPZ, YW, and SW performed case analyses of Minerva solutions.
- List of contributions: AQJ, TL, GL, SW, and JL contributed to the dataset.The passage attributes dataset construction to this group.
- List of contributions: The authors collectively distributed responsibilities across experiments, pipeline development, proof production, analysis, dataset work, and writing.The contribution statement assigns distinct roles to the named collaborators.
A CONJECTURES AND THE DECLARATIVE PROOF STYLE
Declarative theorem proving interleaves conjectures with their proofs, allowing formal sketches to organize high-level reasoning while automated provers discharge individual conjectures.
- Declarative proofs interleave conjectures with their corresponding proofs, paralleling proof sketches in mathematical textbooks.
- Sledgehammer automates Isabelle reasoning by translating higher-order-logic goals into logics handled by automated theorem provers.
- If an external prover succeeds, Sledgehammer reconstructs the result in Isabelle/HOL using certified provers.
- Users can declare a conjecture in Isabelle/HOL and invoke Sledgehammer to search for a proof step, though searches may fail or time out.
C A PROOF TO AN INTERNATIONAL MATHEMATICAL OLYMPIAD PROBLEM
DSP successfully formalizes an IMO problem from a Minerva-generated informal proof, while the human-written proof fails because its indirect Euclidean-algorithm notation produces an incorrect sketch conjecture.
- A Minerva-generated informal solution led DSP to discover a proof for imo 1959 p1, the first problem of the first IMO.
- The autoformalizer copied relevant informal-proof segments as inline comments and selected premises after introducing conjectures.
- Five conjectures in the formal proof were subsequently proved by the automated theorem prover.The conjectures comprised four have statements and one show statement.
- The proof step used two verified low-level provers and ten lemmas or facts outside the language model’s scope.
- The human-written proof failed because indirect greatest-common-divisor notation was less suitable for sketching and yielded a semantically incorrect conjecture.
D MORE CASE ANALYSES OF HUMAN AND MINERVA INFORMAL PROOFS
Case analyses show that formal sketches preserve the structure of human and Minerva-generated informal proofs, including explicit case splits and intermediate conjectures.
- Human informal proofs: The human absolute-value proof considers ranges outside [0,1], derives contradictions, and concludes 0 ≤ x ≤ 1.
- Human informal proofs: The human algebra proof divides the problem into three cases, derives a contradiction in each, and then establishes the final objective.
- Minerva informal proofs: A Minerva-generated algebra proof yields a successful formal sketch with five intermediate conjectures based on the informal proof.
- Minerva informal proofs: The Minerva proof’s formal sketch makes even and odd cases explicit, although the informal proof does not state them directly.
- Minerva informal proofs: In a correct Minerva proof, the formal sketch is well aligned with the informal proof, while an incorrect proof receives an explicit base-case correction.