Elamur Research⌕
☰
home / papers / 2019 / Learning to Reason in Large Theories without Imitation

Learning to Reason in Large Theories without Imitation

Paper · 2019 · Kshitij Bansal, Christian Szegedy, Markus N. Rabe et al.

Summary

Automated theorem proving in large formal libraries is hard mainly because, at every proof step, the prover must choose a few useful premises (earlier theorems and lemmas) from about 10,000 candidates. Earlier neural provers learned this choice from human-written proofs, which an open-ended reasoning system cannot depend on. The authors train a prover for HOL Light in the HOList environment using only reinforcement learning. They reuse the GNN-based tactic and premise scoring model of Paliwal et al. [2020]. Their key addition is an exploration step: alongside the top-k1 premises ranked by the current model, the prover interleaves k2 extra premises retrieved by a tf-idf similarity lookup. Successful proofs are then pruned so that only truly needed premises become training data. Without this exploration, an RL loop with no human data stalls. With it, the prover outperforms a purely imitation-trained model and nearly matches a system that combines human proofs with RL. This shows that premise selection can be learned without human demonstrations.

Key points

  • Results on a single checkpoint (8M training steps):
    • ZERO EXPLORE, with no human proofs, proves 56.3% of validation theorems.
    • The state-of-the-art pure-imitation GNN model proves 49.95%.
    • HUMAN EXPLORE, which uses human proofs plus RL, proves 59.9%.
  • Cumulative results: ZERO EXPLORE reaches about 64% versus 69.1% for the human-assisted loop. This is over 90% of the human-assisted performance.
  • Baseline without exploration: ZERO REFERENCE, the original Bansal et al. [2019] RL setup run without human data, fails to find new proofs and stalls.
  • Hand-engineered retrieval alone: Selecting premises only with hand-engineered metrics (k1 = 0) proves about 43% cumulatively.
  • Seeding instead of exploring: ZERO SEEDED starts from roughly 20% of training theorems proven by heuristics. It avoids stalling but stays below continuous exploration.
  • Minor ablations:
    • 10% token dropout in the exploration lookup gives at most a marginal gain.
    • Adding exploration to the human-data loop changes little.

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

🏢GoogleMountain View · United States533 works · 443,885 citations🎓Institute of Science and Technology AustriaKlosterneuburg · Austria5 works · 382 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 Kshitij Bansal, Christian Szegedy, Markus N. Rabe, Sarah M. Loos and Viktor Toman. 2019. Learning to Reason in Large Theories without Imitation. arXiv:1905.10501.

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

@misc{bansal2019learning,
  title = {{Learning to Reason in Large Theories without Imitation}},
  author = {Kshitij Bansal, Christian Szegedy, Markus N. Rabe, Sarah M. Loos and Viktor Toman},
  year = {2019},
  doi = {10.48550/arxiv.1905.10501},
  eprint = {1905.10501},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1905.10501}
}

