Source-linked AI summary
Graph Representations for Higher-Order Logic and Theorem Proving
Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, Christian Szegedy
TL;DR
Higher-order theorem proving remains challenging for deep learning, and graph-based formula representations are not well established. This paper applies message-passing GNNs to higher-order logic proof search and reports improved HOList results, including a 49.95% proof-closing rate for its best model.
Problem
The paper addresses how to represent higher-order logic formulas for deep learning, where no well-established graph-based method exists and prior TreeRNNs have not shown strong gains over baselines.
Source: §1 · p. 1Method
The authors represent formula syntax trees as graphs with child and parent edges, apply message-passing GNNs, and train them by imitating human proofs for tactic and argument prediction.
Source: §1 · p. 1Results
49.95% of proofs were closed by the 12-hop shared subexpression GNN, versus 32.65% for baseline models in the HOList paper and 38.9% for its best reported reinforcement learning experiment.
Source: §5.2 · p. 6Takeaways & Limitations
The experiments indicate that GNN proof search benefits from subexpression sharing and additional message-passing steps, and that top-down message passing outperforms bottom-up.
Source: §5.2 · p. 6, §6 · p. 7The system predicts tactics and arguments from the current sub-goal conclusion while ignoring local assumptions that could be crucial to a proof.
Source: §6 · p. 7
Abstract
from arXiv · showhide
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.
1 Introduction
HOList provides a benchmark for learning-based mathematical reasoning, while prior neural theorem-proving models leave room for stronger representations. This work applies message-passing GNNs to formula graphs and reports improved higher-order proof search, including state-of-the-art performance.
1 Introduction
- HOList combines a stateless theorem-proving API, a benchmark of over twenty thousand mathematical theorems and proofs, and the DeepHOL neural prover.Source: §1 · p. 1
- Earlier TreeRNNs and sequence models such as LSTMs showed no strong gains over logical-reasoning baselines, which the authors attribute to missing parent context.Source: §1 · p. 1
- GNNs significantly improve higher-order proof search and achieve state-of-the-art performance by a wide margin; the best model proves nearly 50% of validation theorems.Source: §1 · pp. 1–2
- The paper models formula syntax trees as graphs with child and parent edges, applies message-passing GNNs, and learns by imitating human proofs.Source: §1 · p. 1
- The authors report that emphasizing subexpression context outperforms the alternative message-passing direction.Source: §1 · pp. 1–2
2 Related Work
Prior work applies neural methods to higher-order reasoning and proof assistance, but its tasks and representations differ. The paper contrasts those approaches with graph-based, end-to-end proof search that can use context across shared subexpressions.
2 Related Work
- GNNs are a family of graph-structured-data neural networks applied across domains, and prior work argues they can manipulate structured knowledge.Source: §2 · p. 2
- Wang et al. (2017) use GNNs for premise selection, whereas this work predicts tactics and arguments at each proof step and evaluates theorems actually proved.Source: §2 · p. 2
- Unlike Wang et al. (2017), the authors find shared-subexpression representations stronger than trees, with type information and a function-application node supporting uniform treatment of variables, abstractions, and quantifiers.Source: §2 · p. 2
- GamePad, TacticToe, CoqGym, and Proverbot9001 use imitation learning on human proofs collected from Coq and HOL4.Source: §2 · p. 2
- The authors choose HOList over GamePad and CoqGym because it spans varied mathematics and simplifies evaluation while guiding proof search.Source: §2 · p. 2
- Formalization efforts use interactive higher-order proof assistants such as Coq and HOL Light, while tactic-level automation is comparatively recent.Source: §2 · p. 2
- TreeRNNs constrain information flow across syntax trees and assign a subexpression the same embedding regardless of context, which may limit encoding long-distance semantic information.Source: §2 · p. 2
- Message-passing GNNs update node embeddings from children and parents, and shared subexpressions can incorporate context from multiple occurrences.Source: §2 · p. 2
3 Graph Representations of HOL
The paper converts HOList higher-order logic S-expressions into directed graphs based on abstract syntax trees. It compares ordinary trees with variants that share nodes, alter connectivity, or transform variable labels.
3 Graph Representations of HOL
- HOList S-expressions encode function applications with the token a and variables with v, alongside type and name information.Source: §3 · p. 2
- Sharing subexpressions reduces the illustrated graph from 27 nodes to 15, and the amount of sharing increases as terms grow.Source: Figure 1 · p. 3, §3 · p. 3
- S-expressions represent HOL abstract syntax trees as directed graphs with edges to children and parents; child-index labels preserve the original string structure.Source: §3 · p. 3
- The authors compare plain ASTs with subexpression sharing, leaf sharing, variable blinding, random edges, and top-down-only edge variants.Source: §3 · p. 3
- Subexpression sharing merges syntactically equal expressions, including types; a shared variable node can have multiple parents tracking its original occurrences.Source: §3 · p. 3
- Leaf sharing merges only leaves with identical tokens, while variable blinding renames variables to x without merging their distinct graph nodes.Source: §3 · p. 3
- Restricting edges to bottom-up flow resembles TreeRNNs, whereas top-down flow lets nodes receive context without seeing their children.Source: §3 · p. 3
- Adding three labeled random outgoing edges per node tests whether extra connectivity helps information propagate through the graph.Source: §3 · p. 3
4 Model Architecture
The architecture embeds higher-order goals and premises with message-passing GNNs, then predicts tactics and scores candidate premises to guide proof search.
4.1 Graph Neural Networks
- Each labeled logic graph is embedded over T rounds of message passing, with parent- and child-derived messages summarized separately to update each node.The final node embeddings carry information from each node’s T-hop neighborhood.Source: §4.1 · p. 4
4.2 Complete Model Architecture
- Two GNNs with unshared weights embed goal and premise graphs; node features expand from 128 to 512 and then 1,024 dimensions before max pooling.The resulting goal and premise embeddings are each size 1,024.Source: §4.2 · p. 4
- The model predicts from 41 tactics and scores each premise for a goal using concatenated embeddings, their element-wise product, and sigmoid cross-entropy.The tactic classifier uses fully connected layers to produce softmax logits.Source: §4.2 · p. 4, Figure 3 · p. 5
- Trained on human HOList proofs, the model guides breadth-first search by retaining the top 5 tactics and top 20 premises from 19,262 theorem-database entries.A successful tactic may create subgoals, and the top-level goal closes when one proof-search branch closes all its subgoals.Source: §4.2 · p. 4
- Unlike earlier premise-selection work, the model generates new tactic-parameter lists for each subgoal rather than using one list for the top-level goal.Source: §4.2 · p. 4
5 Experiments
Experiments evaluate proof closure on HOList and show that a 12-hop shared-subexpression GNN outperforms the reported baselines. Results also show that representation choices, message-passing direction, and model depth affect proof performance.
5.1 Evaluation Metrics
- Evaluation uses end-to-end theorem proving on 3,225 held-out validation theorems, with proof closure as the primary metric.Tactic and parameter prediction metrics serve as training proxies because running the prover during training would slow it by several orders of magnitude.Source: §5 · p. 5, §5.1 · pp. 5–6
5 Experiments
- The training set derives from 10,200 top-level theorem proofs, comprising around 375,000 proof steps, with the 19,262 corpus theorems and definitions eligible as premises according to sequence order.Source: §5 · p. 5
5.2 Results and Analysis
- 49.95% of proofs are closed by the 12-hop shared-subexpression GNN, versus 32.65% for HOList baselines and 38.9% for the best reported reinforcement-learning experiment.The bag-of-words model closes 37.98% of proofs.Source: Table 1 · p. 5, §5.2 · p. 6
- More message-passing hops increase proof closure for ASTs with and without subexpression sharing, while variable blinding causes a significant performance drop.For the shared-subexpression representation, 12 hops yield 1.93-step proofs on average versus 1.86 for zero hops, and successful tactic applications rise from 33.8% to 38.6%.Source: §5.2 · p. 6
- Random edges improve the 2-hop network but not networks with four or more hops, where their benefits diminish and become harmful.Source: §5.2 · p. 6
- Top-down message passing significantly outperforms bottom-up, while allowing both directions gives the best performance.The authors interpret this as evidence that context from where subexpressions occur in the larger formula can matter more than the subexpression itself.Source: §5.2 · p. 6
- Leaf sharing compresses tree representations by approximately 40% but substantially reduces performance, with message-passing models falling below the 0-hop baseline.Source: §5.2 · p. 6
5.3 Implementation Details
- Implementation uses 128-dimensional node embeddings and message passing, with positive and sampled negative premise pairs trained using cross-entropy and AUCROC losses.The combined loss weights tactic cross-entropy at 1.0, pairwise-score cross-entropy at 0.2, and AUCROC at 4.0.Source: §5.3 · pp. 6–7
6 Conclusions and Future Work
The paper reports that GNNs improve imitation-learning proof search on HOList, with results sensitive to graph structure and message-passing depth. The experiments omit local assumptions when representing goals, a limitation the authors identify for future work.
6 Conclusions and Future Work
- GNNs significantly improve previous state-of-the-art imitation-learning results on the HOList theorem set and proof-search environment.The paper reports stronger performance than non-structured representations, especially when graphs permit subexpression sharing.Source: §6 · p. 7
- The experiments represent goals using only each sub-goal's conclusion, ignoring local assumptions that could be crucial to proof.The authors propose incorporating the local assumptions list in future goal embeddings.Source: §6 · p. 7
A.1 Statistics over the Theorem Database
The statistics show that shared-subexpression graphs reduce theorem graph sizes, while graph depth suggests 12 message-passing hops may not suffice to propagate information across all nodes.
A.1 Statistics over the Theorem Database
- Shared-subexpression representations significantly reduce graph sizes in the HOList theorem database.The reduction nearly eliminates the tail of the graph-size distribution.Source: §A.1 · p. 9
- The shared-subexpression representation almost eliminates the tail of the graph-size distribution.Source: §A.1 · p. 9
- Twelve message-passing hops may not propagate information between all leaves and the root, or vice versa; more hops might improve performance.The measured depth is the maximal path length from a graph's root node.Source: §A.1 · p. 9