# Stateful Premise Selection by Recurrent Neural Networks

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Mar 2020.

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

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [Vampire With a Brain Is a Good ITP Hammer](https://mlsanity.com/paper/2102.03529/) (2021)
- [The Isabelle ENIGMA](https://mlsanity.com/paper/2205.01981/) (2022)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [MizAR 60 for Mizar 50](https://mlsanity.com/paper/2303.06686/) (2023)
- [Learning Conjecturing from Scratch](https://mlsanity.com/paper/2503.01389/) (2025)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspective](https://mlsanity.com/paper/2510.21999/) (2025)

## Abstract (arXiv)

In this work, we develop a new learning-based method for selecting facts (premises) when proving new goals over large formal libraries. Unlike previous methods that choose sets of facts independently of each other by their rank, the new method uses the notion of state that is updated each time a choice of a fact is made. Our stateful architecture is based on recurrent neural networks which have been recently very successful in stateful tasks such as language translation. The new method is combined with data augmentation techniques, evaluated in several ways on a standard large-theory benchmark, and compared to state-of-the-art premise approach based on gradient boosted trees. It is shown to perform significantly better and to solve many new problems.