Elamur Research⌕
☰
home / papers / 2018 / GamePad: A Learning Environment for Theorem Proving

GamePad: A Learning Environment for Theorem Proving

Paper · 2018 · Daniel Huang, Prafulla Dhariwal, Dawn Song et al.

Summary

Most deep learning work on theorem proving has targeted fully automated provers, for example premise selection, which run with almost no human guidance. This paper turns to interactive theorem provers, where experts build machine-checkable proofs step by step. These proofs are unambiguous and plentiful, which makes them a strong supervision signal. The authors present GamePad, a tool for the Coq proof assistant. It patches Coq's Ltac interpreter to log every intermediate proof state and exposes proofs to Python as structured objects: contexts, goals, tactic steps, proof trees and term ASTs. A thin wrapper around coqtop lets users build proofs interactively, for instance as a reinforcement learning environment. Treating proving as a game, the paper defines two tasks. Position evaluation estimates how many steps remain, and tactic prediction chooses the next step. A tactic predictor is used to synthesize proof scripts for a toy algebraic rewriting problem, and baseline models are trained on data from the Feit-Thompson formalization. The provided excerpt omits the quantitative results. The main value is open, reusable infrastructure for learning from human-written formal proofs.

Key points

  • GamePad is built on a patch to Coq 8.6.1 that also supports the SSreflect plugin. The patch leaves Coq's proof checker untouched, so proof verification stays trustworthy.
  • Proof states are recorded at two granularities. One splits sequenced tactics joined by ; into primitive tactics, and the other follows human proof-script steps ending in ..
  • Terms are available in Coq's mid-level language, which can drop implicit arguments and is closer to human proving, and its kernel-level language, which is closer to machine proving. Terms are stored in a shared form so that training scales to large datasets.
  • Data is drawn from the Feit-Thompson theorem formalization. A hand-crafted algebraic rewrite problem serves as a proof-synthesis demonstration.
  • Code, datasets, models and results are open source at github.com/ml4tp/gamepad.

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

🎓University of California, BerkeleyBerkeley · United States243 works · 251,774 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Daniel Huang, Prafulla Dhariwal, Dawn Song and Ilya Sutskever. 2018. GamePad: A Learning Environment for Theorem Proving. arXiv:1806.00608.

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

@misc{huang2018gamepad,
  title = {{GamePad: A Learning Environment for Theorem Proving}},
  author = {Daniel Huang, Prafulla Dhariwal, Dawn Song and Ilya Sutskever},
  year = {2018},
  doi = {10.48550/arxiv.1806.00608},
  eprint = {1806.00608},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1806.00608}
}

References

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

  1. Kyunghyun Cho, Bart van Merriënboer, Çalar Gülçehre, Dzmitry Bahdanau, Fethi Bougares, Holger Schwenk, and Yoshua Bengio. Learning Phrase Representations using RNN Encoder–Decoder for Statistical Machine Translation. In Proceedings of the 2014 Conference on Empirical Methods in Natural Language…
  2. Corinna Cortes and Vladimir Vapnik. Support-vector networks. Machine learning, 20(3):273–297, 1995.
  3. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337–340. Springer, 2008. find
  4. Hazel Duncan. The use of Data-Mining for the Automatic Formation of Tactics. PhD thesis, University of Edinburgh, 2002. find
  5. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. TacticToe: Learning to reason with HOL4 Tactics. In 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 46, pp. 125–143, 2017. find
  6. Georges Gonthier and Roux Stéphane Le. An Ssreflect Tutorial. Technical Report RT-0367, INRIA, 2009. URL https://hal.inria.fr/inria-00407778.6 Concurrent to our work, such techniques have been shown to work for tableau-based theorem provers (Kaliszyk et al., 2018). ↗
  7. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell OConnor, Sidi Ould Biha, et al. A machine-checked proof of the odd order theorem. In International Conference on Interactive Theorem Proving, pp. 163–179. Springe… find
  8. Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Een, Francois Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. In Advances in Neural Information Processing Systems, pp. 2235–2243, 2016.
  9. Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with flyspeck. Journal of Automated Reasoning, 53(2):173–213, 2014.
  10. Cezary Kaliszyk, François Chollet, and Christian Szegedy. Holstep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. In International Conference on Learning Representations (ICLR), 2017.
  11. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Mirek Olk. Reinforcement Learning of Theorem Proving. arXiv preprint arXiv:1805.07563, 2018.
  12. Diederik Kingma and Jimmy Ba. Adam: A method for stochastic optimization. Proceedings of the International Conference on Learning Representations 2015, 2015.
  13. Ekaterina Komendantskaya, Jónathan Heras, and Gudmund Grov. Machine Learning in Proof General: Interfacing Interfaces. arXiv preprint arXiv:1212.3618, 2012. — [arXiv:1212.3618](https://arxiv.org/abs/1212.3618) find
  14. Xavier Leroy et al. The compcert verified compiler. Documentation and users manual. INRIA Paris-Rocquencourt, 2012. find
  15. Moshe Looks, Marcello Herreshoff, DeLesley Hutchins, and Peter Norvig. Deep learning with dynamic computation graphs. Proceedings of the International Conference on Learning Representations 2017, 2017. find
  16. Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In LPAR, volume 46 of EPiC Series in Computing, pp. 85–105. EasyChair, 2017.
  17. Norman D. Megill. Metamath: A Computer Language for Mathematics. Lulu Press, Morrisville, North Carolina, — Regularizing and Optimizing LSTM Language Models http://us.metamath.org/downloads/metamath.pdf. Stephen Merity, Nitish Shirish Keskar, and Richard Socher. Regularizing and Optimizing LSTM Language Models. arXiv preprint arXiv:1708.02182, 2017. ↗
  18. Yutaka Nagashima and Yilun He. Pamper: Proof method recommendation system for isabelle/hol. arXiv preprint arXiv:1806.07239, 2018.
  19. Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary DeVito, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer. Automatic differentiation in PyTorch. In NIPS-W, 2017. find
  20. Illia Polosukhin and Maksym Zavershynskyi. Pytorch fold. https://github.com/nearai/pytorch-tools, 2018. ↗
  21. Tim Rocktäschel and Sebastian Riedel. End-to-end differentiable proving. In Advances in Neural Information Processing Systems, pp. 3791–3803, 2017.
  22. Stephan Schulz. E–a brainiac theorem prover. AI Communications, 15(2, 3):111–126, 2002. find
  23. Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a SAT Solver from Single-Bit Supervision. arXiv preprint arXiv:1802.03685, 2018.
  24. Nitish Srivastava, Geoffrey Hinton, Alex Krizhevsky, Ilya Sutskever, and Ruslan Salakhutdinov. Dropout: A Simple Way to Prevent Neural Networks from Overfitting. The Journal of Machine Learning Research, 15(1):1929–1958, 2014.
  25. Kai Sheng Tai, Richard Socher, and Christopher D. Manning. Improved semantic representations from tree-structured long short-term memory networks. In ACL (1), pp. 1556–1566. The Association for Computer Linguistics, 2015. find
  26. Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise Selection for Theorem Proving by Deep Graph Embedding. In Advances in Neural Information Processing Systems, pp. 2783–2793, 2017.
  27. Daniel Whalen. Holophrasm: a neural Automated Theorem Prover for higher-order logic. arXiv preprint arXiv:1608.02644, 2016.

Updated

↑ back to top

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