Elamur Research⌕
☰
home / papers / 2019 / Generating Correctness Proofs with Neural Networks

Generating Correctness Proofs with Neural Networks

Paper · 2019 · Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul et al.

Summary

Foundational verification in interactive theorem provers such as Coq gives very strong guarantees about software, but writing the proofs takes a lot of expert labor. Verifying the CompCert compiler, for example, required about 6 person-years. The authors present Proverbot9001, which learns from existing human-written Coq proofs and uses the learned models to steer a depth-first tree search over proof commands. Their main design choice is to predict tactic arguments first and let those predictions shape tactic selection. Arguments are chosen by recurrent networks (GRU) that read goals and hypotheses as token sequences. The search also prunes branches that reach contexts no easier than ones already seen. Trained and tested on CompCert, the system proves about a fifth of held-out theorems on its own and more when paired with existing solvers. That is roughly four times the completion rate of the earlier learning-based approach, CoqGym. The work shows that domain-aware features and search can make machine-learned proof automation practical for real verification projects.

Key points

  • Data split: Training used proofs from 162 CompCert files, and testing used 13 files containing 501 theorem statements.
  • Without external solvers: Proverbot9001 completed 19.36% of test proofs (97/501), close to a 4X gain over CoqGym.
  • With solver-based tooling: Coverage rose to 28% (138/501), while the solvers alone managed only about 7%.
  • Prediction accuracy and proof length: The model matched the human tactic name 32% of the time, and given the right tactic it chose the correct argument 89% of the time. For original proofs of 10 commands or fewer, the solve rate was 35% (89/256). The longest proof it solved was originally 25 commands long.
  • Availability and transfer: The code is public (github.com/UCSD-PL/proverbot9001), and the system can be trained on one project and applied to a different one.

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 San DiegoSan Diego · United States101 works · 54,571 citations

 Fields, topics and concepts

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

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

Cite

Cite as Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul and Sorin Lerner. 2019. Generating Correctness Proofs with Neural Networks. arXiv:1907.07794.

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

@misc{sanchezstern2019generating,
  title = {{Generating Correctness Proofs with Neural Networks}},
  author = {Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul and Sorin Lerner},
  year = {2019},
  doi = {10.48550/arxiv.1907.07794},
  eprint = {1907.07794},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1907.07794}
}

References

