Elamur Research⌕
☰
home / papers / 2018 / Reinforcement Learning of Theorem Proving

Reinforcement Learning of Theorem Proving

Paper · 2018 · Cezary Kaliszyk, Josef Urban, Henryk Michalewski et al.

Summary

The paper asks whether a first-order theorem prover can learn its proof-search strategy from experience instead of relying on hand-crafted heuristics. The authors begin with mlCoP, an OCaml version of the connection-tableau prover leanCoP. They remove iterative deepening, which yields a deliberately incomplete "bare" prover that picks inferences at random. They then add three things: Monte-Carlo tree search driven by the UCT formula, a learned policy that estimates prior probabilities for inferences, and a learned value function that scores tableaux. The resulting system, rlCoP, repeatedly alternates between proving and learning on Mizar problems taken from the Miz40 dataset. Only training problems feed the learning, and evaluation uses held-out problems. Untrained, rlCoP is much weaker than standard mlCoP. After a few iterations, however, it solves over 40% more unseen problems under an equal inference budget. Typical published gains in the field are 3–10%, so this result suggests reinforcement learning can work for general mathematical reasoning at scale with almost no domain engineering.

Key points

  • Training and evaluation: rlCoP was trained on data from iterations 0–4 and then proved 1624 test problems in the 5th iteration. That is 42.1% more than mlCoP achieved with the same inference limit.
  • Overlap with the baseline: after 10 iterations, rlCoP solved 577 test problems that mlCoP could not, while mlCoP solved 96 that rlCoP missed, for a net gain of 481. Some of rlCoP's proofs, such as WAYBEL_0:28, TOPREALC:10 and FUNCOP_1:34, were out of reach for mlCoP even at 4 million inferences.
  • Default value heuristic: before the learned value function is introduced, a leaf is scored as 0.95 raised to the number of open goals. This rewards tableaux with fewer unclosed branches.
  • Tuned settings: a small grid search set the UCT exploration constant c to 2 (with learned guidance) and the policy softmax temperature to 2.5. Training examples come only from bigstep nodes.
  • Comparison with AlphaZero-style selection: using AlphaZero-style PUCT instead of UCT made practically no difference to the results.

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

🎓Charles UniversityPrague · Czechia135 works · 21,106 citations🎓Universität InnsbruckInnsbruck · Austria23 works · 1,475 citations🎓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 Cezary Kaliszyk, Josef Urban, Henryk Michalewski and Mirek Olšák. 2018. Reinforcement Learning of Theorem Proving. arXiv:1805.07563.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.1805.07563 · arXiv 1805.07563

@misc{kaliszyk2018reinforcement,
  title = {{Reinforcement Learning of Theorem Proving}},
  author = {Cezary Kaliszyk, Josef Urban, Henryk Michalewski and Mirek Olšák},
  year = {2018},
  doi = {10.48550/arxiv.1805.07563},
  eprint = {1805.07563},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1805.07563}
}

References

44 references, 10 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. A. A. Alemi, F. Chollet, N. Eén, G. Irving, C. Szegedy, 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…
  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 Conference on Neural Informati…
  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. find
  5. C. W. Barrett, R. Sebastiani, S. A. Seshia, C. Tinelli, et al. Satisfiability modulo theories. Handbook of satisfiability, 185:825–885, 2009. find
  6. 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. find
  7. J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban. Hammering towards QED. J. Formalized Reasoning, 9(1):101–148, 2016.
  8. 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. find
  9. 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. find
  10. 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. find
  11. 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. find
  12. 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, Artificial Intelligence and Reasoning, LPAR-21, volume 46 of EPiC Series in Computing, pages 125–143. EasyChair, 2017. find
  13. A. Grabowski, A. Korniłowicz, and A. Naumowicz. Mizar in a nutshell. J. Formalized Reasoning, 3(2):153–245, 2010. find
  14. 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. find
  15. R. Hähnle. Tableaux and related methods. In Robinson and Voronkov [34], pages 100–178. find
  16. 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. find
  17. 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. S…
  18. C. Kaliszyk and J. Urban. Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning, 53(2):173–213, 2014.
  19. 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, pag… find
  20. C. Kaliszyk and J. Urban. MizAR 40 for Mizar 40. J. Autom. Reasoning, 55(3):245–256, 2015.
  21. C. Kaliszyk, J. Urban, and J. Vyskočil. Machine learner for automated reasoning 0.4 and 0.5. 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. EasyCh… find
  22. 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. find
  23. 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. find
  24. D. Kühlwein, T. van Laarhoven, E. Tsivtsivadze, J. Urban, and T. Heskes. Overview and evaluation 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. find
  25. 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. find
  26. 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, Artificial Intelligence and Reasoning, LPAR-21, volume 46 of EPiC Series in Computing, pages 85–105. EasyChair, 2017.
  27. W. McCune. Otter 2.0. In International Conference on Automated Deduction, pages 663–664. Springer, 1990. find
  28. J. Meng and L. C. Paulson. Translating higher-order clauses to first-order clauses. J. Autom. Reasoning, 40(1):35–60, 2008. find
  29. J. Otten. Restricting backtracking in connection calculi. AI Commun., 23(2-3):159–182, 2010. find
  30. J. Otten and W. Bibel. leanCoP: lean connection-based theorem proving. J. Symb. Comput., 36(1-2):139–161, 2003. find
  31. F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. Scikit-learn: Machine learning in Python. Journal of Machine Learning Research, 12:2825–2830… find
  32. B. Piotrowski and J. Urban. ATPboost: Learning premise selection in binary setting with ATP feedback. CoRR, abs/1802.03375, 2018. — [arXiv:1802.03375](https://arxiv.org/abs/1802.03375) find
  33. J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM (JACM), 12(1):23–41, 1965. find
  34. J. A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press, 2001. find
  35. 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. find
  36. 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. Kalchbrenner, I. Sutskever, T. P. Lillicrap, M. Leach, K. Kavukcuoglu, T. Graepel, and D. Hassabis. Mastering the game of G… find
  37. D. Silver, T. Hubert, J. Schrittwieser, I. Antonoglou, M. Lai, A. Guez, M. Lanctot, L. Sifre, D. Kumaran, T. Graepel, T. P. Lillicrap, K. Simonyan, and D. Hassabis. Mastering chess and shogi by self-play with a general reinforcement learning algorithm. CoRR, abs/1712.01815, 2017.
  38. 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. find
  39. R. S. Sutton and A. G. Barto. Reinforcement learning: An introduction, volume 1. Cambridge Univ Press, 1998. find
  40. J. Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. find
  41. 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. find
  42. J. Urban, G. Sutcliffe, P. Pudlák, and J. Vyskočil. MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In A. Armando, P. Baumgartner, and G. Dowek, editors, IJCAR, volume 5195 of LNCS, pages 441–456. Springer, 2008. find
  43. 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. find
  44. D. Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. CoRR, abs/1608.02644, 2016.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/kaliszyk-2018-reinforcement-learning-theorem-proving/