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.
Description
[1905.10006] Graph Representations for Higher-Order Logic and Theorem Proving
%0 Journal Article
%1 paliwal2019graph
%A Paliwal, Aditya
%A Loos, Sarah
%A Rabe, Markus
%A Bansal, Kshitij
%A Szegedy, Christian
%D 2019
%K deep-learning mathematics proof-systems theory
%T Graph Representations for Higher-Order Logic and Theorem Proving
%U http://arxiv.org/abs/1905.10006
%X 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.
@article{paliwal2019graph,
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.},
added-at = {2019-05-30T12:54:49.000+0200},
author = {Paliwal, Aditya and Loos, Sarah and Rabe, Markus and Bansal, Kshitij and Szegedy, Christian},
biburl = {https://www.bibsonomy.org/bibtex/29ea3012de34b74ed5d6902be67796ca1/kirk86},
description = {[1905.10006] Graph Representations for Higher-Order Logic and Theorem Proving},
interhash = {22f408b796076772edaa6c2fdfb85665},
intrahash = {9ea3012de34b74ed5d6902be67796ca1},
keywords = {deep-learning mathematics proof-systems theory},
note = {cite arxiv:1905.10006},
timestamp = {2019-05-30T12:54:49.000+0200},
title = {Graph Representations for Higher-Order Logic and Theorem Proving},
url = {http://arxiv.org/abs/1905.10006},
year = 2019
}