41 references, 11 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, Geoffrey Irving, Christian Szegedy, and Josef Urban. 2016. DeepMath - Deep Sequence Models for Premise Selection. CoRR abs/1606.04442 (2016). arXiv:1606.04442 http://arxiv.org/abs/1606.04442 ↗
  2. Miltiadis Allamanis, Earl T. Barr, Premkumar T. Devanbu, and Charles A. Sutton. 2017. A Survey of Machine Learning for Big Code and Naturalness. CoRR abs/1709.06182 (2017). arXiv:1709.06182 http://arxiv.org/abs/1709.06182 ↗
  3. Andrew W. Appel. 2015. Verification of a Cryptographic Primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37, 2, Article 7 (April 2015), 31 pages. https://doi.org/10.1145/2701415 — [doi:10.1145/2701415](https://doi.org/10.1145/2701415) ↗
  4. Mislav Balunoviundefined, Pavol Bielik, and Martin Vechev. 2018. Learning to Solve SMT Formulas. In Proceedings of the 32nd International Conference on Neural Information Processing Systems (NIPS’18). Curran Associates Inc., Red Hook, NY, USA, 10338–10349. find
  5. Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. 2019. HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version). CoRR abs/1904.03241 (2019). arXiv:1904.03241 http://arxiv.org/abs/1904.03241 ↗
  6. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11). Springer-Verlag, Berlin, Heidelberg, 171–177. http://dl.acm.o… ↗
  7. Pavol Bielik, Veselin Raychev, and Martin Vechev. 2016. PHOG: Probabilistic Model for Code. In Proceedings of The 33rd International Conference on Machine Learning (Proceedings of Machine Learning Research), Maria Florina Balcan and Kilian Q. Weinberger (Eds.), Vol. 48. PMLR, New York, New York, USA… find
  8. Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay İleri, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2017. Verifying a High-performance Crash-safe File System Using a Tree Specification. In Proceedings of the 26th Symposium on Operating Systems Principles (SOSP ’17). ACM,… — [doi:10.1145/3132747.3132776](https://doi.org/10.1145/3132747.3132776) find
  9. Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press. find
  10. Kyunghyun Cho, Bart van Merrienboer, Çaglar Gülçehre, Fethi Bougares, Holger Schwenk, and Yoshua Bengio. 2014. Learning Phrase Representations using RNN Encoder-Decoder for Statistical Machine Translation. CoRR abs/1406.1078 (2014). arXiv:1406.1078 http://arxiv.org/abs/1406.1078 ↗
  11. Łukasz Czajka and Cezary Kaliszyk. 2018. Hammer for Coq: Automation for Dependent Type Theory. Journal of Automated Reasoning 61, 1 (01 Jun 2018), 423–453. https://doi.org/10.1007/s10817-018-9458-4 ↗
  12. Hoa Khanh Dam, Truyen Tran, and Trang Pham. 2016. A deep language model for software code. CoRR abs/1608.02715 (2016). arXiv:1608.02715 http://arxiv.org/abs/1608.02715 — [arXiv:1608.02715](https://arxiv.org/abs/1608.02715) ↗
  13. Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337–340. find
  14. Jean-Christophe Filliâtre, Hugo Herbelin, Bruno Barras, Bruno Barras, Samuel Boutin, Eduardo Giménez, Samuel Boutin, Gérard Huet, César Muñoz, Cristina Cornes, Cristina Cornes, Judicaël Courant, Judicael Courant, Chetan Murthy, Chetan Murthy, Catherine Parent, Catherine Parent, Christine Paulin-mohr… find
  15. Jonathan Frankle, Peter-Michael Osera, David Walker, and S Zdancewic. 2016. Example-directed synthesis: a type-theoretic interpretation. ACM SIGPLAN Notices 51 (01 2016), 802– 815. https://doi.org/10.1145/2914770.2837629 — [doi:10.1145/2914770.2837629](https://doi.org/10.1145/2914770.2837629) ↗
  16. Pranav Garg, Daniel Neider, P. Madhusudan, and Dan Roth. 2016. Learning Invariants Using Decision Trees and Implication Counterexamples. SIGPLAN Not. 51, 1 (Jan. 2016), 499–512. https://doi.org/10.1145/2914770.2837664 ↗
  17. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. 2017. TacticToe: Learning to Reason with HOL4 Tactics. In LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (EPiC Series in Computing), Thomas Eiter and David Sands (Eds.), Vol. 46. Easy-Chair,… find
  18. Sumit Gulwani. 2010. Dimensions in Program Synthesis. In PPDP ’10 Hagenberg, Austria (ppdp ’10 hagenberg, austria ed.). https://www.microsoft.com/en-us/research/publication/dimensions-program-synthesis/ ↗
  19. Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, and Ruzica Piskac. 2013. Complete Completion using Types and Weights. PLDI 2013 (2013), 12. 27–38. http://infoscience.epfl.ch/record/188990 ↗
  20. Jónathan Heras and Ekaterina Komendantskaya. 2014. ACL2(ml): Machine-Learning for ACL2. In Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014. 61– 75. https://doi.org/10.4204/EPTCS.152.5 — [doi:10.4204/eptcs.152.5](https://doi.org/10.4204/eptcs.152.5) ↗
  21. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. 2018. GamePad: A Learning Environment for Theorem Proving. CoRR abs/1806.00608 (2018). arXiv:1806.00608 http://arxiv.org/abs/1806.00608 ↗
  22. Cezary Kaliszyk, François Chollet, and Christian Szegedy. 2017. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. CoRR abs/1703.00426 (2017). arXiv:1703.00426 http://arxiv.org/abs/1703.00426 ↗
  23. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: Formal Verification of an OS Kernel. In Proceedings of the ACM SIGOPS 22Nd Symposi… find
  24. Ekaterina Komendantskaya, Jónathan Heras, and Gudmund Grov. 2012. Machine Learning in Proof General: Interfacing Interfaces. Electronic Proceedings in Theoretical Computer Science 118 (12 2012). https://doi.org/10.4204/EPTCS.118.2 — [doi:10.4204/eptcs.118.2](https://doi.org/10.4204/eptcs.118.2) ↗
  25. Ekaterina Komendantskaya and Kacper Lichota. 2012. Neural Networks for Proof-Pattern Recognition, Vol. 7553. 427–434. https://doi.org/10.1007/978-3-642-33266-1_53 — [doi:10.1007/978-3-642-33266-1_53](https://doi.org/10.1007/978-3-642-33266-1_53) ↗
  26. Laura Kovács and Andrei Voronkov. 2013. First-Order Theorem Proving and Vampire, Vol. 8044. 1–35. https://doi.org/10.1007/978-3-642-39799-8_1 ↗
  27. Daniel Kästner, Joerg Barrho, Ulrich Wünsche, Marc Schlick-ling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine Blazy. 2018. CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler. find
  28. Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (2009), 107–115. http://xavierleroy.org/publi/compcert-CACM.pdf ↗
  29. Fan Long, Peter Amidon, and Martin Rinard. 2017. Automatic inference of code transforms for patch generation. 727–739. https://doi.org/10.1145/3106237.3106253 — [doi:10.1145/3106237.3106253](https://doi.org/10.1145/3106237.3106253) ↗
  30. Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. 2017. Deep Network Guided Proof Search. CoRR abs/1701.06972 (2017). arXiv:1701.06972 http://arxiv.org/abs/1701.06972 ↗
  31. Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. 2010. Toward a Verified Relational Database Management System. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’10). ACM, New York, NY, USA, 237–248. https://doi.org/10.11… — [doi:10.1145/1706299.1706329](https://doi.org/10.1145/1706299.1706329) find
  32. Lili Mou, Ge Li, Zhi Jin, Lu Zhang, and Tao Wang. 2014. TBCNN: A Tree-Based Convolutional Neural Network for Programming Language Processing. CoRR abs/1409.5718 (2014). arXiv:1409.5718 http://arxiv.org/abs/1409.5718 ↗
  33. Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-example-directed Program Synthesis. SIGPLAN Not. 50, 6 (June 2015), 619–630. https://doi.org/10.1145/2813885.2738007 ↗
  34. Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. 2019. Graph Representations for Higher-Order Logic and Theorem Proving. CoRR abs/1905.10006 (2019). arXiv:1905.10006 http://arxiv.org/abs/1905.10006 ↗
  35. Lawrence C. Paulson. 1993. Natural Deduction as Higher-Order Resolution. CoRR cs.LO/9301104 (1993). http://arxiv.org/abs/cs.LO/9301104 — [arXiv:cs.lo/9301104](https://arxiv.org/abs/cs.lo/9301104) ↗
  36. Stephan Schulz. 2013. System Description: E 1.8. In Proc. of the 19th LPAR, Stellenbosch (LNCS), Ken McMillan, Aart Middeldorp, and Andrei Voronkov (Eds.), Vol. 8312. Springer. find
  37. Taro Sekiyama, Akifumi Imanishi, and Kohei Suenaga. 2017. Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic. CoRR abs/1706.06462 (2017). arXiv:1706.06462 http://arxiv.org/abs/1706.06462 — [arXiv:1706.06462](https://arxiv.org/abs/1706.06462) ↗
  38. O. Tange. 2011. GNU Parallel - The Command-Line Power Tool. ;login: The USENIX Magazine 36, 1 (Feb 2011), 42–47. http://www.gnu.org/s/parallel ↗
  39. James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. 2015. Verdi: A Framework for Implementing and Formally Verifying Distributed Systems. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLD… — [doi:10.1145/2737924.2737958](https://doi.org/10.1145/2737924.2737958) find
  40. Kaiyu Yang and Jia Deng. 2019. Learning to Prove Theorems via Interacting with Proof Assistants. CoRR abs/1905.09381 (2019). arXiv:1905.09381 http://arxiv.org/abs/1905.09381 ↗
  41. Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and Understanding Bugs in C Compilers. PLDI (2011).

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/stern-2019-generating-correctness-proofs-neural-networks/