Elamur Research⌕
☰
home / papers / 2020 / Stateful Premise Selection by Recurrent Neural Networks

Stateful Premise Selection by Recurrent Neural Networks

Paper · 2020 · Bartosz Piotrowski and Josef Urban

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 PraguePrague · Czechia16 works · 930 citations🎓University of WarsawWarsaw · Poland14 works · 774 citations

 Fields, topics and concepts

📚 Shelves 2The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 works

🧭 Topics 1Research subjects and languages the work is about.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. DOI 10.48550/arxiv.2004.08212 · arXiv 2004.08212

@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}
}

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. J. Autom. Reasoning, 52(2):191–213, 2014.
  2. J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban. Hammering towards 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
  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
  5. K. Cho, B. van Merrienboer, D. Bahdanau, and Y. Bengio. On the properties of neural machine translation: Encoder-decoder approaches. 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…
  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
  8. M. Freitag and Y. Al-Onaizan. Beam search strategies for neural machine translation. 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
  10. S. Hochreiter and J. Schmidhuber. Long short-term memory. Neural Computation, 9(8):1735–1780, 1997. find
  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
  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
  13. C. Kaliszyk and J. Urban. Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning, 53(2):173–213, 2014.
  14. C. Kaliszyk and J. Urban. MizAR 40 for 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. 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
  17. G. Lample and F. Charton. Deep learning for symbolic mathematics. CoRR, abs/1912.01412, 2019.
  18. T. Luong, H. Pham, and C. D. Manning. Effective approaches to attention-based neural machine translation. 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
  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
  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
  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
  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
  24. I. Sutskever, O. Vinyals, and Q. V. Le. Sequence to sequence learning with 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
  26. J. Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. find
  27. Q. Wang, C. Kaliszyk, and J. Urban. First experiments with neural translation of informal to formal mathematics. 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

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/piotrowski-2020-stateful-premise-selection-recurrent-neural/