Source-linked AI summary
DeepMath - Deep Sequence Models for Premise Selection
Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban
TL;DR
Automated theorem proving needs effective premise selection because exhaustive reasoning over large formal corpora quickly becomes impractical. This paper develops two-stage neural sequence models using definition-aware embeddings, reports strong premise-selection results without hand-engineered features, and finds complementary gains from ensembling. The models remain shallow and cannot capture high-level mathematical properties.
Problem
Automated theorem proving is limited by the difficulty of selecting relevant facts from large formal corpora, where exhaustive reasoning faces combinatorial explosion.
Method
The paper uses a two-stage neural sequence approach with character-level embeddings followed by definition-based word-level embeddings for premise selection.
Results
Neural models compete with hand-engineered features, while definition-based embeddings improve generalization for infrequent symbols and ensembling produces superior results.
Takeaways & Limitations
Neural premise selection can aid large-scale automated logical reasoning and help find many new proofs.
Takeaways & Limitations
The relatively shallow models cannot capture high-level properties of mathematical statements.
Abstract
from arXiv · showhide
We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving on a large scale.
1 Introduction
Automated theorem proving is limited by weak formal parsing and reasoning, while premise selection is needed to control combinatorial explosion. The paper develops neural methods for selecting relevant facts and highlights several contributions, including definition-aware embeddings and complementary ensembles.
- Formal proof production is often impractical without automation because current systems have limited assistance capabilities.
- Automated theorem proving faces bottlenecks in autoformalization and reasoning over already formalized proofs.
- Exhaustive reasoning over many facts quickly encounters combinatorial explosion, making careful premise selection essential.
- The paper trains deep neural networks to select a limited set of relevant facts for proving new conjectures.
- The contributions include neural premise selection without hand-engineered features, architecture comparisons, definition-aware embeddings, and complementary ensembling.
2 Formalization and Theorem Proving
Interactive theorem proving formalizes mathematics in computer-understandable detail, while automated theorem proving attempts conjectures fully automatically. Large formal libraries support both activities, and hammers combine relevance estimation with ATP search to automate substantial portions of theorem proving.
- Interactive theorem proving encodes theorems, definitions, proofs, and theories in complete detail for computer understanding.
- ITP systems support human-assisted formalization and proving, whereas ATP systems attempt conjecture proofs fully automatically.
- The Mizar Mathematical Library contains over 50,000 lemmas, alongside core libraries with thousands of lemmas in other ITP systems.
- Automated Reasoning in Large Theories systems called hammers estimate theorem relevance, translate theories, and guide ATP searches.
- Recent evaluations fully automatically proved 40% of Mizar and Flyspeck theorems.
3 Premise Selection, Experimental Setting and Previous Results
Premise selection predicts which premises will help an ATP prove a conjecture, using the chronologically ordered Mizar corpus and E prover setting. Earlier systems relied on hand-crafted features and achieved substantial but limited automated coverage.
- Premise selection predicts premises likely to produce an automatically constructed proof for a conjecture under fixed ATP resource limits.
- The experiments use Mizar Mathematical Library version 4.181.11473 and E prover version 1.9.
- The Mizar corpus contains 57,917 proved theorems and 88,783 additional formulas translated into first-order logic.
- Because later Mizar theorems can refer only to earlier theorems, the corpus is chronologically ordered for training and evaluation.
- Earlier evaluations proved 40% of theorems with a 14-method portfolio, while the best single method proved 27.3%.These methods used learners such as k-nearest-neighbors and naive Bayes with hand-crafted formula features.
4 Motivation for the use of Deep Learning
Deep learning is motivated by its ability to learn representations from sequential inputs without hand-tuned features. The Mizar corpus is a demanding sequence-learning setting because statements vary greatly in length and contain many rare words.
- Deep neural networks have extracted useful representations from sequential inputs across several natural-language tasks without hand-tuned features.
- Figure 3 separates conjecture and axiom embeddings before a logistic classifier predicts axiom usefulness, with character- and word-level inputs.
- The architecture comparison includes recurrent, convolutional, and hybrid models for premise selection.
- Mizar formulas are highly structured, so the main challenge arises after parsing rather than from ambiguous natural-language syntax.
- Statement lengths range from 5 to 84,299 characters and from 2 to 21,251 tokens, complicating recurrent processing and batching.
5 Overview of our approach
The approach reduces premise selection to pairwise relevance prediction by separately embedding conjectures and axioms, then ranking their pairs. It progresses from character-level models to word-level models using definition-aware embeddings, avoiding parser and hand-engineered feature requirements.
- Pairwise premise selection: Premise selection is simplified to predicting whether an axiom is useful for a conjecture, using separately embedded sequences and a classifier with logistic loss.Conjecture and axiom embeddings are concatenated before classification.
- Two-stage pipeline: The pipeline trains first-stage character-level models, then builds word-level models on embeddings produced by earlier stages.This staged design reuses stronger embeddings rather than training every representation independently.
- Embedder architectures: Character sequences use 80-dimensional one-hot encoding and are processed by recurrent, convolutional, or recurrent-convolutional embedding networks.The convolutional option uses temporal max pooling to produce fixed-length representations.
- Scope and motivation: Character-level models are limited to word and structural similarity within each embedded axiom or conjecture, motivating the use of earlier definition embeddings.Earlier corpus definitions provide axiom embeddings for symbols occurring in later formulas.
- Definition-aware embeddings: Definition-based word embeddings reuse stage-1 embeddings of entire symbol-defining statements instead of recursively expanding definition chains.Recursive expansion is avoided because definition chains can be deep and expensive to train.
- Implementation choices: The method requires no parser because tokens are embedded independently of grammatical structure, while repeated additional stages produced no measurable gains.A trivial lexer supplies the tokenization, and word-level models use shorter input sequences.
6 Experiments
Experiments evaluate neural premise rankings on Mizar using ranking metrics and ATP proof counts, comparing architectures, a two-stage model, and a handcrafted-feature k-NN baseline. Convolutional and definition-based models perform best, while combining methods proves the largest set of theorems.
- Experimental setup: The evaluation uses 32,524 ATP-provable theorems, with 2,724 conjectures reserved for final evaluation after holdout and validation splits.A separate holdout of 400 conjectures monitors training and selects models and checkpoints.
- Metrics: Average maximum relative rank measures how early all testing premises appear in the model ranking, complementing the computationally expensive proof-count metric.Its motivation is that conjectures are easier to prove when dependencies occur early.
- Metrics: The approximate aMRR evaluation uses all true dependencies and 128 random false dependencies for 400 holdout conjectures, with a best possible value of 0.051.The metric remains nonzero even when every true dependency precedes every false dependency.
- Model comparison: Pure convolutional models outperform recurrent models, and the best ranking model is a word-level CNN using definition embeddings from a character-level two-layer CNN.A word-embedding model with random initialization overfits after 250,000 iterations and underperforms the best character-level model.
- Experimental setup: Models rank premises for each conjecture, and E prover tests the top k premises at k = 16, 32, . . . , 1024 until finding a proof or exhausting the cutoff.The experiments impose soft and hard time limits, a memory limit, and a processed-clauses limit.
- Model comparison: The two-stage definition-based def-CNN significantly outperforms naïve word-CNN embeddings, while shorter-sequence recurrent models outperform longer-sequence recurrent models.Averaging stage-1 and stage-2 prediction scores was also evaluated.
- ATP results: The union of all methods proves 2,218 theorems (80.9%), while neural models alone prove 2,151 (78.4%) on the 2,742-theorem test set.The def-CNN and k-NN union proves 74.25%, exceeding the def-CNN and char-CNN union at 69.8%.
- ATP results: Applying two premise-selection models to previously unproved Mizar statements yields 823 additional automatically proved statements.This result extends evaluation beyond the theorem set already known to be ATP-provable.
7 Conclusions
The models achieved competitive premise-selection performance and helped find many new proofs, although their shallow architectures limit representation of high-level mathematical properties.
- The best sustained test results used max average relative rank, where lower values are better and perfect predictions attain 0.051.Performance was monitored on a 400-theorem holdout set with true-positive premises and 128 randomly selected negatives.
- Simple neural models can compete with hand-engineered features for premise selection and help find many new proofs.
- The models produce real gains in automatic theorem proving despite being relatively shallow networks.
- Their limited representational power prevents them from capturing high-level properties of mathematical statements.