Elamur Research⌕
☰
home / papers / 2024 / Graph2Tac: Online Representation Learning of Formal Math Concepts

Graph2Tac: Online Representation Learning of Formal Math Concepts

Paper · 2024 · Lasse Blaauwbroek, Miroslav Olšák, Jason Rute et al.

Summary

The paper tackles a practical gap in machine-learning provers for Coq: models trained offline cannot easily handle the new definitions, lemmas and proofs that appear when working in an unfamiliar formalization project. The authors argue that items located close together in a library tend to be mutually relevant and often have similar proofs, so a solver that learns on the fly should beat one frozen after training. They test this inside the Tactician platform, which encodes all Coq kernel objects and proof states as one large interconnected graph. They study two online solvers. The first is Tactician's existing k-NN, which learns from recent proof scripts. The second is Graph2Tac, a new GNN with an extra training objective: it learns to compute embeddings for unseen definitions from their graphs, building them hierarchically on top of the embeddings of their components. Evaluated on theorems from Coq packages never seen in training, both online solvers clearly outperform their offline counterparts and existing Coq provers. Because they exploit different kinds of new data, combining them helps further. The work shows that online representation learning matters for real-world proof automation.

Key points

  • The online k-NN raises the share of proved theorems from 15.0% to 25.8% (1.72×) over its offline version. It only looks at the 1000 latest tactic steps and needs no training.
  • Graph2Tac's definition-embedding task improves results from 17.4% to 26.1% (about 1.5×). The online advantage is largest for theorems with 10 or more dependencies unseen in training.
  • Combining Graph2Tac and k-NN proves 33.2% of the test set, roughly 1.27× better than either solver on its own.
  • Both online solvers beat CoqHammer, Proverbot9001, a transformer baseline, ASTactic, TacTok and Passport by at least 1.48×. The main benchmark gives each theorem a 10-minute limit.
  • Graph2Tac is integrated into Tactician, so Coq end-users can actually run it. The code is public and the experiments are reproducible (ICML 2024).

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

🏢IBMArmonk · United States163 works · 73,139 citations🎓Radboud University NijmegenNijmegen · Netherlands26 works · 2,125 citations🎓Czech Technical University in PraguePrague · Czechia16 works · 930 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

Cite

Cite as Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock and Vasily Pestun. 2024. Graph2Tac: Online Representation Learning of Formal Math Concepts. arXiv:2401.02949.

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

@misc{blaauwbroek2024graph2tac,
  title = {{Graph2Tac: Online Representation Learning of Formal Math Concepts}},
  author = {Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock and Vasily Pestun},
  year = {2024},
  doi = {10.48550/arxiv.2401.02949},
  eprint = {2401.02949},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2401.02949}
}

