mlsanityData to 14 Oct 2026

Training a First-Order Theorem Prover from Synthetic Data

arXiv 2103.03798 ↗First posted 5 Mar 2021cs.AIcited by 8

Not on the map. Why?

Abstract (arXiv)

A major challenge in applying machine learning to automated theorem proving is the scarcity of training data, which is a key ingredient in training successful deep learning models. To tackle this problem, we propose an approach that relies on training purely with synthetically generated theorems, without any human data aside from axioms. We use these theorems to train a neurally-guided saturation-based prover. Our neural prover outperforms the state-of-the-art E-prover on this synthetic data in both time and search steps, and shows significant transfer to the unseen human-written theorems from the TPTP library, where it solves 72% of first-order problems without equality.

Key facts. Cited by 8 papers in the map (data through 14 Oct 2026). Builds on 14 of its 28 references that are in the map. First posted on arXiv 5 Mar 2021.

Builds on

14 of 28 references.

References · 14

  1. 2017Attention Is All You Needcited by 60,361
  2. 2020Language Models are Few-Shot Learnerscited by 32,419
  3. 2020Scaling Laws for Neural Language Modelscited by 6,586
  4. 2020A Generalization of Transformer Networks to Graphscited by 661
  5. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  6. 2020Emergent Complexity and Zero-shot Transfer via Unsupervised Environment Designcited by 275
  7. 2017Intrinsic Motivation and Automatic Curricula via Asymmetric Self-Playcited by 141
  8. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  9. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 109
  10. 2017Intrinsically Motivated Goal Exploration Processes with Automatic Curriculum Learningcited by 83
  11. 2017Deep Network Guided Proof Searchcited by 47
  12. 2020Learning to Prove Theorems by Learning to Generate Theoremscited by 43
2 more
  1. 2019Automated curricula through setter-solver interactionscited by 26
  2. 2019HOList: An Environment for Machine Learning of Higher-Order Theorem Provingcited by 19

Built on by

Cited by year

Citing papers per year: 2021: 1; 2022: 2; 2023: 0; 2024: 4; 2025: 1.

8 papers.

  1. 2022Formal Mathematics Statement Curriculum Learningcited by 142
  2. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  3. 2024Proposing and solving olympiad geometry with guided tree searchcited by 19
  4. 2021Proving Theorems using Incremental Learning and Hindsight Experience Replaycited by 13
  5. 2024Application of AI to formal methods - an analysis of current trendscited by 2
  6. 2022Adversarial Learning to Reason in an Arbitrary Logiccited by 1
  7. 2024Learning Better Representations From Less Data For Propositional Satisfiabilitycited by 1
  8. 2025Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Enginecited by 1