Elamur Research⌕
☰
home / papers / 2019 / Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic

Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic

Paper · 2019 · Thibault Gauthier

Summary

The paper explores whether theorem-proving-style search can be guided by neural networks that teach themselves, rather than by hand-crafted heuristics. Gauthier builds a deep reinforcement learning framework directly inside the HOL4 proof assistant. Tree neural networks (TNNs) are used because their structure mirrors the tree shape of logical terms, and they are implemented over native HOL4 terms. Each task is cast as a single-player search problem. A TNN supplies a prior policy and value to a Monte Carlo Tree Search (MCTS), which replaces random roll-outs with these learned estimates. The improved search outcomes then train the next network generation, so no oracle or known solutions are needed. The framework is tested on two term synthesis tasks. One is building SK-combinators that behave like given λ-expressions in head-normal form. The other is finding polynomials whose Diophantine sets match target integer sets. The trained system solves 65% of combinator test problems, beating leading ATPs run with their best general strategies. On Diophantine problems it solves 78.5%, with solutions formally checked in HOL4. The work points toward learned term synthesis for interactive provers such as TacticToe.

Key points

  • Contributions include:
    • a TNN implementation with backpropagation;
    • a generic guided MCTS for arbitrary search problems;
    • sustained self-improvement over many generations;
    • an ATP comparison;
    • formal HOL4 verification of solutions.
  • Higher-order terms are turned into labeled trees by adding explicit apply and lam operators.
  • Combinator synthesis reached a 65% success rate, beating state-of-the-art ATPs. Diophantine equation synthesis reached 78.5%, which the paper describes as setting a precedent for statistically guided solving of this task.
  • The 157 Diophantine solutions found by MCTS on the test set were verified with a dedicated HOL4 procedure, DIOPH_PROVE. It checks equality of integer sets bounded below 16 by exhaustive case analysis modulo 16.
  • Planned future work includes:
    • additional tasks such as beta-reduction and higher-order unification;
    • joint training across tasks;
    • giving TacticToe the ability to synthesize tactic arguments.

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

 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 Thibault Gauthier. 2019. Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic. arXiv:1910.11797.

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

@misc{gauthier2019deep,
  title = {{Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic}},
  author = {Thibault Gauthier},
  year = {2019},
  doi = {10.48550/arxiv.1910.11797},
  eprint = {1910.11797},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1910.11797}
}

