Source-linked AI summary
Deep Network Guided Proof Search
Sarah Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk
TL;DR
Automated theorem provers struggle with large fact libraries and costly clause evaluation, motivating learned internal guidance. The paper trains deep networks on Mizar ATP proof traces to guide E’s clause selection, combining neural and fast heuristic phases. This approach improves proving performance and finds ATP proofs for 7.36% of previously unresolved Mizar statements, raising the corpus coverage from 56% to 59%.
Problem
Modern ATPs perform poorly with large fact libraries, while internal clause guidance must overcome the high cost of neural-network inference.
Method
Deep neural networks trained on existing ATP proofs guide clause selection in E through interleaved hybrid heuristics and a two-phase search.
Results
7.36% of previously unresolved hard statements received ATP proofs, while a simple convolutional approach proved 4.34% versus 2.33% for the unguided approach.
Takeaways & Limitations
Deep network guidance can improve first-order prover performance, especially on harder theorems requiring deeper search, when combined with hand-crafted strategies.
Takeaways & Limitations
The approach is computationally expensive, using 30 minutes per proof compared with 15 minutes in previous work.
Abstract
from arXiv · showhide
Deep learning techniques lie at the heart of several significant AI advances in recent years including object recognition and detection, image captioning, machine translation, speech recognition and synthesis, and playing the game of Go. Automated first-order theorem provers can aid in the formalization and verification of mathematical theorems and play a crucial role in program analysis, theory reasoning, security, interpolation, and system verification. Here we suggest deep learning based guidance in the proof search of the theorem prover E. We train and compare several deep neural network models on the traces of existing ATP proofs of Mizar statements and use them to select processed clauses during proof search. We give experimental evidence that with a hybrid, two-phase approach, deep learning based guidance can significantly reduce the average number of proof search steps while increasing the number of theorems proved. Using a few proof guidance strategies that leverage deep neural networks, we have found first-order proofs of 7.36% of the first-order logic translations of the Mizar Mathematical Library theorems that did not previously have ATP generated proofs. This increases the ratio of statements in the corpus with ATP generated proofs from 56% to 59%.
1 Introduction
The paper argues that internal, deep-network guidance can improve automated theorem-proving search, despite the cost of neural inference. Its hybrid and two-phase strategies aim to preserve high-quality clause choices while allowing fast heuristics to complete the search.
- Motivation: Modern ATPs perform poorly with large fact libraries, motivating learned guidance for selecting useful premises and clauses.Internal guidance can exploit the complete proof state, unlike external lemma selection.
- Motivation: Deep neural architectures are proposed as guidance for the combinatorial search involved in proving mathematical theorems.
- Challenges: Neural guidance is computationally challenging because evaluating one clause can take as long as hundreds or thousands of prover superposition steps.The guidance must therefore provide sufficiently high-quality suggestions to produce a positive effect.
- Approach: Interleaving neural guidance with hard-coded heuristics improves performance over using the neural network alone to choose the next clause.
- Approach: A two-phase strategy uses slow network guidance first and fast heuristics afterward, giving the remaining search a better starting point.Without the second phase, the network-guided search often processes only 1% of the clauses processed by a fast-heuristic search.
- Approach: Spending roughly half the time guiding the search and half finishing it improves over lower-quality clause selection that may miss crucial clauses.
2 Related Work
Prior work used hand-engineered or classical learning methods to guide automated theorem provers, while more recent efforts began applying deep learning to premise selection and theorem proving.
- Earlier guidance: Earlier theorem-proving guidance methods used multilayer perceptrons, k-nearest neighbors, hand-crafted clause features, or knowledge-based approaches.
- Deep learning approaches: Recent deep-learning approaches applied convolutional networks to Mizar premise selection and neural architectures to tableau-style or differentiable theorem proving.
3 Theorem Proving Preliminaries
The paper studies clause selection in the saturation-based prover E using problems and proof traces from the Mizar Mathematical Library. Its evaluation distinguishes previously solved easy statements from 25,361 hard statements without earlier ATP proofs.
- The prover E: E converts first-order inputs to clausal normal form and performs saturation-based proof search over clauses.
- The prover E: At each search step, E selects an unprocessed clause, generates its consequences, and moves it into the processed set.
- The prover E: The clause-selection heuristic strongly affects how quickly E finds a proof, and E’s auto mode selects search parameters expected to work well.
- The prover E: Hybrid heuristics combine multiple clause-selection criteria, such as FIFO ordering and shortest-clause selection, through separate rankings.
- Evaluation setting: Given fixed time and memory limits, adding machine-learning classification to clause selection can increase the number of statements proved.
- Mizar problems: The Mizar Mathematical Library is a large formal mathematics library translated into first-order logic for automated-reasoning experiments.
- Mizar problems: Of 57,882 Mizar first-order theorems, 32,521—about 56%—had at least one ATP proof, totaling 91,877 distinct ATP proofs.
- Mizar problems: The networks were trained and evaluated on 91,877 proofs, while the 25,361 conjectures lacking an ATP proof were designated hard statements.
4 Deep Networks
The paper develops neural clause-selection guidance for E using shared embedding-and-combiner architectures, then compares convolutional, WaveNet, and recursive embedding networks. Models are trained on existing ATP proof traces and integrated into proof search to score unprocessed clauses.
- Overall architecture: The system embeds a negated conjecture and an unprocessed clause into fixed-size vectors, then combines them into a clause-selection score.The score is used as a heuristic because the current processed-clause set is omitted for simplicity and speed.
- Overall architecture: At proof time, E processes the unprocessed clause with maximum predicted probability, with training targets set to 1 for proof-used clauses and 0 otherwise.The output probabilities are trained with logistic loss.
- Embedding architectures: Three embedding architectures are evaluated: shallow convolutional networks, WaveNet-style networks for long-range dependencies, and recursive networks whose topology follows formula syntax trees.The same overall guidance architecture supports all three embedding choices.
- Convolutional models: The convolutional models use three one-dimensional layers with patch size 5, stride 1, rectified-linear activations, and varying feature dimensions.These relatively shallow models were motivated by good results on related premise-selection tasks.
- WaveNet models: WaveNet models use three blocks of seven dilated convolutional layers, with dilation factors from 1 to 64, gated activations, residual connections, and optional dropout.Symmetric rather than causal convolutions are used because the task is discrimination rather than generation.
- Recursive models: Recursive networks construct their topology from first-order formula parse trees, sharing layer weights across nodes of the same type and using tree LSTMs or fully connected layers for internal nodes.The tree represents applications, disjunctions, conjunctions, and negations, while learned symbol embeddings occur at the leaves.
5 Experimental Results
The experiments evaluate neural clause guidance from proxy accuracy through theorem-proving performance, culminating in tests on previously unproved Mizar statements. Hybrid and switched strategies outperform simpler alternatives, with deep guidance proving a substantial fraction of hard statements despite inference costs.
- Evaluation protocol: The evaluation progresses from clause-use prediction to guidance on 9,159 holdout tasks and finally to 25,361 Mizar statements without prior ATP proofs.The final test is the most computationally expensive and uses only the best-performing networks from earlier tasks.
- Accuracy evaluations: 81.5% accuracy is achieved by WaveNet 640 with dropout when predicting whether clauses are used in final proofs.Many CNN and WaveNet models also outperform the other evaluated models, but evaluation speed varies widely.
- Guidance design: Hybrid guidance outperforms both Auto and pure CNN heuristics at lower processed-clause limits, but resource demands cause performance to bottom out around 7,500 clauses.The hybrid alternates CNN and Auto guidance while retaining the overhead of neural evaluation.
- Guidance design: The switched approach is the strongest guidance strategy because it uses Auto after neural guidance to avoid resource exhaustion and compensate for slow proof closure.This sequential strategy lets neural guidance select useful clauses before fast heuristics complete the search.
- Easy statements: Neural guidance improves the Auto baseline across processed-clause limits, although gains on the easy holdout dataset are minor because Auto already performs well.CNN models perform strongly, while WaveNet models with better clause-prediction accuracy perform less well on proof guidance.
- Experimental scope: The hard-statement evaluation is constrained by a rough over-approximation of necessary premises, sometimes expanding dependencies from about 10–20 to thousands.These statements also resisted E and Vampire under 15-minute timeouts with default settings.
- Hard statements: Premise selection is important for hard statements because large initial premise sets impose a greater clause-evaluation cost on deep network guidance.Different premise-selection models can produce complementary starting premise sets, and the switched approach outperforms unguided search in these experiments.
- Hard statements: 86% more hard statements are proved by simple CNN guidance than by unguided search, rising from 2.33% to 4.34%.Across all methods, 1,866 hard statements are proved, representing 7.36% of the 25,361-statement corpus.
6 Conclusion
The paper demonstrates that deep neural networks can guide first-order proof search, but effective proving requires combining neural guidance with faster hand-crafted strategies. Accuracy and inference speed jointly determine proving power, while computational cost and syntactic representations remain important limitations.
- Deep neural networks guide first-order proof search by augmenting given-clause selection with learned ranking.
- Neural guidance increases successful proofs only when a deep-guided phase is followed by faster combinatorial search.
- Prediction accuracy and inference speed both affect proving power: a more accurate WaveNet proves fewer theorems than a cheaper CNN under equal time limits.
- The approach is computationally expensive, using 30 minutes per proof versus 15 minutes in previous work.
- Specialized deep-learning hardware may reduce computational overhead and improve the efficiency and quality of higher-performing models.
- Purely syntactic inputs may not produce representations strong enough to capture the semantic content of mathematics.
Selecting Auto Baseline
The experiments compare E prover’s dynamically selected Auto heuristics and use the best-performing fixed heuristic, Auto208, as the baseline. Switching between Auto200 and Auto208 has little effect on final results.
- The baseline is the hybrid heuristic that performs best on the holdout set.
- E prover’s --auto flag dynamically chooses a hybrid selection heuristic, term ordering, and literal selection strategy from conjecture features.
- 52.5% of proofs generated with --auto use Auto208, which proves more theorems than --auto on the full dataset under the reported limits.
- Switching from Auto200 to Auto208 has very little impact on the final result.
- Auto208 is used as the comparison baseline because it was the best-performing heuristic in these experiments.