CoChat
Sign Up
PreprintCited by 68AI-based Problem Solving and PlanningLogic, programming, and type systemsArtificial Intelligence Applications

The DOI matches its DataCite record; 1 of the 1 references it cites were found in a registry or an index.

Reinforcement Learning of Theorem Proving

Open access
Kaliszyk, Cezary, Urban, Josef, Michalewski, Henryk, Olšák, Mirek·2018·arXiv
DOI 10.48550/arxiv.1805.07563arXiv 1805.07563
Open this paper in CoChat — free accountOpen PDF

Abstract

We introduce a theorem proving algorithm that uses practically no domain heuristics for guiding its connection-style proof search. Instead, it runs many Monte-Carlo simulations guided by reinforcement learning from previous proof attempts. We produce several versions of the prover, parameterized by different learning and guiding algorithms. The strongest version of the system is trained on a large corpus of mathematical problems and evaluated on previously unseen problems. The trained system solves within the same number of inferences over 40% more problems than a baseline prover, which is an unusually high improvement in this hard AI domain. To our knowledge this is the first time reinforcement learning has been convincingly applied to solving general mathematical problems on a large scale.

Overview

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

DataCite · 10.48550/arxiv.1805.07563

Cites

1 of 1 references verified0 citation errors · 0 not checkable

Statistics

Verification

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Citations

Cites

Flagged first, then by citations

