Graph Representations for Higher-Order Logic and Theorem Proving
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.
Cite
Text
Paliwal et al. "Graph Representations for Higher-Order Logic and Theorem Proving." AAAI Conference on Artificial Intelligence, 2020. doi:10.1609/AAAI.V34I03.5689Markdown
[Paliwal et al. "Graph Representations for Higher-Order Logic and Theorem Proving." AAAI Conference on Artificial Intelligence, 2020.](https://mlanthology.org/aaai/2020/paliwal2020aaai-graph/) doi:10.1609/AAAI.V34I03.5689BibTeX
@inproceedings{paliwal2020aaai-graph,
title = {{Graph Representations for Higher-Order Logic and Theorem Proving}},
author = {Paliwal, Aditya and Loos, Sarah M. and Rabe, Markus N. and Bansal, Kshitij and Szegedy, Christian},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2020},
pages = {2967-2974},
doi = {10.1609/AAAI.V34I03.5689},
url = {https://mlanthology.org/aaai/2020/paliwal2020aaai-graph/}
}