# Graph Representations for Higher-Order Logic and Theorem Proving

## TL;DR

This paper explores the use of graph neural networks for higher-order theorem proving, demonstrating their potential to improve proof search efficiency by converting complex logical formulas into graph-based representations.

## Contribution

It introduces novel graph representations for higher-order logic and evaluates their effectiveness on the HOList benchmark, advancing the application of GNNs in formal theorem proving.

## Key findings

- GNNs can outperform existing methods in higher-order proof search
- Different graph representations are evaluated for effectiveness
- GNN-based approaches show promise for automating complex 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.