Elamur Research⌕
☰
home / papers / 2019 / Learning to Prove Theorems via Interacting with Proof Assistants

Learning to Prove Theorems via Interacting with Proof Assistants

Paper · 2019 · Kaiyu Yang and Jia Deng

Summary

Classical automated theorem provers work in first-order logic and build long, low-level resolution proofs. Human experts instead use proof assistants such as Coq, typing high-level tactics by hand. This paper asks whether a learned agent can do that interactive work instead. The authors release CoqGym, a dataset and interactive environment built from 71K human-written proofs in 123 open-source Coq projects. The projects cover mathematics, programming languages and hardware verification. CoqGym also adds shorter synthetic proofs taken from intermediate goals of the original proofs. The authors also propose ASTactic, a neural model that encodes the goal and premises with a TreeLSTM. It then builds a tactic as an abstract syntax tree that follows a grammar for part of Coq's tactic language. Because of this, it can produce tactics and arguments that never appeared word for word in training. ASTactic proves 12.2% of test theorems, compared with 4.9% for Coq's built-in automation. Combined with external ATP systems, the success rate reaches 30.0%. The work matters because it gives a large, varied benchmark and shows that generating tactics as structured programs works well for formal proof search.

Key points

  • CoqGym contains 71K proofs from 123 Coq projects (3,061 Coq files). This is much larger than GamePad (1,602 Feit–Thompson theorems) and covers more domains than HOList (29K proofs, all from the Kepler conjecture formalization).
  • The environment returns the new goals after each tactic. A proof counts as complete when no goals remain. Synthetic training proofs come from turning unsolved subgoals into premises and finishing them with auto.
  • ASTactic uses a TreeLSTM to encode goals and premises. It builds tactics top-down from a grammar with about 50 tactic types (e.g., apply, induction, rewrite, destruct) and fills in arguments from the identifiers available in the current context.
  • On the test set, ASTactic proves 12.2% of theorems, compared with 4.9% for built-in tactics such as auto, intuition and easy. Combined with ATPs (Z3, CVC4, Vampire, E), it reaches 30.0%, including theorems that earlier automatic methods could not prove.
  • Code and data: github.com/princeton-vl/CoqGym (ICML 2019).

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

🎓Princeton UniversityPrinceton · United States113 works · 48,612 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksComputational Theory and Mathematics · 321 works

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

Cite

Cite as Kaiyu Yang and Jia Deng. 2019. Learning to Prove Theorems via Interacting with Proof Assistants. arXiv:1905.09381.

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

@misc{yang2019learning,
  title = {{Learning to Prove Theorems via Interacting with Proof Assistants}},
  author = {Kaiyu Yang and Jia Deng},
  year = {2019},
  doi = {10.48550/arxiv.1905.09381},
  eprint = {1905.09381},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1905.09381}
}

