TY - JOUR AU - Paliwal, Aditya AU - Loos, Sarah AU - Rabe, Markus AU - Bansal, Kshitij AU - Szegedy, Christian PY - 2020/04/03 Y2 - 2024/03/29 TI - Graph Representations for Higher-Order Logic and Theorem Proving JF - Proceedings of the AAAI Conference on Artificial Intelligence JA - AAAI VL - 34 IS - 03 SE - AAAI Technical Track: Knowledge Representation and Reasoning DO - 10.1609/aaai.v34i03.5689 UR - https://ojs.aaai.org/index.php/AAAI/article/view/5689 SP - 2967-2974 AB - <p>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.</p> ER -