References

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

  1. David Auger, Adrien Couëtoux, and Olivier Teytaud. Continuous upper confidence trees with polynomial exploration - consistency. In Machine Learning and Knowledge Discovery in Databases - European Conference, ECML PKDD 2013, Prague, Czech Republic, September 23-27, 2013, Proceedings, Part I, pages 19… find
  2. Harald Baier. Efficient algorithms for generating elliptic curves over finite fields suitable for use in cryptography. PhD thesis, Darmstadt University of Technology, Germany, 2002. find
  3. Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 825–885. IOS Pres… find
  4. Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. Journal of Formalized Reasoning, 9(1):101–148, 2016. T. Gauthier Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic
  5. Jasmin Christian Blanchette and Tobias Nipkow. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pages 131–146, 2010. find
  6. C. B. Browne, E. Powley, D. Whitehouse, S. M. Lucas, P. I. Cowling, P. Rohlfshagen, S. Tavener, D. Perez, S. Samothrakis, and S. Colton. A survey of Monte Carlo tree search methods. IEEE Transactions on Computational Intelligence and AI in Games, 4(1):1–43, 2012. find
  7. Lukas Bulwahn. The new Quickcheck for Isabelle - random, exhaustive and symbolic testing under one roof. In Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings, pages 92–108, 2012. find
  8. Tianqi Chen and Carlos Guestrin. XGBoost: A scalable tree boosting system. In Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, San Francisco, CA, USA, August 13-17, 2016, pages 785–794, 2016. find
  9. Karel Chvalovský, Jan Jakubuv, Martin Suda, and Josef Urban. ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. In Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, pages 197– 215, 2019.
  10. Koen Claessen, Moa Johansson, Dan Rosén, and Nicholas Smallbone. Automating inductive proofs using theory exploration. In Maria Paola Bonacina, editor, Conference on Automated Deduction (CADE), volume 7898 of LNCS, pages 392–406. Springer, 2013. find
  11. Lukasz Czajka. Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions. In Jeremy Avigad and Adam Chlipala, editors, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016, pages 49–57. A… find
  12. Daniel Duverney. Number Theory: An Elementary Introduction Through Diophantine Problems, volume 4. World Scientific, 2010. find
  13. Laurent Fribourg. A superposition oriented theorem prover. Theor. Comput. Sci., 35:129–164, 1985. find
  14. Matthias Fuchs. Evolving combinators. In William McCune, editor, Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings, volume 1249 of Lecture Notes in Computer Science, pages 416–430. Springer, 199… find
  15. Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Xavier Leroy and Alwen Tiu, editors, Conference on Certified Programs and Proofs (CPP), pages 49–57. ACM, 2015. find
  16. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. TacticToe: Learning to reason with HOL4 tactics. In Thomas Eiter and David Sands, editors, Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), volume 46 of EPiC, pages 125–143. EasyChair, 2017. find
  17. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Learning to prove with tactics. CoRR, 2018. find
  18. Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3(2):153–245, 2010. find
  19. Erich Grädel. Definability on finite structures and the existence of one-way functions. Meth. of Logic in CS, 1(3):299–314, 1994. find
  20. Mohammadhosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom Melham, and Daniel Kroening. Deepsynth: Program synthesis for automatic task segmentation in deep reinforcement learning. CoRR, abs/1911.10244, 2019. — [arXiv:1911.10244](https://arxiv.org/abs/1911.10244) find
  21. Abusaleh M. Jabir, Dhiraj K. Pradhan, and Jimson Mathew. An efficient technique for synthesis and optimization of polynomials in gf(2 m ). In Soha Hassoun, editor, 2006 International Conference on Computer-Aided Design, ICCAD 2006, San Jose, CA, USA, November 5-9, 2006, pages 151– 157. ACM, 2006. T.… find
  22. Jan Jakubuv and Josef Urban. ENIGMA: efficient learning-based inference guiding machine. In Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings, pages 292–302, 2017.
  23. Jan Jakubuv and Josef Urban. Hammering Mizar by learning clause guidance. CoRR, abs/1904.01677, 2019. — [arXiv:1904.01677](https://arxiv.org/abs/1904.01677) find
  24. Mike S. Joy, Victor J. Rayward-Smith, and F. Warren Burton. Efficient combinator code. Comput. Lang., 10(3/4):211–224, 1985. find
  25. 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…
  26. Fadil Kallat, Tristan Schäfer, and Anna Vasileva. CLS-SMT: bringing together combinatory logic synthesis and satisfiability modulo theories. In Giselle Reis and Haniel Barbosa, editors, Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019, volum… find
  27. Eliyahu Kiperwasser and Yoav Goldberg. Easy-first dependency parsing with hierarchical tree LSTMs. TACL, 4:445–461, 2016. find
  28. Oleg Kiselyov. \łambda λ to ski, semantically - declarative pearl. In John P. Gallagher and Martin Sulzmann, editors, Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, 2018, Proceedings, volume 10818 of Lecture Notes in Computer Science, pages 33–5… find
  29. Laura Kovács and Andrei Voronkov. First-order theorem proving and vampire. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science,… find
  30. Mu Li, Tong Zhang, Yuqiang Chen, and Alexander J. Smola. Efficient mini-batch training for stochastic optimization. In The 20th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD ’14, New York, NY, USA - August 24 - 27, 2014, pages 661– 670, 2014. find
  31. Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, pages 85–105, 2017.
  32. J. V. MATIJASEVIC. Enumerable sets are diophantine. Soviet Math. Dokl., 11:354–358, 1970. find
  33. Jens Otten and Wolfgang Bibel. leanCoP: lean connection-based theorem proving. J. Symb. Comput., 36(1-2):139–161, 2003. find
  34. Lawrence C. Paulson and Jasmin C. Blanchette. Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers. In Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, editors, Workshop on the Implementation of Logics (IWIL), volume 2 of EPiC, pages… find
  35. Moses Schönfinkel. Über die bausteine der mathematischen logik. Mathematische annalen, 92(3-4):305–316, 1924. find
  36. Stephan Schulz. E - a brainiac theorem prover. AI Communications, 15(2-3):111–126, 2002. find
  37. David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, Yutian Chen, Timothy Lillicrap, Fan Hui, Laurent Sifre, George van den Driessche, Thore Graepel, and Demis Hassabis. Mastering the game of Go withou… find
  38. 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, Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 5170 of LNCS, pages 28–32. Springer, 2008. T. Gauthier Deep Reinforcement Learning for Synthesizing Fun… find
  39. Neil J. A. Sloane. The on-line encyclopedia of integer sequences. In Manuel Kauers, Manfred Kerber, Robert Miner, and Wolfgang Windsteiger, editors, Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 20… find
  40. Geoff Sutcliffe. The TPTP problem library and associated infrastructure. Journal of Automated Reasoning, 43(4):337–362, 2009. find
  41. Richard S. Sutton and Andrew G. Barto. Introduction to Reinforcement Learning. MIT Press, 1st edition, 1998. find
  42. Andrew M. Webb, Charles Reynolds, Dan-Andrei Iliescu, Henry W. J. Reeve, Mikel Luján, and Gavin Brown. Joint training of neural network ensembles. CoRR, abs/1902.04422, 2019. T. Gauthier — [arXiv:1902.04422](https://arxiv.org/abs/1902.04422) find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/gauthier-2019-deep-reinforcement-learning-synthesizing-functions/