---
title: "Stateful Premise Selection by Recurrent Neural Networks (2020)"
description: "Automated theorem provers that work over large formal libraries depend on premise selection, which… 27 references, cited by 7 papers here."
authors: ["Bartosz Piotrowski", "Josef Urban"]
year: 2020
venue: "arXiv:2004.08212"
source: "https://arxiv.org/abs/2004.08212"
doi: "10.48550/arxiv.2004.08212"
arxiv: "2004.08212"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/piotrowski-2020-stateful-premise-selection-recurrent-neural/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/piotrowski-2020-stateful-premise-selection-recurrent-neural/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2020](https://md.research.elamur.ai/free/en/papers/2020/page/8/) / Stateful Premise Selection by Recurrent Neural Networks

# Stateful Premise Selection by Recurrent Neural Networks

**Authors:** [Bartosz Piotrowski](https://md.research.elamur.ai/free/en/authors/bartosz-piotrowski/) and [Josef Urban](https://md.research.elamur.ai/free/en/authors/josef-urban/) · **Year:** 2020 · **Venue:** [arXiv:2004.08212](https://md.research.elamur.ai/free/en/venues/epic-series-in-computing/) ([EPiC series in computing 2020](https://md.research.elamur.ai/free/en/venues/epic-series-in-computing/2020/)) · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/2004.08212) · [PDF](https://arxiv.org/pdf/2004.08212v1) · [DOI 10.48550/arxiv.2004.08212](https://doi.org/10.48550/arxiv.2004.08212) · [arXiv 2004.08212](https://arxiv.org/abs/2004.08212) · [OpenAlex](https://openalex.org/W3016312047)

**Citations:** 14 citations (OpenAlex, 2026-10-14) · [7](https://md.research.elamur.ai/free/en/papers/piotrowski-2020-stateful-premise-selection-recurrent-neural/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Automated theorem provers that work over large formal libraries depend on premise selection, which means picking the few relevant facts from thousands of candidates. Earlier learning-based selectors score each fact on its own against the conjecture. This ignores that facts can complement or duplicate each other. Piotrowski and Urban reframe the task as sequence-to-sequence translation. An RNN encoder-decoder (OpenNMT with LSTM cells, Luong attention and beam search) reads the theorem statement and outputs premise names one at a time, so a hidden state tracks what has already been chosen. Training data come from many ATP proofs of MPTP2078 problems, a Mizar/MML subset translated to TPTP. The authors compare several ways of building training examples:
- encoding the conjecture in standard or prefix form,
- ordering premises randomly, along the proof tree, or as E linearizes the proof,
- adding subproof data,
- oversampling rare premises.

The best neural setup proves noticeably more test theorems than the gradient-boosted-tree baseline (XGBoost). Its beam search yields alternative, complementary premise sets rather than one ranking that keeps growing, and this tends to be more useful when a prover makes several attempts.

## Key points
- **Dataset:** ATPboost (E prover + XGBoost) produced 24,087 distinct proofs of 1469 MPTP2078 theorems, using 2227 premises. The split gave 18,361 training pairs from 1100 theorems and a test set of 310 theorems.
- **OpenNMT settings:** mostly defaults, with 2-layer LSTMs of 500 units and 500-dimensional embeddings. The 10 most probable beam outputs were passed to the ATP.
- **Premise ordering:** orders derived from the proofs worked better than random permutations. Prefix and standard conjecture encodings performed about the same.
- **Proved share:** subproof augmentation raised the NMT proved share from 0.29 to 0.40, an 11-point gain. The best XGBoost result was 0.31.
- **Overlap with XGBoost:** across the Table 3 runs, NMT proved 167 theorems and XGBoost 142. Only 121 were shared, and 46 were found by NMT alone. XGBoost still scored higher on the Jaccard and Coverage similarity metrics.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Czech Technical University in Prague](https://md.research.elamur.ai/free/en/universities/czech-technical-university-in-prague/) — University, Prague, Czechia · 16 works · 930 citations
- [University of Warsaw](https://md.research.elamur.ai/free/en/universities/university-of-warsaw/) — University, Warsaw, Poland · 14 works · 774 citations

📚 Shelves (2): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Bartosz Piotrowski and Josef Urban. 2020. Stateful Premise Selection by Recurrent Neural Networks. arXiv:2004.08212.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{piotrowski2020stateful,
  title = {{Stateful Premise Selection by Recurrent Neural Networks}},
  author = {Bartosz Piotrowski and Josef Urban},
  year = {2020},
  doi = {10.48550/arxiv.2004.08212},
  eprint = {2004.08212},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2004.08212}
}
```

- [← previous Pragmatic Issue-Sensitive Image Captioning](https://md.research.elamur.ai/free/en/papers/nie-2020-pragmatic-issue-sensitive-image-captioning/)
- [next → TED-CDB: A Large-Scale Chinese Discourse Relation Dataset on TED Talks](https://md.research.elamur.ai/free/en/papers/long-2020-ted-cdb-large-scale-chinese/)
- [↑ back to papers of 2020](https://md.research.elamur.ai/free/en/papers/2020/page/8/)

## References

27 references, 13 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze, and J. Urban. [Premise selection for mathematics by corpus analysis and kernel methods](https://md.research.elamur.ai/free/en/papers/alama-2011-premise-selection-mathematics-corpus-analysis/). J. Autom. Reasoning, 52(2):191–213, 2014.
2. J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban. [Hammering towards QED](https://md.research.elamur.ai/free/en/papers/blanchette-2016-hammering-qed/). J. Formalized Reasoning, 9(1):101–148, 2016.
3. M. Buda, A. Maki, and M. A. Mazurowski. A systematic study of the class imbalance problem in convolutional neural networks. Neural Networks, 106:249–259, 2018. [find](https://scholar.google.com/scholar?q=M%2E+Buda%2C+A%2E+Maki%2C+and+M%2E+A%2E+Mazurowski%2E+A+systematic+study+of+the+class+imbalance+problem+in+convolutional+neural+networks%2E+Neural+Networks%2C+106%3A249%E2%80%93259%2C+2018%2E)
4. T. Chen and C. Guestrin. XGBoost: A scalable tree boosting system. In Proceedings of the 22Nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD 2016, pages 785–794, New York, NY, USA, 2016. ACM. [find](https://scholar.google.com/scholar?q=T%2E+Chen+and+C%2E+Guestrin%2E+XGBoost%3A+A+scalable+tree+boosting+system%2E+In+Proceedings+of+the+22Nd+ACM+SIGKDD+International+Conference+on+Knowledge+Discovery+and+Data+Mining%2C+KDD+2016%2C+pages+785%E2%80%93794%2C+New+Y)
5. K. Cho, B. van Merrienboer, D. Bahdanau, and Y. Bengio. [On the properties of neural machine translation: Encoder-decoder approaches](https://md.research.elamur.ai/free/en/papers/cho-2014-properties-neural-machine-translation-encoder/). In D. Wu, M. Carpuat, X. Carreras, and E. M. Vecchi, editors, Proceedings of SSST@EMNLP 2014, Eighth Workshop on Syntax, Semantics and Structure in Statistical Transla…
6. K. Cho, B. van Merrienboer, Ç. Gülçehre, D. Bahdanau, F. Bougares, H. Schwenk, and Y. Bengio. Learning phrase representations using RNN encoder-decoder for statistical machine translation. In A. Moschitti, B. Pang, and W. Daelemans, editors, Proceedings of the 2014 [Conference on Empirical Methods…](https://md.research.elamur.ai/free/en/papers/cho-2014-learning-phrase-representations-rnn-encoder/)
7. S. C. Deerwester, S. T. Dumais, T. K. Landauer, G. W. Furnas, and R. A. Harshman. Indexing by Latent Semantic Analysis. JASIS, 41(6):391–407, 1990. [find](https://scholar.google.com/scholar?q=S%2E+C%2E+Deerwester%2C+S%2E+T%2E+Dumais%2C+T%2E+K%2E+Landauer%2C+G%2E+W%2E+Furnas%2C+and+R%2E+A%2E+Harshman%2E+Indexing+by+Latent+Semantic+Analysis%2E+JASIS%2C+41%286%29%3A391%E2%80%93407%2C+1990%2E)
8. M. Freitag and Y. Al-Onaizan. [Beam search strategies for neural machine translation](https://md.research.elamur.ai/free/en/papers/freitag-2017-beam-search-strategies-neural-machine/). In T. Luong, A. Birch, G. Neubig, and A. M. Finch, editors, Proceedings of the First Workshop on Neural Machine Translation, NMT@ACL 2017, Vancouver, Canada, August 4, 2017, pages 56–60. Association for Computationa…
9. A. Grabowski, A. Kornilowicz, and A. Naumowicz. Mizar in a nutshell. J. Formalized Reasoning, 3(2):153–245, 2010. [find](https://scholar.google.com/scholar?q=A%2E+Grabowski%2C+A%2E+Kornilowicz%2C+and+A%2E+Naumowicz%2E+Mizar+in+a+nutshell%2E+J%2E+Formalized+Reasoning%2C+3%282%29%3A153%E2%80%93245%2C+2010%2E)
10. S. Hochreiter and J. Schmidhuber. Long short-term memory. Neural Computation, 9(8):1735–1780, 1997. [find](https://scholar.google.com/scholar?q=S%2E+Hochreiter+and+J%2E+Schmidhuber%2E+Long+short%2Dterm+memory%2E+Neural+Computation%2C+9%288%29%3A1735%E2%80%931780%2C+1997%2E)
11. K. Hoder and A. Voronkov. Sine qua non for large theory reasoning. In N. Bjørner and V. Sofronie-Stokkermans, editors, CADE, volume 6803 of LNCS, pages 299–314. Springer, 2011. [find](https://scholar.google.com/scholar?q=K%2E+Hoder+and+A%2E+Voronkov%2E+Sine+qua+non+for+large+theory+reasoning%2E+In+N%2E+Bj%C3%B8rner+and+V%2E+Sofronie%2DStokkermans%2C+editors%2C+CADE%2C+volume+6803+of+LNCS%2C+pages+299%E2%80%93314%2E+Springer%2C+2011%2E)
12. G. Irving, C. Szegedy, A. A. Alemi, N. Eén, F. Chollet, and J. Urban. DeepMath – Deep sequence models for premise selection. In D. D. Lee, M. Sugiyama, U. V. Luxburg, I. Guyon, and R. Garnett, editors, Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Pro… — [DeepMath - Deep Sequence Models for Premise Selection](https://md.research.elamur.ai/free/en/papers/alemi-2016-deepmath-deep-sequence-models-premise/)
13. C. Kaliszyk and J. Urban. [Learning-assisted automated reasoning with Flyspeck](https://md.research.elamur.ai/free/en/papers/kaliszyk-2012-learning-assisted-automated-reasoning-flyspeck/). J. Autom. Reasoning, 53(2):173–213, 2014.
14. C. Kaliszyk and J. Urban. [MizAR 40 for Mizar 40](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/). J. Autom. Reasoning, 55(3):245–256, 2015.
15. G. Klein, Y. Kim, Y. Deng, J. Senellart, and A. Rush. [OpenNMT: Open-source toolkit for neural machine translation](https://md.research.elamur.ai/free/en/papers/klein-2017-opennmt-open-source-toolkit-neural/). In Proceedings of ACL 2017, System Demonstrations, pages 67–72, Vancouver, Canada, July 2017. Association for Computational Linguistics.
16. A. S. Kucik and K. Korovin. Premise selection with neural networks and distributed representation of features. CoRR, abs/1807.10268, 2018. — [arXiv:1807.10268](https://arxiv.org/abs/1807.10268) [find](https://scholar.google.com/scholar?q=A%2E+S%2E+Kucik+and+K%2E+Korovin%2E+Premise+selection+with+neural+networks+and+distributed+representation+of+features%2E+CoRR%2C+abs%2F1807%2E10268%2C+2018%2E+%E2%80%94+%5BarXiv%3A1807%2E10268%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1807%2E10268%29)
17. G. Lample and F. Charton. [Deep learning for symbolic mathematics](https://md.research.elamur.ai/free/en/papers/lample-2019-deep-learning-symbolic-mathematics/). CoRR, abs/1912.01412, 2019.
18. T. Luong, H. Pham, and C. D. Manning. [Effective approaches to attention-based neural machine translation](https://md.research.elamur.ai/free/en/papers/luong-2015-effective-approaches-attention-based-neural/). In L. Màrquez, C. Callison-Burch, J. Su, D. Pighin, and Y. Marton, editors, Proceed-Piotrowski and Urban Stateful Premise Selection with RNNs ings of the 2015 Conference on Empirical Methods in…
19. J. Meng and L. C. Paulson. Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic, 7(1):41–57, 2009. [find](https://scholar.google.com/scholar?q=J%2E+Meng+and+L%2E+C%2E+Paulson%2E+Lightweight+relevance+filtering+for+machine%2Dgenerated+resolution+problems%2E+J%2E+Applied+Logic%2C+7%281%29%3A41%E2%80%9357%2C+2009%2E)
20. B. Piotrowski and J. Urban. ATPboost: Learning premise selection in binary setting with ATP feedback. In D. Galmiche, S. Schulz, and R. Sebastiani, editors, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, Ju… [find](https://scholar.google.com/scholar?q=B%2E+Piotrowski+and+J%2E+Urban%2E+ATPboost%3A+Learning+premise+selection+in+binary+setting+with+ATP+feedback%2E+In+D%2E+Galmiche%2C+S%2E+Schulz%2C+and+R%2E+Sebastiani%2C+editors%2C+Automated+Reasoning+%2D+9th+International+Joi)
21. B. Piotrowski, J. Urban, C. E. Brown, and C. Kaliszyk. Can neural networks learn symbolic rewriting? CoRR, abs/1911.04873, 2019. — [arXiv:1911.04873](https://arxiv.org/abs/1911.04873) [find](https://scholar.google.com/scholar?q=B%2E+Piotrowski%2C+J%2E+Urban%2C+C%2E+E%2E+Brown%2C+and+C%2E+Kaliszyk%2E+Can+neural+networks+learn+symbolic+rewriting%3F+CoRR%2C+abs%2F1911%2E04873%2C+2019%2E+%E2%80%94+%5BarXiv%3A1911%2E04873%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1911%2E04873%29)
22. S. Schulz. System description: E 1.8. In K. L. McMillan, A. Middeldorp, and A. Voronkov, editors, LPAR, volume 8312 of LNCS, pages 735–743. Springer, 2013. [find](https://scholar.google.com/scholar?q=S%2E+Schulz%2E+System+description%3A+E+1%2E8%2E+In+K%2E+L%2E+McMillan%2C+A%2E+Middeldorp%2C+and+A%2E+Voronkov%2C+editors%2C+LPAR%2C+volume+8312+of+LNCS%2C+pages+735%E2%80%93743%2E+Springer%2C+2013%2E)
23. G. Sutcliffe. The TPTP world - infrastructure for automated reasoning. In E. M. Clarke and A. Voronkov, editors, LPAR (Dakar), volume 6355 of LNCS, pages 1–12. Springer, 2010. [find](https://scholar.google.com/scholar?q=G%2E+Sutcliffe%2E+The+TPTP+world+%2D+infrastructure+for+automated+reasoning%2E+In+E%2E+M%2E+Clarke+and+A%2E+Voronkov%2C+editors%2C+LPAR+%28Dakar%29%2C+volume+6355+of+LNCS%2C+pages+1%E2%80%9312%2E+Springer%2C+2010%2E)
24. I. Sutskever, O. Vinyals, and Q. V. Le. [Sequence to sequence learning with neural networks](https://md.research.elamur.ai/free/en/papers/sutskever-2014-sequence-sequence-learning-neural-networks/). In Z. Ghahramani, M. Welling, C. Cortes, N. D. Lawrence, and K. Q. Weinberger, editors, Advances in Neural Information Processing Systems 27, pages 3104–3112. Curran Associates, Inc., 2014.
25. E. Tsivtsivadze, J. Urban, H. Geuvers, and T. Heskes. Semantic graph kernels for automated reasoning. In SDM, pages 795–803. SIAM / Omnipress, 2011. [find](https://scholar.google.com/scholar?q=E%2E+Tsivtsivadze%2C+J%2E+Urban%2C+H%2E+Geuvers%2C+and+T%2E+Heskes%2E+Semantic+graph+kernels+for+automated+reasoning%2E+In+SDM%2C+pages+795%E2%80%93803%2E+SIAM+%2F+Omnipress%2C+2011%2E)
26. J. Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. [find](https://scholar.google.com/scholar?q=J%2E+Urban%2E+MPTP+0%2E2%3A+Design%2C+implementation%2C+and+initial+experiments%2E+J%2E+Autom%2E+Reasoning%2C+37%281%2D2%29%3A21%E2%80%9343%2C+2006%2E)
27. Q. Wang, C. Kaliszyk, and J. Urban. [First experiments with neural translation of informal to formal mathematics](https://md.research.elamur.ai/free/en/papers/wang-2018-first-experiments-neural-translation-informal/). In F. Rabe, W. M. Farmer, G. O. Passmore, and A. Youssef, editors, Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Pro…

*Updated 3 November 2026*