Graph Representations for Higher-Order Logic and Theorem Proving

Authors

  • Aditya Paliwal Google Research
  • Sarah Loos Google Research
  • Markus Rabe Google Research
  • Kshitij Bansal Google Research
  • Christian Szegedy Google Research

DOI:

https://doi.org/10.1609/aaai.v34i03.5689

Abstract

This paper presents the first use of graph neural networks (GNNs) for higher-order proof search and demonstrates that GNNs can improve upon state-of-the-art results in this domain. Interactive, higher-order theorem provers allow for the formalization of most mathematical theories and have been shown to pose a significant challenge for deep learning. Higher-order logic is highly expressive and, even though it is well-structured with a clearly defined grammar and semantics, there still remains no well-established method to convert formulas into graph-based representations. In this paper, we consider several graphical representations of higher-order logic and evaluate them against the HOList benchmark for higher-order theorem proving.

Downloads

Published

2020-04-03

How to Cite

Paliwal, A., Loos, S., Rabe, M., Bansal, K., & Szegedy, C. (2020). Graph Representations for Higher-Order Logic and Theorem Proving. Proceedings of the AAAI Conference on Artificial Intelligence, 34(03), 2967-2974. https://doi.org/10.1609/aaai.v34i03.5689

Issue

Section

AAAI Technical Track: Knowledge Representation and Reasoning