Source-linked AI summary
MizAR 40 for Mizar 40
Cezary Kaliszyk, Josef Urban
TL;DR
Large-theory AI/ATP methods had often been evaluated on smaller benchmarks, and scaling them to a full mathematical library is challenging. This work develops and deploys a suite of proof-guidance methods for the Mizar Mathematical Library. Fourteen methods prove 40.6% of its theorems fully automatically in 30 seconds, while manual premise selection raises the reported rate to 56.2%.
Problem
Large-theory AI/ATP methods were often developed and evaluated on smaller benchmarks rather than across the whole Mizar Mathematical Library.
Source: §1 · p. 2Method
The authors iteratively improve a suite of scalable AI/ATP methods by learning premise selection from proof data and using successful methods to obtain further proofs.
Source: §2 · p. 3, §2.2 · p. 5Results
40.6% of nearly 58,000 Mizar theorems are proved fully automatically in 30 seconds by 14 parallel methods; manual premise selection raises the rate to 56.2%.
Source: §1 · p. 2, §6 · p. 10Takeaways & Limitations
The authors hope this performance may significantly lower the barrier to formalizing mathematics in Mizar.
Source: §1 · p. 2The large-scale experiments and training data cover only toplevel Mizar theorems without proof-local constants.
Source: §5 · p. 10
Abstract
from arXiv · showhide
As a present to Mizar on its 40th anniversary, we develop an AI/ATP system that in 30 seconds of real time on a 14-CPU machine automatically proves 40% of the theorems in the latest official version of the Mizar Mathematical Library (MML). This is a considerable improvement over previous performance of large- theory AI/ATP methods measured on the whole MML. To achieve that, a large suite of AI/ATP methods is employed and further developed. We implement the most useful methods efficiently, to scale them to the 150000 formulas in MML. This reduces the training times over the corpus to 1-3 seconds, allowing a simple practical deployment of the methods in the online automated reasoning service for the Mizar users (MizAR).
1 Introduction and Motivation
Earlier large-theory AI/ATP methods were often developed and evaluated on smaller benchmarks, while a scalable suite had demonstrated strong performance on Flyspeck. This work applies and develops such methods across the Mizar library, reporting fully automatic and user-assisted results.
1 Introduction and Motivation
- Large-theory AI/ATP methods were often evaluated on smaller benchmarks such as the MPTP Challenge and MPTP2078.The work targets the whole Mizar library rather than a smaller benchmark.Source: §1 · p. 1
- On the June 2012 Flyspeck development, 14 methods running in parallel proved 47% of theorems in 30 seconds without user interaction.The methods used learned guidance from previous proofs for ATP and SMT systems.Source: §1 · pp. 1–2
- The authors frame computer understanding and checking of ordinary mathematical reasoning as a step toward McCarthy’s “Heavy Duty Set Theory” vision.They hope this performance may lower the barrier to formalizing mathematics in Mizar.Source: §1 · p. 2
- 40.6% of nearly 58,000 Mizar theorems are proved in 30 seconds by 14 parallel methods; with manual premise selection, the rate reaches 56.2%.The fully automatic run requires no user interaction.Source: §1 · p. 2
2 Learning Proof Guidance From the MML
The work builds proof guidance through repeated cycles of extracting dependencies, training premise selectors, and using successful selectors to obtain further proofs. It develops scalable selection methods for the MML and combines them with ATP systems.
2 Learning Proof Guidance From the MML
- The workflow iterates between obtaining proof dependencies, training and testing premise selectors on a random subset, and using successful selectors to obtain more proofs.The authors describe a positive feedback loop: stronger methods produce more and better proof data, which can support further learning.Source: §2 · p. 3
2.1 Obtaining Proof Dependencies from the MML
- For 57,897 theorems and toplevel lemmas, MPTP adds typing background formulas heuristically; the authors skip costly Mizar-based proof minimization after it yielded only about 4% performance gain on MPTP2078.Learning uses ATP proofs of heuristically constructed reproving problems, and the passes use only chronologically previous proofs.Source: §2.1 · p. 3
- Successive learning and ATP passes grow the proof-dependency data, first using Vampire proofs, then learned selectors and further iterations.The first pass runs Vampire 3.0 for 300 seconds; later passes use chronologically available proofs.Source: §2.1 · p. 4, Table 1 · p. 4
- 56.23% of toplevel MML theorems are proved using human or AI-based premise selection and their combinations.The iterations yield 32,165 ATP proofs, reaching 32,557 theorems with the final evaluation.Source: §2.1 · p. 4
2.2 Premise Selection Techniques
- Premise selectors use formula symbols, terms, and subterms as features, with Naive Bayes, distance-weighted k-NN, IDF weighting, and LSI variants among the tested methods.The k-NN variants also include recursive dependency weighting.Source: §2.2 · pp. 4–5
- Combining selector rankings, especially by minimum rank or geometric averaging, is reported as successful; boosting produced no significant improvement.The geometric average is motivated by treating aggregated rankings as ratios, given ATP sensitivity to premise counts.Source: §2.2 · p. 5
- Uniform OCaml implementations and C++ versions of the most useful methods improve training speed; partial sorting avoids sorting all 150,000 formulas when only a small premise set is needed.The C++ versions are about twice as fast as their OCaml versions.Source: §2.2 · p. 5
2.3 ATPs and Their Low-Level Guidance
- The work does not develop new ATP strategies for the whole MML, instead using Vampire and E strategies tuned through prior competitions.BliStr-developed E strategies had raised performance on MPTP2078 over E’s auto-mode by 25%.Source: §2.3 · p. 6
3 Experiments and Results
On the 1930-problem sample, the selected 14 methods jointly cover 44%; across the whole MML, 14 parallel methods prove 40.6% in 30 seconds.
3.1 Experiments and Results on a Random Subset of 1930 Problems
- On a random sample of 1930 theorems, methods trained on preceding proof data supplied 32 to 1024 top-ranked premises to ATPs under a 30-second limit.Source: §3.1 · p. 6
- 44% of the 1930-problem subset is covered by the selected 14 methods, while all 70 tested methods solve 968 problems (50.155%).Source: §3.1 · p. 6, Table 3 · p. 7
3.2 Experiments and Results on the Whole MML
- Comparisons with MPTP2078 are only high-level because the MML version, ATP versions, premise slices, and available premises differ.The current method solved 1059 of 2061 corresponding problems in 30 seconds, whereas the cited older benchmark result solved 823 of 2078 in 5 seconds.Source: §3.2 · pp. 7–8
- 40.6% of whole-MML theorems are proved by 14 parallel methods in 30 seconds; the best individual method solves 27.3%, 50% more problems than the previous 18% result.The reported result requires no user interaction.Source: §3.2 · p. 7, Table 4 · p. 8
4 Proofs
The section compares human Mizar proof lengths with ATP proof dependencies, illustrates substantial shortening, and uses these comparisons to inspect the toolchain while noting interpretability limits.
4 Proofs
- The authors caution that comparing Mizar proof lines with ATP dependencies involves choices that are questionable but useful as a first comparison.The shortest ATP proofs are compared with Mizar proofs for 28,892 named theorems having a human or AI-advised ATP proof.Source: §4 · p. 8
- REARRAN1:24’s 534-line Mizar proof contrasts with a shortest ATP proof using 5 dependencies, reusing symmetry with REARRAN1:17.The authors describe the ATP proof as precisely formulating and using the symmetry, whereas the Mizar proof repeats the argument.Source: §4 · p. 9
- Random inspection of a dozen striking shortenings found no suspicious proofs, but some ATP proofs may be hard to understand without refactoring and presentation.The inspected ATP proofs could be replayed in Mizar.Source: §4 · p. 9
- 23.2% of Mizar proof lines can be written automatically when automation is applied to named top-level theorems.The comparison uses 1,297,926 total source proof lines and 300,914 lines for the 28,892 named theorems proved automatically; the authors note that including proof-local lemmas would raise the average.Source: §4 · p. 9
5 Integration with MizAR
MizAR integrates fast premise selection and parallel ATP runs, while its updating and proof-local-lemma handling remain constrained in specific ways.
5 Integration with MizAR
- Optimized C++ premise selectors train on the whole MML in 1–3 seconds, supporting practical integration into MizAR.For each query, training also incorporates features and proof dependencies from the current article; selectors rank relevant theorems, and multiple selector–ATP pairs run in parallel.Source: §5 · pp. 9–10
- MizAR updates with the submitted article but does not use minimized ATP proofs of earlier theorems in that article for training.Anonymous uploads are not persistent, so projects cannot yet reuse cached computation; adding persistence could make proof computation and minimization less expensive.Source: §5 · p. 10
- The large-scale experiments and training data cover top-level theorems without proof-local constants, not proof-local lemmas containing them.Mizar commonly uses local constants, or eigenvariables, in Jaśkowski-style proofs.Source: §5 · p. 10
- Rare local constants can make selectors prefer relevant local lemmas, while their instantiated terms can distance those lemmas from general theorems needed to justify them.That feature-distance issue may prevent finding the relevant general theorems; the paper generalizes local constants to variables and adds features from the generalized lemmas, while leaving further feature work and evaluation for future work.Source: §5 · p. 10
6 Conclusion, Future Work and Thanks
The paper reports a 40.6% fully automatic success rate on top-level Mizar theorems, achieved through iterative improvement of premise selection and training data. It presents the system as a step toward more accessible formal mathematics and identifies strengthening methods and proof presentation as future work.
6 Conclusion, Future Work and Thanks
- 40.6% of top-level Mizar theorems are proved fully automatically.The result followed iterations of improved premise selection, obtaining better training data with those methods, and using the data to improve learning methods further.Source: §6 · p. 10
- The authors view strong AI/ATP systems as useful tools for making formal mathematics more accessible and as a possible path toward mainstream adoption of computer-assisted mathematics.This is stated as the authors’ belief about the potential consequence of gradually strengthening such systems.Source: §6 · p. 11
- Future work includes strengthening AI/ATP components and adding proof reconstruction and human-friendly proof presentation.The authors suggest that presentation methods may benefit from learning human-friendliness from repositories of human-oriented proofs such as the MML.Source: §6 · p. 11