Source-linked AI summary
Premise Selection for Theorem Proving by Deep Graph Embedding
Mingzhe Wang, Yihe Tang, Jian Wang, Jia Deng
TL;DR
Premise selection asks which mathematical statements are relevant to proving a conjecture, especially when theorem-proving search becomes combinatorial. The paper represents higher-order formulas as variable-renaming-invariant graphs, embeds them while preserving edge ordering, and classifies relevance. On HolStep, accuracy improves from 83% to 90.3%.
Problem
Premise selection must identify relevant statements for a conjecture within a theorem-proving search space that can grow combinatorially.
Method
The approach represents higher-order logic formulas as graphs, embeds them into vectors with order-preserving graph updates, and classifies premise relevance.
Results
90.3% accuracy improves the best existing HolStep result from 83% to 90.3%.
Takeaways & Limitations
Graph embeddings provide a state-of-the-art approach to premise selection on the HolStep dataset.
Takeaways & Limitations
The formula-graph construction assumes formulas have no free variables, with free variables first bounded by adding universal quantifiers.
Abstract
from arXiv · showhide
We propose a deep learning-based approach to the problem of premise selection: selecting mathematical statements relevant for proving a given conjecture. We represent a higher-order logic formula as a graph that is invariant to variable renaming but still fully preserves syntactic and semantic information. We then embed the graph into a vector via a novel embedding method that preserves the information of edge ordering. Our approach achieves state-of-the-art results on the HolStep dataset, improving the classification accuracy from 83% to 90.3%.
1 Introduction
Premise selection narrows the combinatorial search in automated theorem proving by identifying statements relevant to a conjecture. The paper proposes graph-based formula embeddings that preserve logical structure and improve HolStep accuracy from 83% to 90.3%.
- Premise selection makes theorem-proving search tractable by narrowing a combinatorially exploding knowledge-base search to relevant facts.
- The method represents formulas as graphs, embeds them into vectors, and classifies statement relevance for premise selection.Graph construction links terms to constituents and quantifiers to their variables.
- Graph representations expose composition, variable binding, and co-reference, making shared formula structure more explicit than token sequences.
- The graph is invariant to variable renaming while preserving quantifier semantics and co-reference.
- 90.3% accuracy improves the best existing HolStep result from 83% to 90.3%.
2 Related Work
Related work spans automated and interactive theorem proving, machine-learning approaches to premise selection and proof guidance, and graph-embedding architectures. The paper distinguishes its method by preserving edge ordering in general graph embeddings for premise selection.
- Existing automated theorem provers struggle to scale to large mathematical libraries because proof-search spaces grow combinatorially.
- Prior premise-selection systems progressed from symbolic heuristics and bag-of-words classifiers to recurrent and convolutional models over formula sequences.
- Proof guidance selects the next clause during proof search, unlike premise selection, which chooses initial relevant statements for a black-box theorem prover.
- Earlier tree-based proof-guidance representations lack the graph method’s invariance to variable renaming and treatment of quantifier binding.
- The paper claims prior deep-learning approaches on general graphs did not preserve edge order, motivating its order-preserving graph embedding.
3 FormulaNet: Formulas to Graphs to Embeddings
FormulaNet converts higher-order logic formulas into variable-renaming-invariant graphs, embeds them through iterative neural message passing, and extends this process to preserve argument ordering.
- 3.1 Formulas to Graphs: The graph construction represents constants, variable values, variable functions, and quantifiers as nodes, with recursive graph operations defined for formula components.The formal construction assumes formulas have no free variables, which can be bounded by adding universal quantifiers.
- 3.1 Formulas to Graphs: FormulaNet converts higher-order formulas into graphs by parsing trees, connecting quantifiers to quantified variables, merging identical leaves, and renaming variables.Variable renaming preserves syntactic and semantic information because graph structure encodes syntax and quantifier binding.
- 3.2 Graphs to Embeddings: Node embeddings begin from one-hot node-name vectors and are repeatedly updated from neighboring nodes before max pooling produces a graph vector.All variables share the initial name VAR or VARFUNC, while constants and quantifiers retain distinct names.
- 3.2 Graphs to Embeddings: The update functions are neural networks trained end to end, and repeated updates expand each node’s receptive field from local to more global graph structure.With zero updates, max pooling of individual node embeddings reduces the model to a bag-of-words representation.
- 3.2 Graphs to Embeddings: Premise relevance is classified from concatenated conjecture and statement embeddings, or from the statement embedding alone in the unconditional setting.Both update functions and classifiers are learned through backpropagation.
- 3.3 Order-Preserving Embeddings: FormulaNet addresses argument-order insensitivity by updating nodes according to their ordered-edge roles in treelets, including head, left-child, and right-child positions.Treelets encode ordered pairs of outgoing edges, and the update uses separate functions for each role.
- 3.3 Order-Preserving Embeddings: The order-preserving updates can embed f(a, b) differently from f(b, a), and can distinguish identical subexpressions occupying different argument slots.In g(f(a), f(a)), the first and second f nodes receive different left- and right-child updates.
- 3.3 Order-Preserving Embeddings: The treelet-based method is called FormulaNet, whereas FormulaNet-basic omits edge-order information.The update functions are neural networks configured with concatenation, fully connected layers, ReLUs, and batch normalization.
4 Experiments
The experiments evaluate graph-based premise selection on HolStep, including its classification setup, main benchmark results, and ablations of graph structure, variable renaming, and update depth.
- Experimental Setup: HolStep evaluates binary premise relevance classification in conditional and unconditional settings, with over two million conjecture-statement pairs and 50% random-prediction accuracy.The dataset contains 11,410 conjectures, including 9,999 for training and 1,411 for testing.
- Main Results: 90.3% conditional and 90.0% unconditional accuracy improve the best existing 83% result, while FormulaNet exceeds FormulaNet-basic by 1%.Table 1 compares test-set accuracy in both settings; the authors attribute the FormulaNet gain to argument-order information.
- Ablation Experiments: Renamed validation exposes large accuracy drops for models trained with original variable names, showing overfitting to name-specific bias rather than robust semantic generalization.The comparison uses original and randomly renamed validation formulas with unchanged semantics.
- Ablation Experiments: Renamed-tree models perform poorly despite renaming invariance, showing that quantifier and coreference structure encoded in the graph is important.The ablation compares graph formats while keeping the training set and validation protocol controlled.
- Ablation Experiments: 81.5% accuracy with zero update steps shows token names alone are informative, while additional steps improve accuracy before diminishing returns after three steps.More update steps incorporate larger graph neighborhoods; a three-step radius can cover reasonably complex expressions.
5 Conclusion
The paper presents a deep learning approach that graph-embeds higher-order logic formulas while preserving syntactic and semantic information. On HolStep, it achieves state-of-the-art classification accuracy, improving from 83% to 90.3%.
- 90.3% classification accuracy on HolStep improves the previous 83% result.
- The approach represents higher-order logic formulas as graphs invariant to variable renaming while preserving syntactic and semantic information.
- A novel embedding method converts each graph into a continuous vector while preserving edge-ordering information.