Elamur Research⌕
☰
home / papers / 2019 / Graph Representations for Higher-Order Logic and Theorem Proving

Graph Representations for Higher-Order Logic and Theorem Proving

Paper · 2019 · Aditya Paliwal, Sarah Loos, Markus Rabe et al.

Summary

Neural guidance of proof search in higher-order logic is difficult, partly because there is no standard way to turn formulas into graphs that a neural network can process. The authors use HOL Light terms from the HOList benchmark, which contains more than twenty thousand theorems with human-written proofs. They treat each S-expression syntax tree as a graph with both child and parent edges, then compare several variants: subexpression sharing, leaf sharing, variable blinding, added random edges, and one-directional (top-down or bottom-up) message flow. A message-passing GNN embeds goals and candidate premises. Trained by imitating human proofs, the model selects a tactic and ranks the theorems passed to it as arguments. Every model is evaluated end to end by counting how many validation theorems the DeepHOL prover closes when guided by it. The best setup, which uses subexpression sharing, proves nearly half of the validation set and clearly surpasses earlier HOList results. The study shows that small representation choices strongly affect performance and that context from parent nodes matters. This supports GNNs over TreeRNNs for encoding logic.

Key points

  • This is presented as the first use of GNNs for higher-order proof search. It is evaluated on HOList / DeepHOL, which is built on HOL Light, and the best model proves close to 50% of validation theorems.
  • A simple bag-of-words model already outperforms the original HOList reference models.
  • Merging identical subexpressions shrinks the example graph for ∀x : x = x from 27 to 15 nodes. Shared representations clearly outperform plain trees, which contrasts with Wang et al. (2017).
  • Passing messages only top-down, which emphasizes context, works better than bottom-up only. Moving from 0 to 12 message-passing hops raises successful tactic applications from 33.8% to 38.6%.
  • Training details:
    • batches of 4,096 examples with sampled negative premises;
    • a combined loss of cross-entropy and AUCROC;
    • Adam with a learning rate of 0.0001;
    • eight Tesla V100 GPUs.
  • Stated limitation: local assumptions of the goal are ignored.

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

🏢GoogleMountain View · United States533 works · 443,885 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 Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal and Christian Szegedy. 2019. Graph Representations for Higher-Order Logic and Theorem Proving. arXiv:1905.10006.

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

@misc{paliwal2019graph,
  title = {{Graph Representations for Higher-Order Logic and Theorem Proving}},
  author = {Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal and Christian Szegedy},
  year = {2019},
  doi = {10.48550/arxiv.1905.10006},
  eprint = {1905.10006},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1905.10006}
}

