Graph Representations for Higher-Order Logic and Theorem Proving

Higher-order theorem proving is central to formalized mathematics because it allows quantification over propositions and functions, which makes it expressive enough for real mathematical theories. Systems such as HOL Light, Coq, and HOL4 have supported major formalization efforts in topology, analysis, geometry, and the Kepler conjecture. HOList was introduced as a learning environment for this domain: it offers a stateless theorem-proving API, a benchmark with over twenty thousand theorems, and human proofs generated inside HOL Light. Before this paper, deep learning had shown promise in premise selection and tactic prediction, but TreeRNNs, LSTMs, and other sequence/tree encoders had not delivered decisive gains on end-to-end proof search.

The core problem is how to represent higher-order logic formulas so that a neural model can capture both local syntax and global proof-relevant context. A pure tree representation repeats identical subexpressions and isolates sibling branches; a sequence representation loses structure altogether. For theorem proving, this is especially harmful because the same subexpression may play different roles in different locations, and successful proof steps depend on the surrounding goal, available premises, and tactic semantics. The challenge is therefore not only classification, but representation for search.

The paper's innovations are structural and end-to-end. First, it introduces several graph encodings of HOL, especially subexpression sharing, which merges syntactically identical subterms and lets multiple occurrences contribute to the same node state. Second, it uses a bidirectional message-passing GNN so each node can combine parent context and child content instead of encoding only bottom-up like a TreeRNN. Third, it evaluates representations inside an actual theorem prover loop, not just on proxy accuracy. Fourth, it explicitly studies edge direction, random edges, leaf sharing, and variable blinding, showing that graph design choices materially affect proof success.

• �� Input representation: HOList S-expressions are converted into directed graphs. Node labels include application (a), variable (v), lambda (l), constant (c), and type constructors such as fun; edge labels preserve child order.
• �� Representation variants: ordinary AST; leaf sharing; subexpression sharing; variable blinding; random edges; top-down only; bottom-up only. Subexpression sharing merges identical expressions so repeated occurrences of x or a typed subterm point to one shared node.
• �� Node initialization: each token gets a trainable embedding; ML Pv and MLP_E embed node and edge labels into a latent space.
• �� Message passing: for T rounds, each edge produces two directional messages, one from parent to child and one from child to parent. Messages are computed with separate MLPs over [h_u^{t-1}, h_v^{t-1}, e], then summed over parents and children and combined with a residual update.
• �� Goal/premise encoding: the goal and each premise are encoded by separate, non-shared GNNs. Two 1x1 convolutions expand node depth from 128 to 512 and 1024 before max pooling yields a fixed-size embedding.
• �� Prediction heads: the tactic head uses two fully connected layers plus softmax over 41 tactics. The combiner concatenates goal, premise, and elementwise product, then uses three fully connected layers to score premise usefulness.
• �� Search loop: at proof time, the system selects the top-5 tactics, ranks all 19,262 candidate premises, keeps the top-20 as parameters, and uses HOList/DeepHOL breadth-first search to close goals recursively.

The main benchmark is HOList, built from the HOL Light complex-analysis corpus. Training data come from 10,200 top-level theorems and about 375,000 proof steps. Evaluation is the standard HOList validation split with 3,225 held-out theorems. The authors report end-to-end proof closure as the primary metric, because it measures whether a model can actually help prove new theorems. They also track tactic-prediction accuracy and relative premise-ranking accuracy during training, then select the best checkpoint for full prover evaluation. Crucially, they compare multiple graph representations and multiple hop counts under the same architecture.

The strongest result is 49.95% proof closure for the 12-hop subexpression-sharing model. This substantially outperforms the previous HOList WaveNet baseline at 32.65% and the bag-of-words max-pooling baseline at 37.98%. The 0-hop subexpression-sharing model already reaches 40.86%, which shows that the graph representation itself is powerful even before deep propagation. Increasing hops generally helps for ASTs and subexpression-sharing graphs: AST rises from 40.18% at 0 hops to 46.66% at 8 hops; subexpression sharing rises from 40.86% to 47.22% at 8 hops and 49.95% at 12 hops. By contrast, leaf sharing collapses with message passing, confirming that not all compression schemes are equally useful.

In practice, this work is relevant wherever formal proof assistance matters. A prover integrated with a GNN ranker can recommend tactics and premises to mathematicians, speeding up interactive proofs. The same setup can support large formal verification projects, where engineers need to search thousands of lemmas and definitions quickly. More broadly, the representation ideas may transfer to symbolic reasoning tasks such as program verification, specification checking, and structured knowledge retrieval, provided the target system exposes a theorem-proving style search loop.

The approach relies on a specific theorem-proving environment and a fixed tactic vocabulary of 41 actions, so portability is limited. It also requires scoring 19,262 candidate premises, which is expensive and makes training/evaluation slow. The best result is tied to subexpression-sharing graphs in HOList's complex-analysis domain, so broader generalization remains an open question. Finally, the sensitivity to representation choices suggests that more principled theory of graph construction and context propagation is still needed.