Elamur Research⌕
☰
home / papers / 2017 / Premise Selection for Theorem Proving by Deep Graph Embedding

Premise Selection for Theorem Proving by Deep Graph Embedding

Paper · 2017 · Mingzhe Wang, Yihe Tang, Jian Wang et al.

Summary

Automated theorem provers struggle with large mathematical libraries. Premise selection is a filtering step that picks the few known statements likely to help prove a target conjecture. Earlier learning-based systems for this task processed formulas as strings of characters or tokens. This work instead turns each higher-order logic formula into a graph. The parse tree is extended with links from each quantifier to the variables it binds, repeated constants and variables are collapsed into shared nodes, and variable names are replaced by the placeholders VAR or VARFUNC. The graph keeps the formula's full structure and is unaffected by how variables happen to be named. A neural model, FormulaNet, starts each node with an embedding, refines it repeatedly using its neighbours (also taking edge order into account), and pools all node embeddings into one vector that a classifier uses to judge relevance. On HolStep, accuracy rises from 83% to 90.3%. This suggests that explicit structural encodings of formulas outperform sequence models for this task.

Key points

  • Data: experiments use HolStep, which contains roughly 2M statements and 10K conjectures arranged as conjecture–statement pairs. The new model improves the best prior accuracy by 7.3 points, from 83% to 90.3%.
  • Novelty: the authors call this the first deep graph embedding approach to premise selection. They also present the embedding scheme as the first deep model for general graphs that preserves edge ordering. Two versions are evaluated: FormulaNet-basic and FormulaNet.
  • Renaming ablation: variable names were randomly permuted in a validation set. On this set, models using the original names drop sharply: Tree-old-names falls from 89.7 to 82.3 and Graph-old-names from 89.8 to 83.5. The proposed graph stays at 89.9. Renamed trees without quantifier links are stable but weak, at 84.7.
  • Update steps: with zero steps, which amounts to a bag of tokens, accuracy is already 81.5%. FormulaNet reaches 91.1% validation accuracy on conditional premise selection after 3 steps, and further steps give diminishing returns.
  • Qualitative check: nearest neighbours in the learned node-embedding space show similar local topology and naming. This indicates that the embeddings capture the formulas' structure.

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 MichiganAnn Arbor · United States94 works · 18,548 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 Mingzhe Wang, Yihe Tang, Jian Wang and Jia Deng. 2017. Premise Selection for Theorem Proving by Deep Graph Embedding. arXiv:1709.09994.

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

@misc{wang2017premise,
  title = {{Premise Selection for Theorem Proving by Deep Graph Embedding}},
  author = {Mingzhe Wang, Yihe Tang, Jian Wang and Jia Deng},
  year = {2017},
  doi = {10.48550/arxiv.1709.09994},
  eprint = {1709.09994},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1709.09994}
}