References

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

  1. Bansal, K.; Loos, S. M.; Rabe, M. N.; Szegedy, C.; and Wilcox, S. 2019. Holist: An environment for machine learning of higher-order theorem proving. ICML 2019. International Conference on Machine Learning.
  2. Battaglia, P. W.; Hamrick, J. B.; Bapst, V.; Sanchez-Gonzalez, A.; Zambaldi, V. F.; Malinowski, M.; Tacchetti, A.; Raposo, D.; Santoro, A.; Faulkner, R.; Gülçehre, Ç.; Song, F.; Ballard, A. J.; Gilmer, J.; Dahl, G. E.; Vaswani, A.; Allen, K.; Nash, C.; Langston, V.; Dyer, C.; Heess, N.; Wierstra,… — Relational inductive biases, deep learning, and graph networks
  3. Bentkamp, A.; Blanchette, J. C.; Cruanes, S.; and Waldmann, U. 2018. Superposition for lambda-free higher-order logic. In Galmiche, D.; Schulz, S.; and Sebastiani, R., eds., Automated Reasoning, 28–46. Cham: Springer International Publishing. find
  4. Burges, C.; Shaked, T.; Renshaw, E.; Lazier, A.; Deeds, M.; Hamilton, N.; and Hullender, G. N. 2005. Learning to rank using gradient descent. In Proceedings of the 22nd International Conference on Machine learning (ICML-05), 89–96.
  5. Dong, H.; Mao, J.; Lin, T.; Wang, C.; Li, L.; and Zhou, D. 2019. Neural logic machines. ICLR 2019. International Conference on Learning Representations. find
  6. Eban, E. E.; Schain, M.; Mackey, A.; Gordon, A.; Saurous, R. A.; and Elidan, G. 2017. Scalable learning of non-decomposable objectives. Proceedings of the 20th International Conference on Artificial Intelligence and Statistics (AISTATS). find
  7. Evans, R.; Saxton, D.; Amos, D.; Kohli, P.; and Grefenstette, E. 2018. Can neural networks understand logical entailment? ICLR 2018. International Conference on Learning Representations.
  8. Gauthier, T.; Kaliszyk, C.; and Urban, J. 2017. Tactictoe: Learning to reason with hol4 tactics. In LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 46, 125–143. find
  9. Gilmer, J.; Schoenholz, S. S.; Riley, P. F.; Vinyals, O.; and Dahl, G. E. 2017. Neural message passing for quantum chemistry. CoRR abs/1704.01212.
  10. Gonthier, G.; Asperti, A.; Avigad, J.; Bertot, Y.; Cohen, C.; Garillot, F.; Roux, S. L.; Mahboubi, A.; O’Connor, R.; Biha, S. O.; Pasca, I.; Rideau, L.; Solovyev, A.; Tassi, E.; and Théry, L. 2013. A machine-checked proof of the Odd Order Theorem. In ITP, 163–179. find
  11. Gonthier, G. 2008. Formal proof–the four-color theorem. Notices of the AMS 55(11):1382–1393. find
  12. 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. 2017. A formal proof of the kepler conjecture. In Forum of Mathematics, Pi, volume 5. Cambridge University Press.
  13. Harrison, J. 1996. HOL Light: A tutorial introduction. In FMCAD, 265–269. find
  14. Huang, D.; Dhariwal, P.; Song, D.; and Sutskever, I. 2018. Gamepad: A learning environment for theorem proving. ICLR 2018. International Conference on Learning Representations.
  15. Kaliszyk, C., and Urban, J. 2014. Learning-assisted automated reasoning with flyspeck. Journal of Automated Reasoning 53(2):173–213.
  16. Kingma, D. P., and Ba, J. 2014. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980.
  17. Lederman, G.; Rabe, M. N.; and Seshia, S. A. 2018. Learning heuristics for automated reasoning through deep reinforcement learning. CoRR abs/1807.08058.
  18. Li, Y.; Tarlow, D.; Brockschmidt, M.; and Zemel, R. 2015. Gated graph sequence neural networks. arXiv preprint arXiv:1511.05493. find
  19. Li, Y.; Yu, R.; Shahabi, C.; and Liu, Y. 2017. Graph convolutional recurrent neural network: Data-driven traffic forecasting. CoRR abs/1707.01926. — [arXiv:1707.01926](https://arxiv.org/abs/1707.01926) find
  20. Loos, S.; Irving, G.; Szegedy, C.; and Kaliszyk, C. 2017. Deep network guided proof search. LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning.
  21. Polyak, B. T., and Juditsky, A. B. 1992. Acceleration of stochastic approximation by averaging. SIAM Journal on Control and Optimization 30(4):838– 855. find
  22. Polyak, B. T. 1990. A new method of stochastic approximation type. Avtomatika i telemekhanika 7:98– 107. find
  23. Raposo, D.; Santoro, A.; Barrett, D. G. T.; Pascanu, R.; Lillicrap, T. P.; and Battaglia, P. W. 2017. Discovering objects and their relations from entangled scene representations. CoRR abs/1702.05068. — [arXiv:1702.05068](https://arxiv.org/abs/1702.05068) find
  24. Sanchez-Stern, A.; Alhessi, Y.; Saul, L. K.; and Lerner, S. 2019. Generating correctness proofs with neural networks. CoRR abs/1907.07794.
  25. Santoro, A.; Raposo, D.; Barrett, D. G. T.; Malinowski, M.; Pascanu, R.; Battaglia, P.; and Lillicrap, T. P. 2017. A simple neural network module for relational reasoning. CoRR abs/1706.01427.
  26. Scarselli, F.; Gori, M.; Tsoi, A. C.; Hagenbuchner, M.; and Monfardini, G. 2009. The graph neural network model. IEEE Transactions on Neural Networks 20(1):61–80. find
  27. Selsam, D., and Bjørner, N. 2019. Guiding high-performance sat solvers with unsat-core predictions. SAT 2019, The 22nd International Conference on Theory and Applications of Satisfiability Testing.
  28. Wang, M.; Tang, Y.; Wang, J.; and Deng, J. 2017. Premise selection for theorem proving by deep graph embedding. In Advances in Neural Information Processing Systems, 2786–2796.
  29. Wu, Z.; Pan, S.; Chen, F.; Long, G.; Zhang, C.; and Yu, P. S. 2019. A comprehensive survey on graph neural networks. CoRR abs/1901.00596.
  30. Xu, K.; Hu, W.; Leskovec, J.; and Jegelka, S. 2019. How powerful are graph neural networks? ICLR 2019. International Conference on Learning Representations.
  31. Yang, K., and Deng, J. 2019. Learning to prove theorems via interacting with proof assistants. CoRR abs/1905.09381.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/paliwal-2019-graph-representations-higher-order-logic/