References

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

  1. Allamanis, M., Chanthirasegaran, P., Kohli, P., and Sutton, C. Learning continuous semantic representations of symbolic expressions. arXiv preprint arXiv:1611.01423, 2016a. find
  2. Allamanis, M., Peng, H., and Sutton, C. A convolutional attention network for extreme summarization of source code. In International Conference on Machine Learning, pp. 2091–2100, 2016b.
  3. Allamanis, M., Brockschmidt, M., and Khademi, M. Learning to represent programs with graphs. arXiv preprint arXiv:1711.00740, 2017.
  4. Alon, U., Zilberstein, M., Levy, O., and Yahav, E. code2vec: Learning distributed representations of code. arXiv preprint arXiv:1803.09473, 2018. find
  5. Balunovic, M., Bielik, P., and Vechev, M. Learning to solve smt formulas. In Advances in Neural Information Processing Systems, pp. 10317–10328, 2018. find
  6. Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pak, K., and Urban, J. Mizar: State-of-the-art and beyond. In Conferences on Intelligent Computer Mathematics, pp. 261–279. Springer, 2015. find
  7. Bansal, K., Loos, S. M., Rabe, M. N., Szegedy, C., and Wilcox, S. Holist: An environment for machine learning of higher-order theorem proving (extended version). arXiv preprint arXiv:1904.03241, 2019.
  8. Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.-C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C., et al. The Coq proof assistant reference manual: Version 6.1. PhD thesis, Inria, 1997. find
  9. Barrett, C., Conway, C. L., Deters, M., Hadarean, L., Jo-vanovi’c, D., King, T., Reynolds, A., and Tinelli, C. CVC4. In Gopalakrishnan, G. and Qadeer, S. (eds.), Proceedings of the 23rd International Conference on Computer Aided Verification (CAV ’11), volume 6806 of Lecture Notes in Computer Scienc… find
  10. Bordes, A., Boureau, Y.-L., and Weston, J. Learning end-to-end goal-oriented dialog. arXiv preprint arXiv:1605.07683, 2016. find
  11. Bridge, J. P., Holden, S. B., and Paulson, L. C. Machine learning for first-order theorem proving. Journal of automated reasoning, 53(2):141–172, 2014. find
  12. Brockschmidt, M., Allamanis, M., Gaunt, A. L., and Polozov, O. Generative code modeling with graphs. In International Conference on Learning Representations, 2019. URL https://openreview.net/forum?id=Bke4KsA5FX. ↗
  13. Cho, K., Van Merriënboer, B., Gulcehre, C., Bahdanau, D., Bougares, F., Schwenk, H., and Bengio, Y. Learning phrase representations using rnn encoder-decoder for statistical machine translation. arXiv preprint arXiv:1406.1078, 2014.
  14. Czajka, Ł. and Kaliszyk, C. Hammer for coq: Automation for dependent type theory. Journal of Automated Reasoning, 61(1-4):423–453, 2018. find
  15. Darvas, Á., Hähnle, R., and Sands, D. A theorem proving approach to analysis of secure information flow. In International Conference on Security in Pervasive Computing, pp. 193–209. Springer, 2005. find
  16. De Moura, L. and Bjørner, N. 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
  17. Delahaye, D. A tactic language for the system coq. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 85–95. Springer, 2000. find
  18. Dixon, L. and Fleuriot, J. Isaplanner: A prototype proof planner in isabelle. In International Conference on Automated Deduction, pp. 279–283. Springer, 2003. find
  19. Gallego Arias, E. J. SerAPI: Machine-Friendly, Data-Centric Serialization for Coq. Technical report, MINES ParisTech, October 2016. URL https://hal-mines-paristech.archives-ouvertes.fr/hal-01384408. ↗
  20. Gauthier, T., Kaliszyk, C., Urban, J., Kumar, R., and Norrish, M. Learning to prove with tactics. arXiv preprint arXiv:1804.00596, 2018. find
  21. Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., OConnor, R., Biha, S. O., et al. A machine-checked proof of the odd order theorem. In International Conference on Interactive Theorem Proving, pp. 163–179. Springer, 2013. find
  22. Gransden, T., Walkinshaw, N., and Raman, R. Sepia: search for proofs using inferred automata. In International Conference on Automated Deduction, pp. 246–255. Springer, 2015. find
  23. Hales, T., Adams, M., Bauer, G., Dang, T. D., Harrison, J., Le Truong, H., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T. T., et al. A formal proof of the kepler conjecture. In Forum of Mathematics, Pi, volume 5. Cambridge University Press, 2017. find
  24. Harrison, J. Hol light: A tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design, pp. 265–269. Springer, 1996. find
  25. Harrison, J., Urban, J., and Wiedijk, F. History of interactive theorem proving. In Computational Logic, volume 9, pp. 135–214, 2014. find
  26. Hindle, A., Barr, E. T., Su, Z., Gabel, M., and Devanbu, P. On the naturalness of software. In Software Engineering (ICSE), 2012 34th International Conference on, pp. 837– 847. find
  27. Huang, D., Dhariwal, P., Song, D., and Sutskever, I. Gamepad: A learning environment for theorem proving. In International Conference on Learning Representations, 2019. URL https://openreview.net/forum?id=r1xwKoR9Y7. ↗
  28. Irving, G., Szegedy, C., Alemi, A. A., Eén, N., Chollet, F., and Urban, J. Deepmath-deep sequence models for premise selection. In Advances in Neural Information Processing Systems, pp. 2235–2243, 2016.
  29. Kaliszyk, C. and Urban, J. Learning-assisted automated reasoning with flyspeck. Journal of Automated Reasoning, 53(2):173–213, 2014.
  30. Kaliszyk, C., Urban, J., Michalewski, H., and Olšák, M. Reinforcement learning of theorem proving. arXiv preprint arXiv:1805.07563, 2018. find
  31. Kern, C. and Greenstreet, M. R. Formal verification in hardware design: a survey. ACM Transactions on Design Automation of Electronic Systems (TODAES), 4(2):123– 193, 1999. find
  32. Kovács, L. and Voronkov, A. First-order theorem proving and vampire. In International Conference on Computer Aided Verification, pp. 1–35. Springer, 2013. find
  33. Leroy, X. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009. find
  34. Liu, B., Tur, G., Hakkani-Tur, D., Shah, P., and Heck, L. End-to-end optimization of task-oriented dialogue model with deep reinforcement learning. arXiv preprint arXiv:1711.10712, 2017. — [arXiv:1711.10712](https://arxiv.org/abs/1711.10712) find
  35. Loos, S., Irving, G., Szegedy, C., and Kaliszyk, C. Deep network guided proof search. arXiv preprint arXiv:1701.06972, 2017.
  36. McCarthy, J. Recursive functions of symbolic expressions and their computation by machine, part i. Communications of the ACM, 3(4):184–195, 1960. find
  37. McCune, W. Solution of the robbins problem. Journal of Automated Reasoning, 19(3):263–276, 1997. find
  38. Parisotto, E., Mohamed, A.-r., Singh, R., Li, L., Zhou, D., and Kohli, P. Neuro-symbolic program synthesis. arXiv preprint arXiv:1611.01855, 2016.
  39. Paulin-Mohring, C. Circuits as streams in coq: Verification of a sequential multiplier. In International Workshop on Types for Proofs and Programs, pp. 216–230. Springer, 1995. find
  40. Paulson, L. C. Isabelle: A generic theorem prover, volume 828. Springer Science & Business Media, 1994. find
  41. Paulson, L. C. and Blanchette, J. C. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In PAAR@ IJCAR, pp. 1–10, 2010. find
  42. Rocktäschel, T. and Riedel, S. End-to-end differentiable proving. In Advances in Neural Information Processing Systems, pp. 3788–3800, 2017.
  43. Schulz, S. System description: E 1.8. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 735–743. Springer, 2013. find
  44. Sutcliffe, G. The tptp problem library and associated infrastructure. Journal of Automated Reasoning, 43(4):337, 2009. find
  45. Tai, K. S., Socher, R., and Manning, C. D. Improved semantic representations from tree-structured long short-term memory networks. arXiv preprint arXiv:1503.00075, 2015. find
  46. Tieleman, T. and Hinton, G. Lecture 6.5—RmsProp: Divide the gradient by a running average of its recent magnitude. COURSERA: Neural Networks for Machine Learning, 2012. find
  47. Urban, J. Mptp–motivation, implementation, first experiments. Journal of Automated Reasoning, 33(3-4):319– 339, 2004. find
  48. Urban, J., Vyskočil, J., and Štěpánek, P. Malecop machine learning connection prover. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pp. 263–277. Springer, 2011. find
  49. Wang, M., Tang, Y., Wang, J., and Deng, J. Premise selection for theorem proving by deep graph embedding. In Advances in Neural Information Processing Systems, pp. 2786–2796, 2017. find
  50. Williams, R. J. and Zipser, D. A learning algorithm for continually running fully recurrent neural networks. Neural computation, 1(2):270–280, 1989. find
  51. Yin, P. and Neubig, G. A syntactic neural model for general-purpose code generation. arXiv preprint arXiv:1704.01696, 2017.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/yang-2019-learning-prove-theorems-interacting-proof/