Source-linked AI summary
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, Josef Urban
TL;DR
Large-theory automated proving needs premise selection that can identify useful facts among thousands of available premises. The paper combines exact proof-dependency analysis with kernel-based learning and reports about a 50% improvement over Vampire/SInE on its benchmark. The results also show that human premise selection remains ahead as the library grows, marking a challenge for stronger automated reasoning.
Problem
Large mathematical theories expose automated theorem provers to thousands of premises, while only a fraction are typically needed for a proof.
Method
The paper combines exact minimal proof-dependency analysis with a kernel-based machine-learning algorithm for ranking useful premises.
Results
About 50% improvement was achieved with kernel-based learning over state-of-the-art general premise-selection heuristics such as SInE.
Takeaways & Limitations
Learned premise selection can recommend relevant prior theorems and definitions, shielding ATP systems from thousands of irrelevant axioms.
Takeaways & Limitations
As the library grows, human premise selection increasingly outperforms the evaluated algorithms.
Abstract
from arXiv · showhide
Smart premise selection is essential when using automated reasoning as a tool for large-theory formal proof development. A good method for premise selection in complex mathematical libraries is the application of machine learning to large corpora of proofs. This work develops learning-based premise selection in two ways. First, a newly available minimal dependency analysis of existing high-level formal mathematical proofs is used to build a large knowledge base of proof dependencies, providing precise data for ATP-based re-verification and for training premise selection algorithms. Second, a new machine learning algorithm for premise selection based on kernel methods is proposed and implemented. To evaluate the impact of both techniques, a benchmark consisting of 2078 large-theory mathematical problems is constructed,extending the older MPTP Challenge benchmark. The combined effect of the techniques results in a 50% improvement on the benchmark over the Vampire/SInE state-of-the-art system for automated reasoning in large theories.
1 Introduction
The paper combines precise proof-dependency analysis with machine learning for premise selection in large formal mathematical libraries. It evaluates these techniques through an extended benchmark of 2078 mathematical problems.
- The paper’s two-phase approach combines minimal dependency analysis with machine learning to improve theorem proving in large formal mathematical libraries.The dependency analysis supplies precise proof data, while machine learning learns which premises are useful.
- Minimal dependency data supports ATP-based re-verification and provides a repository of solved problems for training premise-selection algorithms.
- A new kernel-based machine-learning algorithm improves premise selection by estimating which previous theorems and definitions are useful for new conjectures.
- Learned premise selection shields ATP systems from thousands of irrelevant axioms and supports automated proving over large existing libraries.
- The evaluation uses a new large-theory benchmark extending the older MPTP Challenge with 2078 related mathematical problems.
2 Automated Reasoning in Large Theories (ARLT)
Large formal theories create challenging ATP problems because they contain many semantically rich premises, motivating heuristic and inductive methods evaluated on large mathematical benchmarks.
- Large formal theories contain semantically rich corpora that make brute-force deductive search inadequate for many automated-reasoning tasks.
- SInE is a successful symbolic preprocessor, especially for domains with many hierarchical definitions.
- Machine-learning premise selection is effective in hard mathematical domains because previous verified proofs provide guidance among many nontrivial lemmas and theorems.
- Automated reasoning in large theories therefore uses data-driven combinations of heuristic, inductive, and deductive methods.
- Large-theory benchmarks such as the MPTP Challenge enable rigorous evaluation of AI methods on thousands of real-world mathematical problems.
3 Computing Minimal Dependencies in Mizar
The Mizar dependency analysis exposes suppressed proof dependencies by decomposing articles into micro-articles and greedily minimizing their environments.
- Fine-grained dependency analysis refactors Mizar articles into single-item micro-articles and computes minimal dependencies for each item.The resulting dependencies include both syntactic items and semantic items such as theorems and typings.
- Interactive proof assistants can suppress logical and mathematical steps, so complete dependency analysis must expose facts omitted from the author’s proof text.
- Mizar environments conservatively import background knowledge, which motivates greedy minimization to retain only items sufficient for verification.
- The minimization produces truly minimal dependencies, meaning that removing any dependency causes verification to fail, although the process can be time consuming.
- The benchmark dependency data covers 33 Mizar articles from the MPTP2078 problem set and compares fine-grained dependencies with MPTP approximations.
4 Premise Selection in Large Theories by Machine Learning
Premise selection addresses ATP degradation in large theories by estimating which premises are useful from thousands of available candidates.
- Premise selection estimates which small subset of thousands of available premises is useful for constructing an ATP proof.
Definition 1 (Premise selection problem)
Premise selection ranks existing premises by their predicted usefulness for proving a new conjecture, using proof dependencies and formula features to train machine-learning classifiers. The paper frames this as learning from precise formal proof corpora while acknowledging limits from single textbook proofs, human-authored training data, and feature choices.
- Premise selection predicts which premises from a large theory are likely to help an automated prover construct a proof of a new conjecture.
- Precise Mizar dependency analysis supplies a proof matrix and formula features for training premise-selection algorithms.The proof matrix records direct dependencies, while features encode symbols and subterms appearing in formulas.
- The training target is typically the single premise set used in a theorem's existing Mizar proof, rather than a collection of alternative proofs.
- The corpus uses human-authored formal proofs, and the chosen feature characterization is acknowledged as arbitrary and open to improvement.The paper notes that better features may correspond more closely to concepts relevant for theorem selection.
- The ranking approach orders premises by predicted usefulness and selects the highest-ranked subset for the conjecture.
4.1 A Naive Bayes Classifier
The naive Bayes baseline estimates whether each premise is useful from the conjecture's expressed features. Under its independence assumption, the resulting classifier is essentially linear in those features.
- Naive Bayes estimates the probability that a premise is used for a conjecture given the conjecture's expressed features.
- The classifier applies Bayes-style conditional probabilities to the premise-use event and the features present in the conjecture.
- The naive-Bayes classifier is essentially a linear function of the conjecture features after a monotonic transformation.
4.2 Kernel-based Learning
Kernel-based learning extends premise selection beyond linear classifiers by using similarity-based function spaces and regularization. The approach addresses overfitting and optimization concerns, while its empirical relevance depends on how classifier loss relates to ATP problems.
- Kernel-based learning provides a framework for testing better parameters and nonlinear functions than the linear naive Bayes classifier.
- Lower expected loss on training proofs does not necessarily yield more ATP-solved problems because training proofs may differ from ATP reasoning paths.
- A kernel acts as a similarity measure, and its function space compares an input with formulas while weighting those comparisons.
- Regularization penalizes complex functions, helps ensure a solution exists, and is intended to reduce overfitting.
- Kernel methods can outperform naive Bayes because suitable nonlinear kernels capture nonlinear dependencies and regularization controls model complexity.
4.3 MOR Experimental Setup
The MOR setup turns premise selection into simultaneous multi-output learning: one classifier is trained for every premise, with shared kernel computations used to improve efficiency. The method uses square loss and solves the resulting optimization through matrix-based procedures.
- MOR extends preference learning into a kernel-based multi-output ranking algorithm for premise selection.
- The setup uses square loss and reformulates the optimization with premise-classifier parameters, a kernel matrix, and a label matrix.
- Because each premise requires a classifier, MOR learns all premise weights simultaneously rather than training each classifier separately.
- For fixed regularization and Gaussian-kernel parameters, the optimal weights are obtained through matrix computations, while parameter values are selected by grid search and cross-validation.
5 Data: The MPTP2078 Benchmark
The MPTP2078 benchmark expands the earlier MPTP Challenge to 2078 problems and evaluates precise dependency pruning alongside heuristic pruning and unpruned large-theory problems. Its three datasets share conjectures but differ in redundant axioms and premise counts.
- Evaluation design: The benchmark evaluates minimized dependency data for direct re-proving and premise-selection training, together with the kernel-based MOR algorithm.These effects are assessed on the newly created large-theory benchmark.
- Benchmark construction: 2078 problems extend the older 252-problem MPTP Challenge using all problems from 33 Mizar articles and more precise dependency analysis.The benchmark preserves the earlier benchmark’s two divisions while enlarging its problem set and premise information.
- Benchmark divisions: The chainy division attacks each conjecture with all previous Mizar Mathematical Library contents, without premise selection.Its chronological dependencies emulate the library’s growth and the use of all existing knowledge.
- Benchmark divisions: The bushy division uses fine-grained dependency information to prune premises, testing how effectively automated theorem provers work with precise advice.This setting reflects proof-assistant use of an explicit premise list selected from a large library.
- Dataset comparison: 31.5 average premises in fine-grained bushy problems versus 74 in heuristically pruned bushy-old and 1976.5 in unpruned chainy problems.All three datasets contain the same conjectures; they differ in redundant axioms, and the table summarizes these averages.
6 Experiments and Results
The experiments evaluate fine-grained dependency pruning, learned premise ranking, and their combined effect on Vampire over the 2078-problem MPTP benchmark. The combined learning strategies substantially outperform unpruned and SInE-based baselines, while performance declines as more problems are included.
- 6.1 Using the Fine-Grained Dependency Analysis for Re-proving: With fine-grained dependency pruning, Vampire solves 1105 of 2078 problems, an 8% improvement over the 1023 solved with heuristic pruning.Unpruned Vampire solves 548 problems, so pruning nearly doubles the number solved relative to the unpruned setting.
- 6.2 Combining Fine-Grained Dependencies with Learning: MOR places 88% of used premises within its top 50 ranked premises, compared with around 80% for SNoW.This measures average recall against premises used in the original Mizar proofs.
- 6.3 Combining It All: ATP Supported by Learning from Fine Dependencies: 50% improvement over Vampire auto-mode is achieved by the combined MOR runs with the two strategies having the largest joint coverage.The corresponding combined SNoW runs improve over auto-mode by 44%.
- 6.3 Combining It All: ATP Supported by Learning from Fine Dependencies: The solved-problem ratio decreases for all algorithms as the library grows, and human selection increasingly outperforms automated strategies beyond the initial 800 problems.MOR remains comparable to the Vampire-bushy setting through roughly the initial 800 problems.
7 Conclusion and Future Work
The paper reports substantial gains in large-theory automated theorem proving from precise proof-dependency analysis and improved premise-selection learning, while identifying remaining opportunities for better selection and broader proof guidance.
- Learning from exact previous proof dependencies improved ATP performance by about 44% with naive Bayes and about 50% with kernel-based methods.
- The benchmark performance remains below what better premise selection could achieve, with at least 1105 problems provable compared with 824 currently proved within 10 seconds.
- The authors identify finer and faster dependency analysis, alternative MOR parameterizations, richer formula features, and learned ATP strategies as promising improvements.