References

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

  1. Alan JA Robinson and Andrei Voronkov. Handbook of automated reasoning, volume 1. Elsevier, 2001. find
  2. Christoph Kern and Mark R Greenstreet. Formal verification in hardware design: a survey. ACM Transactions on Design Automation of Electronic Systems (TODAES), 4(2):123–193, 1999. find
  3. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pages 207–… find
  4. Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009. find
  5. Alexander A Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, and Josef Urban. Deepmath - deep sequence models for premise selection. In D. D. Lee, M. Sugiyama, U. V. Luxburg, I. Guyon, and R. Garnett, editors, Advances in Neural Information Processing Systems 29, pages 2235–2…
  6. Adam Naumowicz and Artur Korniłowicz. A Brief Overview of Mizar, pages 67–72. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009. find
  7. John Harrison. HOL Light: An Overview, pages 60–66. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009. find
  8. Kryštof Hoder and Andrei Voronkov. Sine qua non for large theory reasoning. In International Conference on Automated Deduction, pages 299–314. Springer, 2011. find
  9. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. Journal of Automated Reasoning, 52(2):191–213, 2014.
  10. Cezary Kaliszyk, François Chollet, and Christian Szegedy. Holstep: A machine learning dataset for higher-order logic theorem proving. arXiv preprint arXiv:1703.00426, 2017.
  11. John Harrison, Josef Urban, and Freek Wiedijk. History of interactive theorem proving. In Computational Logic, volume 9, pages 135–214, 2014.
  12. Gilles Dowek, Amy Felty, Hugo Herbelin, Gérard Huet, Chetan Murthy, Catherin Parent, Christine Paulin-Mohring, and Benjamin Werner. The COQ Proof Assistant: User’s Guide: Version 5.6. INRIA, 1992. find
  13. Makarius Wenzel, Lawrence C Paulson, and Tobias Nipkow. The isabelle framework. In International Conference on Theorem Proving in Higher Order Logics, pages 33–38. Springer, 2008.
  14. Stephan Schulz. E–a brainiac theorem prover. Ai Communications, 15(2, 3):111–126, 2002. find
  15. Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, et al. A formal proof of the kepler conjecture. arXiv preprint arXiv:1501.02155, 2015.
  16. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A Machine-Checked Proof of the Odd Order Theorem, pages 16… find
  17. Christian Suttner and Wolfgang Ertel. Automatic acquisition of search guiding heuristics. In International Conference on Automated Deduction, pages 470–484. Springer, 1990. find
  18. Jörg Denzinger, Matthias Fuchs, Christoph Goller, and Stephan Schulz. Learning from previous proof experience: A survey. Citeseer, 1999. find
  19. SA Schulz. Learning search control knowledge for equational deduction, volume 230. IOS Press, 2000. find
  20. Michael Färber and Chad Brown. Internal guidance for satallax. In International Joint Conference on Automated Reasoning, pages 349–361. Springer, 2016. find
  21. Cezary Kaliszyk and Josef Urban. Femalecop: fairly efficient machine learning connection prover. In Logic for Programming, Artificial Intelligence, and Reasoning, pages 88–96. Springer, 2015. find
  22. Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644, 2016.
  23. Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. arXiv preprint arXiv:1701.06972, 2017.
  24. Richard Socher, Eric H. Huang, Jeffrey Pennin, Christopher D Manning, and Andrew Y. Ng. Dynamic pooling and unfolding recursive autoencoders for paraphrase detection. In J. Shawe-Taylor, R. S. Zemel, P. L. Bartlett, F. Pereira, and K. Q. Weinberger, editors, Advances in Neural Information Processing… find
  25. Richard Socher, Cliff C Lin, Chris Manning, and Andrew Y Ng. Parsing natural scenes and natural language with recursive neural networks. In Proceedings of the 28th international conference on machine learning (ICML-11), pages 129–136, 2011. find
  26. Daniel Kühlwein and Josef Urban. Males: A framework for automatic tuning of automated theorem provers. Journal of Automated Reasoning, 55(2):91–116, 2015. find
  27. James P. Bridge, Sean B. Holden, and Lawrence C. Paulson. Machine learning for first-order theorem proving. Journal of Automated Reasoning, 53(2):141–172, 2014. find
  28. Bryan Perozzi, Rami Al-Rfou, and Steven Skiena. Deepwalk: Online learning of social representations. In Proceedings of the 20th ACM SIGKDD international conference on Knowledge discovery and data mining, pages 701–710. ACM, 2014. find
  29. Jian Tang, Meng Qu, Mingzhe Wang, Ming Zhang, Jun Yan, and Qiaozhu Mei. Line: Large-scale information network embedding. In Proceedings of the 24th International Conference on World Wide Web, pages 1067–1077. ACM, 2015. find
  30. Aditya Grover and Jure Leskovec. node2vec: Scalable feature learning for networks. In Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, pages 855–864. ACM, 2016. find
  31. Tomas Mikolov, Ilya Sutskever, Kai Chen, Greg S Corrado, and Jeff Dean. Distributed representations of words and phrases and their compositionality. In Advances in neural information processing systems, pages 3111–3119, 2013.
  32. Tomas Mikolov, Kai Chen, Greg Corrado, and Jeffrey Dean. Efficient estimation of word representations in vector space. arXiv preprint arXiv:1301.3781, 2013.
  33. Christoph Goller and Andreas Kuchler. Learning task-dependent distributed representations by backpropagation through structure. In Neural Networks, 1996., IEEE International Conference on, volume 1, pages 347–352. IEEE, 1996. find
  34. Kai Sheng Tai, Richard Socher, and Christopher D Manning. Improved semantic representations from tree-structured long short-term memory networks. arXiv preprint arXiv:1503.00075, 2015. find
  35. Marco Gori, Gabriele Monfardini, and Franco Scarselli. A new model for learning in graph domains. In Neural Networks, 2005. IJCNN’05. Proceedings. 2005 IEEE International Joint Conference on, volume 2, pages 729–734. IEEE, 2005. find
  36. Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini. The graph neural network model. IEEE Transactions on Neural Networks, 20(1):61–80, 2009. find
  37. David K Duvenaud, Dougal Maclaurin, Jorge Iparraguirre, Rafael Bombarell, Timothy Hirzel, Alán Aspuru-Guzik, and Ryan P Adams. Convolutional networks on graphs for learning molecular fingerprints. In Advances in neural information processing systems, pages 2224–2232, 2015.
  38. Yujia Li, Daniel Tarlow, Marc Brockschmidt, and Richard Zemel. Gated graph sequence neural networks. arXiv preprint arXiv:1511.05493, 2015. find
  39. Ashesh Jain, Amir R Zamir, Silvio Savarese, and Ashutosh Saxena. Structural-rnn: Deep learning on spatiotemporal graphs. In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pages 5308–5317, 2016. find
  40. Mikael Henaff, Joan Bruna, and Yann LeCun. Deep convolutional networks on graph-structured data. arXiv preprint arXiv:1506.05163, 2015. — [arXiv:1506.05163](https://arxiv.org/abs/1506.05163) find
  41. Michaël Defferrard, Xavier Bresson, and Pierre Vandergheynst. Convolutional neural networks on graphs with fast localized spectral filtering. In Advances in Neural Information Processing Systems, pages 3837–3845, 2016.
  42. Thomas N Kipf and Max Welling. Semi-supervised classification with graph convolutional networks. arXiv preprint arXiv:1609.02907, 2016.
  43. Mathias Niepert, Mohamed Ahmed, and Konstantin Kutzkov. Learning convolutional neural networks for graphs. In Proceedings of the 33rd annual international conference on machine learning. ACM, 2016. find
  44. Alonzo Church. A formulation of the simple theory of types. The journal of symbolic logic, 5(02):56–68, 1940. find
  45. John Harrison. The hol light theory of euclidean space. Journal of Automated Reasoning, pages 1–18, 2013. find
  46. Sergey Ioffe and Christian Szegedy. Batch normalization: Accelerating deep network training by reducing internal covariate shift. arXiv preprint arXiv:1502.03167, 2015. find
  47. Geoffrey Hinton, Nitish Srivastava, and Kevin Swersky. Lecture 6a overview of mini–batch gradient descent. Coursera Lecture slides https://class.coursera. org/neuralnets-2012-001/lecture,[Online, 2012. ↗
  48. Laurens van der Maaten and Geoffrey Hinton. Visualizing data using t-sne. Journal of Machine Learning Research, 9(Nov):2579–2605, 2008. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wang-2017-premise-selection-theorem-proving-deep/