# Graph Representations for Higher-Order Logic and Theorem Proving

Source: [Graph Representations for Higher-Order Logic and Theorem Proving](<https://www.sota2.com/research/paper/68fa66571e209131cea0fa3a>)

Collection index: [llms.txt](<https://www.sota2.com/research/llms.txt>)

Data updated: 2026-01-04T03:08:42.382Z

Authors: Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, Christian Szegedy

Published: 2019-05-24T02:42:22.000Z

## 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.

## Recorded benchmark results

A research result applies to its stated dataset, split, metric and evaluation configuration. Compare like-for-like settings, preserve the metric's unit and direction, and distinguish paper-reported results from independent reproduction. The best result recorded here is not a claim of exhaustive, current global coverage.

- [Automated Theorem Proving on HOList complex analysis corpus (val)](<https://www.sota2.com/research/sota/automated-theorem-proving-on-holist-complex-analysis-corpus-val.md>): Automated Theorem Proving; HOList complex analysis corpus (val); Proofs Closed Rate: 49.95.

## Original sources and implementation

[Original paper](<https://arxiv.org/abs/1905.10006>)

[PDF](<https://arxiv.org/pdf/1905.10006.pdf>)