Research works printed but not linked: 42

  1. J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze, and J. Urban. Premise selection for math- ematics by corpus analysis and kernel methods. J. Autom. Reasoning, 52(2):191-213, 2014.
  2. A. A. Alemi, F. Chollet, N. Eén, G. Irving, C. Szegedy, and J. Urban. DeepMath -deep se- quence 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 Con- ference on Neural Information Processing Systems 2016, pages 2235-2243, 2016.
  3. T. Anthony, Z. Tian, and D. Barber. Thinking fast and slow with deep learning and tree search. In I. Guyon, U. von Luxburg, S. Bengio, H. M. Wallach, R. Fergus, S. V. N. Vishwanathan, and R. Garnett, editors, Advances in Neural Information Processing Systems 30: Annual Con- ference on Neural Information Processing Systems 2017, pages 5366-5376, 2017.
  4. L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217-247, 1994.
  5. J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, and J. Urban. A learning-based fact selector for Isabelle/HOL. J. Autom. Reasoning, 57(3):219-244, 2016.
  6. J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban. Hammering towards QED. J. Formalized Reasoning, 9(1):101-148, 2016.
  7. 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 '16, pages 785-794, New York, NY, USA, 2016. ACM.
  8. R.-E. Fan, K.-W. Chang, C.-J. Hsieh, X.-R. Wang, and C.-J. Lin. Liblinear: A library for large linear classification. Journal of machine learning research, 9(Aug):1871-1874, 2008.
  9. M. Färber, C. Kaliszyk, and J. Urban. Monte Carlo tableau proof search. In L. de Moura, editor, 26th International Conference on Automated Deduction (CADE), volume 10395 of LNCS, pages 563-579. Springer, 2017.
  10. T. Gauthier and C. Kaliszyk. Premise selection and external provers for HOL4. In X. Leroy and A. Tiu, editors, Proc. of the 4th Conference on Certified Programs and Proofs (CPP'15), pages 49-57. ACM, 2015.
  11. T. Gauthier, C. Kaliszyk, and J. Urban. TacticToe: Learning to reason with HOL4 tactics. In T. Eiter and D. Sands, editors, 21st International Conference on Logic for Programming, Ar- tificial Intelligence and Reasoning, LPAR-21, volume 46 of EPiC Series in Computing, pages 125-143. EasyChair, 2017.
  12. A. Grabowski, A. Korniłowicz, and A. Naumowicz. Mizar in a nutshell. J. Formalized Rea- soning, 3(2):153-245, 2010.
  13. T. Gransden, N. Walkinshaw, and R. Raman. SEPIA: search for proofs using inferred automata. In Automated Deduction -CADE-25 -25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 246-255, 2015.
  14. R. Hähnle. Tableaux and related methods. In Robinson and Voronkov [34], pages 100-178.
  15. J. Jakubuv and J. Urban. BliStrTune: hierarchical invention of theorem proving strategies. In Y. Bertot and V. Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 43-52. ACM, 2017.
  16. J. Jakubuv and J. Urban. ENIGMA: efficient learning-based inference guiding machine. In H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke, editors, Intelligent Computer Mathematics -10th International Conference, CICM 2017, volume 10383 of Lecture Notes in Computer Science, pages 292-302. Springer, 2017.
  17. C. Kaliszyk and J. Urban. Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning, 53(2):173-213, 2014.
  18. C. Kaliszyk and J. Urban. FEMaLeCoP: Fairly efficient machine learning connection prover. In M. Davis, A. Fehnker, A. McIver, and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning -20th International Conference, volume 9450 of Lecture Notes in Computer Science, pages 88-96. Springer, 2015.
  19. C. Kaliszyk and J. Urban. MizAR 40 for Mizar 40. J. Autom. Reasoning, 55(3):245-256, 2015.
  20. In S. Schulz, L. de Moura, and B. Konev, editors, 4th Workshop on Practical Aspects of Automated Reasoning, PAAR@IJCAR 2014, Vienna, Austria, 2014, volume 31 of EPiC Series in Computing, pages 60-66. EasyChair, 2014.
  21. C. Kaliszyk, J. Urban, and J. Vyskočil. Certified connection tableaux proofs for HOL Light and TPTP. In X. Leroy and A. Tiu, editors, Proc. of the 4th Conference on Certified Programs and Proofs (CPP'15), pages 59-66. ACM, 2015.
  22. L. Kocsis and C. Szepesvári. Bandit based monte-carlo planning. In J. Fürnkranz, T. Scheffer, and M. Spiliopoulou, editors, Machine Learning: ECML 2006, 17th European Conference on Machine Learning, volume 4212 of LNCS, pages 282-293. Springer, 2006.
  23. D. Kühlwein, T. van Laarhoven, E. Tsivtsivadze, J. Urban, and T. Heskes. Overview and evalu- ation of premise selection techniques for large theory mathematics. In B. Gramlich, D. Miller, and U. Sattler, editors, IJCAR, volume 7364 of LNCS, pages 378-392. Springer, 2012.
  24. R. Letz, K. Mayr, and C. Goller. Controlled integration of the cut rule into connection tableau calculi. Journal of Automated Reasoning, 13:297-337, 1994.
  25. S. M. Loos, G. Irving, C. Szegedy, and C. Kaliszyk. Deep network guided proof search. In T. Eiter and D. Sands, editors, 21st International Conference on Logic for Programming, Ar- tificial Intelligence and Reasoning, LPAR-21, volume 46 of EPiC Series in Computing, pages 85-105. EasyChair, 2017.
  26. W. McCune. Otter 2.0. In International Conference on Automated Deduction, pages 663-664. Springer, 1990.
  27. J. Meng and L. C. Paulson. Translating higher-order clauses to first-order clauses. J. Autom. Reasoning, 40(1):35-60, 2008.
  28. J. Otten. Restricting backtracking in connection calculi. AI Commun., 23(2-3):159-182, 2010.
  29. J. Otten and W. Bibel. leanCoP: lean connection-based theorem proving. J. Symb. Comput., 36(1-2):139-161, 2003.
  30. F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Pret- tenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Per- rot, and E. Duchesnay. Scikit-learn: Machine learning in Python. Journal of Machine Learning Research, 12:2825-2830, 2011.
  31. B. Piotrowski and J. Urban. ATPboost: Learning premise selection in binary setting with ATP feedback. CoRR, abs/1802.03375, 2018. · arXiv
  32. J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM (JACM), 12(1):23-41, 1965.
  33. J. A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press, 2001.
  34. S. Schäfer and S. Schulz. Breeding theorem proving heuristics with genetic algorithms. In G. Gottlob, G. Sutcliffe, and A. Voronkov, editors, Global Conference on Artificial Intelligence, GCAI 2015, volume 36 of EPiC Series in Computing, pages 263-274. EasyChair, 2015.
  35. D. Silver, A. Huang, C. J. Maddison, A. Guez, L. Sifre, G. van den Driessche, J. Schrittwieser, I. Antonoglou, V. Panneershelvam, M. Lanctot, S. Dieleman, D. Grewe, J. Nham, N. Kalch- brenner, I. Sutskever, T. P. Lillicrap, M. Leach, K. Kavukcuoglu, T. Graepel, and D. Hassabis. Mastering the game of Go with deep neural networks and tree search. Nature, 529(7587):484- 489, 2016.
  36. D. Silver, J. Schrittwieser, K. Simonyan, I. Antonoglou, A. Huang, A. Guez, T. Hubert, L. Baker, M. Lai, A. Bolton, et al. Mastering the game of go without human knowledge. Nature, 550(7676):354, 2017.
  37. R. S. Sutton and A. G. Barto. Reinforcement learning: An introduction, volume 1. Cambridge Univ Press, 1998.
  38. J. Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21-43, 2006.
  39. J. Urban. BliStr: The Blind Strategymaker. In G. Gottlob, G. Sutcliffe, and A. Voronkov, editors, Global Conference on Artificial Intelligence, GCAI 2015, volume 36 of EPiC Series in Computing, pages 312-319. EasyChair, 2015.
  40. J. Urban, G. Sutcliffe, P. Pudlák, and J. Vyskočil. MaLARea SG1 -Machine Learner for Au- tomated Reasoning with Semantic Guidance. In A. Armando, P. Baumgartner, and G. Dowek, editors, IJCAR, volume 5195 of LNCS, pages 441-456. Springer, 2008.
  41. J. Urban, J. Vyskočil, and P. Štěpánek. MaLeCoP: Machine learning connection prover. In K. Brünnler and G. Metcalfe, editors, TABLEAUX, volume 6793 of LNCS, pages 263-277. Springer, 2011.
  42. D. Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. CoRR, abs/1608.02644, 2016. · arXiv

Cited by

Sorted by citations

Metadata

Authors
Kaliszyk, C., Urban, J., Michalewski, H., & Olšák, M.
Affiliations
  • Universität Innsbruck (AT)
  • Czech Technical University in Prague (CZ)
  • University of Warsaw (PL)
ORCID
Venue
arXiv
Publisher
arXiv
Published
2018
Volume
31
Pages
8822-8833
ISSN
2331-8422 (ISSN-L)
DOI
10.48550/arxiv.1805.07563
arXiv
1805.07563
OpenAlex
W2804556168
Cited by
68
References
1
Citations by year
2026: 2 · 2025: 3 · 2024: 7 · 2023: 9 · 2022: 6 · 2021: 18 · 2020: 10 · 2019: 10 · 2018: 3
Type
posted content
Language
en
Open access
Licence
arxiv.org/licenses/nonexclusive-distrib/1.0/
Locations
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
  • neural information processing systems
Funders
European Regional Development Fund (02.1.01/0.0/0.0, CZ.02, CZ.02.1.01, CZ.02.1.01/0.0, CZ.02.1.01/0.0/0.0)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › AI-based Problem Solving and Planning
  • Physical Sciences › Computer Science › Software › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Artificial Intelligence › Artificial Intelligence Applications
Keywords
automated theorem proving, reinforcement learning, Monte Carlo tree search, mathematical problem solving

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review