REVIEW 18 cited by
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original 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.
Forward citations
Cited by 18 Pith papers
-
How Your Credentials Are Leaked by LLM Agent Skills: An Empirical Study
Large-scale audit of SkillsMP agent skills finds 520 skills with 1,708 credential-leak issues, dominated by debug logging into the LLM context and hard-to-remediate forks.
-
ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
ProofAug extracts progressively coarser valid proof skeletons from failed LLM proof attempts and fills them with automated theorem provers, improving miniF2F pass rates and sample efficiency in Isabelle and Lean.
-
CircuitProver: Agentic Lean 4 Theorem Proving with Reusable Circuit Proof Library for Hardware Verification
CircuitProver is an agentic Lean 4 framework that automatically proves parameterized hardware designs correct against formalized specifications and reuses proof knowledge across tasks.
-
Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
A verifier-grounded self-evolving Lean proof agent with a champion-driven, self-hardening benchmark reached 45.1% held-out miniF2F solve rate versus 32.0% for a fixed-benchmark baseline.
-
FormaRL: Enhancing Autoformalization with no Labeled Data
A reinforcement learning framework improves autoformalization without labeled data by rewarding outputs that pass Lean syntax and LLM consistency checks.
-
StepFun-Prover Preview: Let's Think and Verify Step by Step
A reinforcement learning pipeline with Lean verifier feedback trains a 32B model that scores 70.0% pass@1 on miniF2F-test, a new state of the art.
-
Mathesis: Towards Formal Theorem Proving from Natural Languages
An RL-trained autoformalizer plus a Lean prover solves 18% of Chinese Gaokao proof problems end-to-end from natural language, and 64.3% of MiniF2F at pass@32.
-
MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?
MATP-BENCH pairs 1,056 multimodal math problems with formal theorem statements in Lean 4, Coq, and Isabelle; the strongest tested model solves only 5.68% of Lean 4 end-to-end proving tasks at pass@10.
-
Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Engine
SDE-GPG samples from a knowledge-point-to-definition mapping table, runs the AlphaGeometry symbolic deduction engine to produce conclusions, filters candidates with a checking function, and translates the formal outpu...
-
Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening
GRPO's rank bias reinforces likely answers and neglects rare correct proofs; an unlikeliness reward that down-weights likely correct samples improves pass@N in formal theorem proving.
-
Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
An open-source theorem-proving model reaches state-of-the-art scores on miniF2F (57.6% Pass@32) and PutnamBench by training on 800K formal proofs synthesized through autoformalization and expert iteration.
-
From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
The authors create an 18,000-pair formal-verification dataset, evaluate ten LLMs on six subtasks in five languages, and find that 7-8B fine-tuned models match DeepSeek-R1-671B while also yielding mixed but positive tr...
-
Generative Agents for Multi-Agent Autoformalization of Interaction Scenarios
GAMA uses LLM agents to turn natural language game descriptions into validated executable logic programs, reaching about 77% semantic correctness on 110 scenarios from five 2x2 games.
-
Case study: proving sqrt(2) irrational with LPTP and an LLM
A general-purpose LLM and the LPTP proof checker jointly produced a machine-checked proof that sqrt(2) is irrational, with the checker localizing every wrong step.
-
Solving Formal Math Problems by Decomposition and Iterative Reflection
An agent that decomposes Lean 4 goals into subproblems and iteratively repairs proofs achieves a 95.9% pass rate on miniF2F-test using a stock Gemini model.
-
StepProof: Step-by-step verification of natural language mathematical proofs
Decomposing natural-language proofs into sentence-level formal subproofs improves autoformalization success rates and efficiency compared with whole-proof formalization.
-
Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations
The proposed Faithful-Refiner, combining syntactic parsing, quantifier and consistency checks, logical-relation guidance, and detailed proof feedback, raises explanation refinement rates on three NLI benchmarks by lar...
-
Psychometric-Based Evaluation for Theorem Proving with Large Language Models
The authors annotate miniF2F theorems with LLM-computed difficulty and discrimination scores, then use adaptive testing to rank 10 theorem-proving LLMs using only about 23% of the theorems.
Discussion (0). Continue with ORCID to comment.