References

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

  1. Martı́n Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenbe… find
  2. Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner. A modular integration of SAT/SMT solvers to coq through proof witnesses. In Jean-Pierre Jouannaud and Zhong Shao (eds.), Certified Programs and Proofs - First International Conference, CPP 2011,… find
  3. Springer, 2011. doi: 10.1007/978-3-642-25379-9\\ 12. URL https://doi.org/10.1007/978-3-642-25379-9_12. — [doi:10.1007/978-3-642-25379-9\](https://doi.org/10.1007/978-3-642-25379-9\) ↗
  4. Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning, ICML 2… — HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
  5. PMLR, 2019. URL http://proceedings.mlr.press/v97/bansal19a.html. ↗
  6. Frédéric Besson. Itauto: An extensible intuitionistic SAT solver. In Liron Cohen and Cezary Kaliszyk (eds.), 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), volume 193 of LIPIcs, pp. 9:1–9:18. Schloss Dagstuhl - Lei… — [doi:10.4230/lipics.itp.2021.9](https://doi.org/10.4230/lipics.itp.2021.9) find
  7. Lasse Blaauwbroek. Tactician’s web of large-scale formal knowledge, December 2023. URL https://doi.org/10.5281/zenodo.10028721. — [doi:10.5281/zenodo.10028721](https://doi.org/10.5281/zenodo.10028721) ↗
  8. Lasse Blaauwbroek. The Tactician’s web of large-scale formal knowledge. arXiv preprint, January 2024. doi: 10.48550/arXiv.2401.02950. URL https://doi.org/10.48550/arXiv.2401.02950. — [doi:10.48550/arxiv.2401.02950](https://doi.org/10.48550/arxiv.2401.02950) ↗
  9. Lasse Blaauwbroek, Josef Urban, and Herman Geuvers. Tactic learning and proving for the coq proof assistant. In Elvira Albert and Laura Kovács (eds.), LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 7… find
  10. EasyChair, 2020a. doi: 10.29007/wg1q. URL https://doi.org/10.29007/wg1q. — [doi:10.29007/wg1q](https://doi.org/10.29007/wg1q) ↗
  11. Lasse Blaauwbroek, Josef Urban, and Herman Geuvers. The tactician - A seamless, interactive tactic learner and prover for coq. In Christoph Benzmüller and Bruce R. Miller (eds.), Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceed… find
  12. Springer, 2020b. doi: 10.1007/978-3-030-53518-6\\ 17. URL https://doi.org/10.1007/978-3-030-53518-6_17. — [doi:10.1007/978-3-030-53518-6\](https://doi.org/10.1007/978-3-030-53518-6\) ↗
  13. Lasse Blaauwbroek, Miroslav Olšák, and Herman Geuvers. Hashing modulo context-sensitive α-equivalence. arXiv preprint, January 2024. doi: 10.48550/arXiv.2401.02948. URL https://doi.org/10.48550/arXiv.2401.02948. — [doi:10.48550/arxiv.2401.02948](https://doi.org/10.48550/arxiv.2401.02948) ↗
  14. Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban. A learning-based fact selector for isabelle/hol. J. Autom. Reason., 57(3):219–244, 2016a. doi: 10.1007/s10817-016-9362-8. 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) ↗
  15. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. J. Formaliz. Reason., 9(1):101–148, 2016b. doi: 10.6092/issn.1972-5787/4593. URL https://doi.org/10.6092/issn.1972-5787/4593. ↗
  16. Karel Chvalovský, Jan Jakubuv, Martin Suda, and Josef Urban. ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. In Pascal Fontaine (ed.), Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, vol…
  17. Springer, 2019. doi: 10.1007/978-3-030-29436-6\\ 12. URL https://doi.org/10.1007/978-3-030-29436-6_12. — [doi:10.1007/978-3-030-29436-6\](https://doi.org/10.1007/978-3-030-29436-6\) ↗
  18. Lukasz Czajka. Practical proof search for coq by type inhabitation. In Nicolas Peltier and Viorica Sofronie-Stokkermans (eds.), Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Scienc… find
  19. Springer, 2020. doi: 10.1007/978-3-030-51054-1\\ 3. URL https://doi.org/10.1007/978-3-030-51054-1_3. — [doi:10.1007/978-3-030-51054-1\](https://doi.org/10.1007/978-3-030-51054-1\) ↗
  20. Lukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory. J. Autom. Reason., 61(1-4):423–453, 2018. doi: 10.1007/s10817-018-9458-4. URL https://doi.org/10.1007/s10817-018-9458-4. ↗
  21. Oleksandr Ferludin, Arno Eigenwillig, Martin Blais, Dustin Zelle, Jan Pfeifer, Alvaro Sanchez-Gonzalez, Sibon Li, Sami Abu-El-Haija, Peter Battaglia, Neslihan Bulut, Jonathan Halcrow, Filipe Miguel Gonçalves de Almeida, Silvio Lattanzi, André Linhares, Brandon Mayer, Vahab Mirrokni, John Palowitch… — [arXiv:2207.03522](https://arxiv.org/abs/2207.03522) find
  22. Emily First and Yuriy Brun. Diversity-driven automated formal verification. In Proceedings of the 44th International Conference on Software Engineering, ICSE ’22, pp. 749–761, New York, NY, USA, 2022. Association for Computing Machinery. ISBN 9781450392211. doi: 10.1145/3510003.3510138. URL https://… — [doi:10.1145/3510003.3510138](https://doi.org/10.1145/3510003.3510138) find
  23. Emily First, Yuriy Brun, and Arjun Guha. Tactok: Semantics-aware proof synthesis. Proc. ACM Program. Lang., 4(OOPSLA), nov 2020. doi: 10.1145/3428299. URL https://doi.org/10.1145/3428299. — [doi:10.1145/3428299](https://doi.org/10.1145/3428299) ↗
  24. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Tactictoe: Learning to reason with hol4 tactics. In Thomas Eiter and David Sands (eds.), LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 46 of EPiC Series in Computing, pp. 125–143. Ea… find
  25. Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, and Josef Urban. The isabelle ENIGMA. In June Andronick and Leonardo de Moura (eds.), 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, volume 237 o… — [doi:10.4230/lipics.itp.2022.16](https://doi.org/10.4230/lipics.itp.2022.16) find
  26. Georges Gonthier. The four colour theorem: Engineering of a formal proof. In Deepak Kapur (ed.), Computer Mathematics, pp. 333–333, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. ISBN 978-3-540-87827-8. find
  27. Thomas Gransden, Neil Walkinshaw, and Rajeev Raman. Sepia: Search for proofs using inferred automata. In Amy P. Felty and Aart Middeldorp (eds.), Automated Deduction - CADE-25, pp. 246–255, Cham, 2015. Springer International Publishing. ISBN 978-3-319-21401-6. find
  28. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. In International Conference on Learning Representations, 2021.
  29. Y. F. Hu. Efficient and high quality force-directed graph drawing. The Mathematica Journal, 10:37–71, 2005. URL http://www.mathematica-journal.com/issue/v10i1/contents/graph_draw/ graph_draw.pdf. ↗
  30. 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.
  31. OpenReview.net, 2019. URL https://openreview.net/forum?id=r1xwKoR9Y7. ↗
  32. Jan Jakubuv and Josef Urban. ENIGMA: efficient learning-based inference guiding machine. In Herman Geuvers, Matthew England, Osman Hasan, Florian Rabe, and Olaf Teschke (eds.), Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings,…
  33. Springer, 2017. doi: 10.1007/978-3-319-62075-6\\ 20. URL https://doi.org/10.1007/978-3-319-62075-6_20. — [doi:10.1007/978-3-319-62075-6\](https://doi.org/10.1007/978-3-319-62075-6\) ↗
  34. Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, and Josef Urban. ENIGMA anonymous: Symbol-independent inference guiding machine (system description). In Nicolas Peltier and Viorica Sofronie-Stokkermans (eds.), Automated Reasoning - 10th International Joint Conferenc…
  35. Springer, 2020. doi: 10.1007/978-3-030-51054-1\\ 29. URL https://doi.org/10.1007/978-3-030-51054-1_29. — [doi:10.1007/978-3-030-51054-1\](https://doi.org/10.1007/978-3-030-51054-1\) ↗
  36. Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygózdz, Piotr Milos, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. In NeurIPS, 2022.
  37. Cezary Kaliszyk and Josef Urban. Mizar 40 for mizar 40. Journal of Automated Reasoning, 55(3):245–256, 2015.
  38. Cezary Kaliszyk, Lionel Mamane, and Josef Urban. Machine learning of coq proof guidance: First experiments. In Temur Kutsia and Andrei Voronkov (eds.), 6th International Symposium on Symbolic Computation in Software Science, SCSS 2014, Gammarth, La Marsa, Tunisia, December 7-8, 2014, volume 30 of EP… find
  39. EasyChair, 2014. doi: 10.29007/lmmg. URL https://doi.org/10.29007/lmmg. — [doi:10.29007/lmmg](https://doi.org/10.29007/lmmg) ↗
  40. Ekaterina Komendantskaya, Jonathan Heras, and Gud-mund Grov. Machine learning in proof general. In Proceedings 10th International Workshop On User Interfaces for Theorem Provers (UITP 2012), Electronic Proceedings in Theoretical Computer Science, pp. 15– 41, Australia, 2013. Open Publishing Associat… — [doi:10.4204/eptcs.118.2](https://doi.org/10.4204/eptcs.118.2) find
  41. Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. Mash: Machine learning for sledgehammer. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (eds.), Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. P… find
  42. Springer, 2013. doi: 10.1007/978-3-642-39634-2\\ 6. URL https://doi.org/10.1007/978-3-642-39634-2_6. — [doi:10.1007/978-3-642-39634-2\](https://doi.org/10.1007/978-3-642-39634-2\) ↗
  43. Guillaume Lample, Timothée Lacroix, Marie-Anne Lachaux, Aurélien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. In NeurIPS, 2022.
  44. Maciej Mikuła, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. Magnushammer: A transformer-based approach to premise selection. arXiv preprint arXiv:2303.04488, 2023.
  45. Aditya Paliwal, Sarah M. Loos, Markus N. 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, The Thirty-Second Innovative Applications of Artificial Intelligence Con…
  46. AAAI Press, 2020. doi: 10.1609/AAAI.V34I03.5689. URL https://doi.org/10.1609/aaai.v34i03.5689. — [doi:10.1609/aaai.v34i03.5689](https://doi.org/10.1609/aaai.v34i03.5689) ↗
  47. Bartosz Piotrowski, Ramon Fernández Mir, and Edward Ayers. Machine-learned premise selection for lean. In Revantha Ramanayake and Josef Urban (eds.), Automated Reasoning with Analytic Tableaux and Related Methods, pp. 175–186, Cham, 2023. Springer Nature Switzerland. ISBN 978-3-031-43513-3. find
  48. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  49. Alec Radford, Jeff Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language models are unsupervised multitask learners. 2019. find
  50. Jason Rute, Miroslav Olšák, Lasse Blaauwbroek, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun. Artifact for: Graph2Tac: Learning Hierarchical Representations of Math Concepts in Theorem Proving, December 2023. URL https://doi.org/10.5281/zenodo.10410473. — [doi:10.5281/zenodo.10410473](https://doi.org/10.5281/zenodo.10410473) ↗
  51. Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. Generating correctness proofs with neural networks. In Proceedings of the 4th ACM SIG-PLAN International Workshop on Machine Learning and Programming Languages, MAPL 2020, pp. 1–10, New York, NY, USA, 2020. Association for Computin…
  52. Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer. Passport: Improving automated formal verification using identifiers. ACM Trans. Program. Lang. Syst., 45(2), jun 2023. ISSN 0164-0925. doi: 10.1145/3593374. URL https://doi.org/10.1145/3593374. ↗
  53. The Coq Development Team. The Coq Proof Assistant, July 2023. URL https://doi.org/10.5281/zenodo.8161141. — [doi:10.5281/zenodo.8161141](https://doi.org/10.5281/zenodo.8161141) ↗
  54. Josef Urban. Translating mizar for first order theorem provers. In Andrea Asperti, Bruno Buchberger, and James H. Davenport (eds.), Mathematical Knowledge Management, Second International Conference, MKM 2003, Bertinoro, Italy, February 16-18, 2003, Proceedings, volume 2594 of Lecture Notes in Compu… find
  55. Springer, 2003. doi: 10.1007/3-540-36469-2\\ 16. URL https://doi.org/10.1007/3-540-36469-2_16. — [doi:10.1007/3-540-36469-2\](https://doi.org/10.1007/3-540-36469-2\) ↗
  56. Thomas Wolf, Lysandre Debut, Victor Sanh, Julien Chaumond, Clement Delangue, Anthony Moi, Pierric Cistac, Tim Rault, Rémi Louf, Morgan Funtowicz, Joe Davison, Sam Shleifer, Patrick von Platen, Clara Ma, Yacine Jernite, Julien Plu, Canwen Xu, Teven Le Scao, Sylvain Gugger, Mariama Drame, Quentin Lho… — Transformers: State-of-the-Art Natural Language Processing
  57. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning (ICML), 2019.
  58. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. arXiv preprint arXiv:2306.15626, 2023.
  59. Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Černỳ, Cezary Kaliszyk, and Josef Urban. Online machine learning techniques for coq: A comparison. In Fairouz Kamareddine and Claudio Sacerdoti Coen (eds.), Intelligent Computer Mathematics, pp. 67–83, Cham, 2021. Springer International Pub… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/blaauwbroek-2024-graph2tac-online-representation-learning-formal/