mlsanityData to 14 Oct 2026

Learning to Reason in Large Theories without Imitation

arXiv 1905.10501 ↗First posted 25 May 2019cs.LG cs.AI cs.LOcited by 27

Not on the map. Why?

Abstract (arXiv)

In this paper, we demonstrate how to do automated theorem proving in the presence of a large knowledge base of potential premises without learning from human proofs. We suggest an exploration mechanism that mixes in additional premises selected by a tf-idf (term frequency-inverse document frequency) based lookup in a deep reinforcement learning scenario. This helps with exploring and learning which premises are relevant for proving a new theorem. Our experiments show that the theorem prover trained with this exploration mechanism outperforms provers that are trained only on human proofs. It approaches the performance of a prover trained by a combination of imitation and reinforcement learning. We perform multiple experiments to understand the importance of the underlying assumptions that make our exploration approach work, thus explaining our design choices.

Key facts. Cited by 27 papers in the map (data through 14 Oct 2026). First posted on arXiv 25 May 2019.

Builds on

No reference list yet.

Built on by

Cited by year

Citing papers per year: 2021: 6; 2022: 6; 2023: 4; 2024: 9; 2025: 2.

27 papers.

Sort:

By area:

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  2. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  3. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  4. 2022Autoformalization with Large Language Modelscited by 263
  5. 2022Formal Mathematics Statement Curriculum Learningcited by 142
  6. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  7. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 109
  8. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 58
  9. 2021LIME: Learning Inductive Bias for Primitives of Mathematical Reasoningcited by 46
  10. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  11. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  12. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 27
15 more
  1. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 25
  2. 2023TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Modelscited by 24
  3. 2021Learning to Guide a Saturation-Based Theorem Provercited by 15
  4. 2024Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Provingcited by 11
  5. 2021Learning Symbolic Rules for Reasoning in Quasi-Natural Languagecited by 9
  6. 2024REFACTOR: Learning to Extract Theorems from Proofscited by 9
  7. 2024Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verificationcited by 9
  8. 2022Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesiscited by 5
  9. 2022Gym-saturation: an OpenAI Gym environment for saturation proverscited by 3
  10. 2024NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesiscited by 3
  11. 2024QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learningcited by 3
  12. 2024BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Provingcited by 2
  13. 2024Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generationcited by 2
  14. 2022Adversarial Learning to Reason in an Arbitrary Logiccited by 1
  15. 2025Extended Triangular Method: A Generalized Algorithm for Contradiction Separation Based Automated Deductioncited by 1