# Learning Guided Automated Reasoning: A Brief Survey

arXiv: https://arxiv.org/abs/2403.04017 · HTML: https://mlsanity.com/paper/2403.04017/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 56 of its 163 references that are in the map.
- First posted on arXiv 6 Mar 2024.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 30 of 56)

- [XGBoost: A Scalable Tree Boosting System](https://mlsanity.com/paper/1603.02754/) (2016)
- [Efficient Estimation of Word Representations in Vector Space](https://mlsanity.com/paper/1301.3781/) (2013)
- [Are Emergent Abilities of Large Language Models a Mirage?](https://mlsanity.com/paper/2304.15004/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Neural Probabilistic Logic Programming in DeepProbLog](https://mlsanity.com/paper/1907.08194/) (2019)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Learning Explanatory Rules from Noisy Data](https://mlsanity.com/paper/1711.04574/) (2017)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [Inductive logic programming at 30: a new introduction](https://mlsanity.com/paper/2008.07912/) (2020)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [Premise Selection for Theorem Proving by Deep Graph Embedding](https://mlsanity.com/paper/1709.09994/) (2017)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [Generating Correctness Proofs with Neural Networks](https://mlsanity.com/paper/1907.07794/) (2019)
- [ENIGMA: Efficient Learning-based Inference Guiding Machine](https://mlsanity.com/paper/1701.06532/) (2017)
- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [First Neural Conjecturing Datasets and Experiments](https://mlsanity.com/paper/2005.14664/) (2020)
- [Learning Continuous Semantic Representations of Symbolic Expressions](https://mlsanity.com/paper/1611.01423/) (2016)
- [Can Neural Networks Understand Logical Entailment?](https://mlsanity.com/paper/1802.08535/) (2018)
- [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019)
- [The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq](https://mlsanity.com/paper/2008.00120/) (2020)
- [Techniques for Symbol Grounding with SATNet](https://mlsanity.com/paper/2106.11072/) (2021)
- [MizAR 40 for Mizar 40](https://mlsanity.com/paper/1310.2805/) (2013)
- [Neuro-Symbolic Hierarchical Rule Induction](https://mlsanity.com/paper/2112.13418/) (2021)
- [Property Invariant Embedding for Automated Reasoning](https://mlsanity.com/paper/1911.12073/) (2019)

## Built on by (most cited first, 7 of 7)

- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [Learning Conjecturing from Scratch](https://mlsanity.com/paper/2503.01389/) (2025)
- [Towards AI-assisted Neutrino Flavor Theory Design](https://mlsanity.com/paper/2506.08080/) (2025)
- [Neuro-Symbolic AI for Cybersecurity: State of the Art, Challenges, and Opportunities](https://mlsanity.com/paper/2509.06921/) (2025)
- [Tree-Based Deep Learning for Ranking Symbolic Integration Algorithms](https://mlsanity.com/paper/2508.06383/) (2025)
- [Machine Learning for Quantifier Selection in cvc5](https://mlsanity.com/paper/2408.14338/) (2024)
- [Efficient Neural Clause-Selection Reinforcement](https://mlsanity.com/paper/2503.07792/) (2025)

## Abstract (arXiv)

Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems reducible to mathematics and logical reasoning. In practice, such systems however face large combinatorial explosion, and therefore include many heuristics and choice points that considerably influence their performance. This is an opportunity for trained machine learning predictors, which can guide the work of such reasoning systems. Conversely, deductive search supported by the notion of logically valid proof allows one to train machine learning systems on large reasoning corpora. Such bodies of proof are usually correct by construction and when combined with more and more precise trained guidance they can be boostrapped into very large corpora, with increasingly long reasoning chains and possibly novel proof ideas. In this paper we provide an overview of several automated reasoning and theorem proving domains and the learning and AI methods that have been so far developed for them. These include premise selection, proof guidance in several settings, AI systems and feedback loops iterating between reasoning and learning, and symbolic classification problems.