# Learning Rules Explaining Interactive Theorem Proving Tactic Prediction

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 15 of its 30 references that are in the map.
- First posted on arXiv 2 Nov 2024.

## Builds on (most cited first, 15 of 15)

- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [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)
- [Learning programs by learning from failures](https://mlsanity.com/paper/2005.02259/) (2020)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [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)
- [Tactic Learning and Proving for the Coq Proof Assistant](https://mlsanity.com/paper/2003.09140/) (2020)
- [Premise Selection and External Provers for HOL4](https://mlsanity.com/paper/1509.03534/) (2015)
- [Online Machine Learning Techniques for Coq: A Comparison](https://mlsanity.com/paper/2104.05207/) (2021)
- [LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL](https://mlsanity.com/paper/1906.08084/) (2019)

## Abstract (arXiv)

Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theorem provers (ITP). Deriving the most appropriate subsequent proof step, and reasoning about it, given the multitude of possibilities, remains a daunting task for novice users. To improve the situation, several investigations have developed machine learning based guidance for tactic selection. Such approaches struggle to learn non-trivial relationships between the chosen tactic and the structure of the proof state and represent them as symbolic expressions. To address these issues we (i) We represent the problem as an Inductive Logic Programming (ILP) task, (ii) Using the ILP representation we enriched the feature space by encoding additional, computationally expensive properties as background knowledge predicates, (iii) We use this enriched feature space to learn rules explaining when a tactic is applicable to a given proof state, (iv) we use the learned rules to filter the output of an existing tactic selection approach and empirically show improvement over the non-filtering approaches.