REVIEW 9 cited by
A Survey on Deep Learning for Theorem Proving
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
Theorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in natural language to rigorous derivations in formal systems. In recent years, the advancement of deep learning, especially the emergence of large language models, has sparked a notable surge of research exploring these techniques to enhance the process of theorem proving. This paper presents a comprehensive survey of deep learning for theorem proving by offering (i) a thorough review of existing approaches across various tasks such as autoformalization, premise selection, proofstep generation, and proof search; (ii) an extensive summary of curated datasets and strategies for synthetic data generation; (iii) a detailed analysis of evaluation metrics and the performance of state-of-the-art methods; and (iv) a critical discussion on the persistent challenges and the promising avenues for future exploration. Our survey aims to serve as a foundational reference for deep learning approaches in theorem proving, inspiring and catalyzing further research endeavors in this rapidly growing field. A curated list of papers is available at https://github.com/zhaoyu-li/DL4TP.
Forward citations
Cited by 9 Pith papers
-
FormalRx: Rectify and eXamine Semantic Failures in Autoformalization
FormalRx diagnoses Lean autoformalization failures with a 28-category SCI taxonomy and an 8B model that jointly predicts alignment, error type, location, and correction.
-
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.
-
Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs
Quarry splits Rocq proof automation into LLM-proposed decompositions and CoqHammer execution, ranking candidates by learned difficulty, improving success by 7–13 points.
-
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.
-
Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
An inference-only neuro-symbolic pipeline, DSP+, solves 80.7% of miniF2F and the previously unsolved imo_2019_p1, matching heavily RL-trained theorem provers without fine-tuning.
-
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.
-
Formally Solving Answer-Construction Problems in Lean
ECP, an enumerate-conjecture-prove framework with Lean verification, improves answer-construction accuracy on ConstructiveBench and a PutnamBench subset, but its benchmark has a 17% major-error rate and its abstract r...
-
An Ontology-Based Approach to Optimizing Geometry Problem Sets for Skill Development
The paper presents a retrospective ontology-and-solution-graph framework for curriculum design in Euclidean geometry, with a research agenda for automated solution validation.
-
Autoformalization in the Era of Large Language Models: A Survey
A literature review of LLM-based autoformalization, covering datasets, workflows, benchmarks, and its potential role in verifying AI outputs.
Discussion (0). Continue with ORCID to comment.