References

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

  1. Alexander A. Alemi, François Chollet, Niklas Eén, Geoffrey Irving, Christian Szegedy, and Josef Urban. Deepmath - deep sequence models for premise selection. In Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett, editors, Advances in Neural Information Processing…
  2. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. TacticToe: Learning to reason with HOL4 tactics. In Thomas Eiter and David Sands, editors, LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46 of EPiC Se… find
  3. EasyChair, 2017. URL https://easychair.org/publications/volume/LPAR-21. ↗
  4. Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In Thomas Eiter and David Sands, editors, LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46 of EPiC S…
  5. EasyChair, 2017. URL https://easychair.org/publications/paper/ND13. ↗
  6. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. GamePad: A learning environment for theorem proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019.
  7. OpenReview.net, 2019. URL https://openreview.net/forum?id=r1xwKoR9Y7. ↗
  8. Kshitij Bansal, Sarah M Loos, Markus N Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of higher-order theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9…
  9. PMLR, 2019. URL http://proceedings.mlr.press/v97/bansal19a/bansal19a.pdf. ↗
  10. Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, New York, NY, USA, February 7-12, 2020.
  11. AAAI Press, 2020. ISBN 978-1-57735-823-7. URL https://www.aaai.org/Papers/AAAI/2020GB/AAAI-PaliwalA.9149.pdf. ↗
  12. Dennis Lee, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Kshitij Bansal. Mathematical reasoning in latent space. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020.
  13. OpenReview.net, 2020. URL https://openreview.net/forum?id=Ske31kBtPr. ↗
  14. Christopher D. Manning, Prabhakar Raghavan, and Hinrich Schütze. Introduction to Information Retrieval. Cambridge University Press, 2008. ISBN 978-0-521-86571-5. find
  15. Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Alex Graves, Ioannis Antonoglou, Daan Wierstra, and Martin A. Riedmiller. Playing atari with deep reinforcement learning. CoRR, abs/1312.5602, 2013. URL http://arxiv.org/abs/1312.5602. ↗
  16. David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al. Mastering the game of go without human knowledge. Nature, 550(7676):354, 2017. find
  17. Oriol Vinyals, Igor Babuschkin, Wojciech M Czarnecki, Michaël Mathieu, Andrew Dudzik, Junyoung Chung, David H Choi, Richard Powell, Timo Ewalds, Petko Georgiev, Junhyuk Oh, Dan Horgan, Manuel Kroiss, Ivo Danihelka, Aja Huang, Laurent Sifre, Trevor Cai, John P Agapiou, Max Jaderberg, Alexander S Vezh… find
  18. Rein Houthooft, Xi Chen, Yan Duan, John Schulman, Filip De Turck, and Pieter Abbeel. VIME: variational information maximizing exploration. In Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett, editors, Advances in Neural Information Processing Systems 29: Annual… find
  19. Yuri Burda, Harrison Edwards, Deepak Pathak, Amos J. Storkey, Trevor Darrell, and Alexei A. Efros. Large-scale study of curiosity-driven learning. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. find
  20. OpenReview.net, 2019. URL https://openreview.net/forum?id=rJNwDjAqYX. ↗
  21. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning, 52(2):191–213, 2014. URL https://doi.org/10.1007/s10817-013-9286-5. ↗
  22. Cezary Kaliszyk and Josef Urban. Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput., 69:109–128, 2015. URL https://doi.org/10.1016/j.jsc.2014.09.032. — [doi:10.1016/j.jsc.2014.09.032](https://doi.org/10.1016/j.jsc.2014.09.032) ↗
  23. Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban. A learning-based fact selector for Isabelle/HOL. Journal of Automated Reasoning, 57(3):219–244, 2016. URL https://doi.org/10.1007/s10817-016-9362-8. — [doi:10.1007/s10817-016-9362-8](https://doi.org/10.1007/s10817-016-9362-8) ↗
  24. Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett, editors, Advances in Neural Information Processing Systems 30:…
  25. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings o…
  26. PMLR, 2019. URL http://proceedings.mlr.press/v97/yang19a/yang19a.pdf. ↗
  27. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olsák. Reinforcement learning of theorem proving. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett, editors, Advances in Neural Information Processing Systems 31: Annual Conferenc…
  28. Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban. Towards finding longer proofs. CoRR, abs/1905.13100, 2019. URL http://arxiv.org/abs/1905.13100. ↗
  29. Zsolt Zombori, Josef Urban, and Chad E. Brown. Prolog technology reinforcement learning prover. CoRR, abs/2004.06997, 2020. URL https://arxiv.org/abs/2004.06997. — [arXiv:2004.06997](https://arxiv.org/abs/2004.06997) ↗
  30. John Harrison. HOL Light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri, editors, Formal Methods in Computer-Aided Design, First International Conference, FMCAD ’96, Palo Alto, California, USA, November 6-8, 1996, Proceedings, volume 1166 of Lecture Notes in Computer Scien… find
  31. Springer, 1996. URL https://doi.org/10.1007/BFb0031795. — [doi:10.1007/bfb0031795](https://doi.org/10.1007/bfb0031795) ↗
  32. Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. Generating correctness proofs with neural networks. CoRR, abs/1907.07794, 2019. URL http://arxiv.org/abs/1907.07794. ↗
  33. Coq. The Coq Proof Assistant, 1989. URL http://coq.inria.fr. ↗
  34. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Comput… find
  35. Springer, 2008. URL https://doi.org/10.1007/978-3-540-71067-7_6. — [doi:10.1007/978-3-540-71067-7_6](https://doi.org/10.1007/978-3-540-71067-7_6) ↗
  36. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A formal proof of the kepler conjecture. In Forum of Mathematics, Pi, volume 5. Cambridge University Press, 2017. URL https://www.cambridge… ↗
  37. Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The isabelle framework. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Le…
  38. Springer, 2008. URL https://doi.org/10.1007/978-3-540-71067-7_7. ↗
  39. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015,… find
  40. Springer, 2015. URL https://doi.org/10.1007/978-3-319-21401-6. — [doi:10.1007/978-3-319-21401-6](https://doi.org/10.1007/978-3-319-21401-6) ↗
  41. Gil Lederman, Markus N. Rabe, Sanjit Seshia, and Edward A. Lee. Learning heuristics for quantified boolean formulas through reinforcement learning. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. find
  42. OpenReview.net, 2020. URL https://openreview.net/forum?id=BJluxREKDB. ↗
  43. Georges Gonthier. Formal proof–the four-color theorem. Notices of the AMS, 55(11):1382–1393, 2008. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/bansal-2019-learning-reason-large-theories-without/