Elamur Research⌕
☰
home / papers / 2011 / Premise Selection for Mathematics by Corpus Analysis and Kernel Methods

Premise Selection for Mathematics by Corpus Analysis and Kernel Methods

Paper · 2011 · Jesse Alama, Tom Heskes, Daniel Kühlwein et al.

Summary

Automated theorem provers (ATPs) struggle when a conjecture must be proved against a library of thousands of facts. Picking a small, relevant set of premises is therefore critical. The authors tackle this for the Mizar Mathematical Library (MML) in two ways.

First, they use a new dependency analysis. It splits Mizar articles into single-item micro-articles and greedily shrinks each one's environment to a truly minimal set of required items. This exposes facts Mizar normally uses silently, such as subtyping relations. The exact dependencies yield clean problems for ATP re-verification and precise training data for learning.

Second, they propose a kernel-based multi-output ranking algorithm (MOR). It orders library facts by how useful they are likely to be for a new conjecture.

For evaluation, they assemble MPTP2078, a benchmark that enlarges the older MPTP Challenge. Together, the exact data and MOR prove about half again as many problems as Vampire with SInE. The work shows that learning from existing formal proofs can substantially strengthen reasoning over large mathematical theories.

Key points

  • MPTP2078 benchmark: 2078 related problems taken from 33 MML articles, extending the MPTP Challenge. CASC LTB data was judged too small for machine learning.
  • Minimal dependencies: computed by refactoring articles into micro-articles and applying brute-force/greedy environment minimization. Only semantic dependencies (those that MPTP translates into first-order formulas) are used for ATP.
  • Off-the-shelf learning: naive Bayes (SNoW) trained on the exact dependencies gives roughly 44% improvement over SInE.
  • MOR results: MOR raises the gain to about 50% over Vampire/SInE, with 824 problems solved within 10 seconds.
  • Remaining gap: human-selected premises (Vampire-bushy) show that at least 1105 problems are provable, so premise selection still has clear room to improve.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Radboud University NijmegenNijmegen · Netherlands26 works · 2,125 citations🎓University of LisbonLisbon · Portugal28 works · 3,860 citations🎓Universidade Nova de LisboaLisbon · Portugal7 works · 2,172 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze and Josef Urban. 2011. Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. arXiv:1108.3446.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.1007/s10817-013-9286-5 · arXiv 1108.3446

@misc{alama2011premise,
  title = {{Premise Selection for Mathematics by Corpus Analysis and Kernel Methods}},
  author = {Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze and Josef Urban},
  year = {2011},
  doi = {10.1007/s10817-013-9286-5},
  eprint = {1108.3446},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.1007/s10817-013-9286-5}
}

References

37 references, 1 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Alama, J.: Formal Proofs and Refutations. Ph.D. thesis, Stanford University (2009) find
  2. Alama, J., Brink, K., Mamane, L., Urban, J.: Large formal wikis: Issues and solutions. In: Davenport, J., Farmer, W., Urban, J., Rabe, F. (eds.) Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 6824, pp. 133–148. Springer Berlin / Heidelberg (2011) find
  3. Alama, J., Kühlwein, D., Urban, J.: Automated and human proofs in general mathematics: An initial comparison. In: Bjørner, N., Voronkov, A. (eds.) LPAR. Lecture Notes in Computer Science, vol. 7180, pp. 37–45. Springer (2012) find
  4. Alama, J., Mamane, L., Urban, J.: Dependencies in formal mathematics: Applications and extraction for Coq and Mizar (2011), arxiv.org pre-print abs/1109.3687 — [arXiv:1109.3687](https://arxiv.org/abs/1109.3687) find
  5. Aronszajn, N.: Theory of reproducing kernels. Transactions of the American Mathematical Society 68 (1950) find
  6. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, Springer Verlag (2004) find
  7. Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCos. Lecture Notes in Computer Science, vol. 6989, pp. 12–27. Springer (2011) find
  8. Brin, S., Page, L.: The anatomy of a large-scale hypertextual web search engine. Computer Networks 30(1-7), 107–117 (1998)
  9. Carlson, A., Cumby, C., Rizzolo, N., Rosen, J., Roth, D.: SNoW user manual (1999), http://l2r.cs.uiuc.edu/~cogcomp/software/snow-userguide.pdf ↗
  10. Davis, M.: Obvious logical inferences. In: Hayes, P.J. (ed.) IJCAI. pp. 530–531. William Kaufmann (1981) find
  11. Grabowski, A., Korni lowicz, A., Naumowicz, A.: Mizar in a nutshell. Journal of Formalized Reasoning 3(2), 153–245 (2010) find
  12. Harrison, J.: Optimizing proof search in model elimination. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE. Lecture Notes in Computer Science, vol. 1104, pp. 313–327. Springer (1996) find
  13. Harrison, J., Slind, K., Arthan, R.: HOL. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. Lecture Notes in Computer Science, vol. 3600, pp. 11–19. Springer (2006) find
  14. Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) Automated Deduction – CADE-23, Lecture Notes in Computer Science, vol. 6803, pp. 299–314. Springer Berlin / Heidelberg (2011) find
  15. Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Mathematics and Its Applications 4, 3–24 (2005) find
  16. Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning 40(1), 35–60 (2008) find
  17. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283. Springer (2002) find
  18. Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs. Lecture Notes in Computer Science, vol. 4732, pp. 232–245. Springer (2007) find
  19. Pease, A., Sutcliffe, G.: First order reasoning on a large ontology. In: Sutcliffe, G., Urban, J., Schulz, S. (eds.) ESARLT. CEUR Workshop Proceedings, vol. 257. CEUR-WS.org (2007) find
  20. Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2-3), 91–110 (2002) find
  21. Richard, M.D., Lippmann, R.P.: Neural Network Classifiers Estimate Bayesian a posteriori Probabilities. Neural Computation 3(4), 461–483 (2010) find
  22. Rifkin, R., Yeo, G., Poggio, T., Rifkin, R., Yeo, G., Poggio, T.: Regularized Least-Squares Classification. In: Suykens, J., Horvath, G., Basu, S., Micchelli, C., Vandewalle, J. (eds.) Advances in Learning Theory: Methods, Model and Applications NATO Science Series III: Computer and Systems Sciences… find
  23. Rudnicki, P.: Obvious inferences. J. Autom. Reasoning 3(4), 383–393 (1987) find
  24. Schoelkopf, B., Herbrich, R., Williamson, R., Smola, A.J.: A Generalized Representer Theorem. In: Helmbold, D., Williamson, R. (eds.) Proceedings of the 14th Annual Conference on Computational Learning Theory. pp. 416–426. Berlin, Germany (2001) find
  25. Scholkopf, B., Smola, A.J.: Learning with Kernels: Support Vector Machines, Regularization, Optimization, and Beyond. MIT Press, Cambridge, MA, USA (2001) find
  26. Shalev-Shwartz, S., Singer, Y., Srebro, N., Cotter, A.: Pegasos: primal estimated subgradient solver for SVM. Math. Program. 127(1), 3–30 (2011) find
  27. Shawe-Taylor, J., Cristianini, N.: Kernel Methods for Pattern Analysis. Cambridge University Press, New York, NY, USA (2004) find
  28. Simpson, S.G.: Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic, Springer, 2 edn. (2009) find
  29. Solovay, R.: AC and strongly inaccessible cardinals. Available on the Foundations of Mathematics archives at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783. html (March 29 2008) ↗
  30. Tarski, A.: On well-ordered subsets of any set. Fundamenta Mathematicae 32, 176–183 (1939) find
  31. Tsivtsivadze, E., Pahikkala, T., Boberg, J., Salakoski, T., Heskes, T.: Co-regularized least-squares for label ranking. In: Hüllermeier, E., Fürnkranz, J. (eds.) Chapter in Preference Learning Book). pp. 107–123 (2010) find
  32. Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning 37(1-2), 21–43 (2006) find
  33. Urban, J., Hoder, K., Voronkov, A.: Evaluation of automated theorem proving on the Mizar mathematical library. In: Fukuda, K., van der Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS. Lecture Notes in Computer Science, vol. 6327, pp. 155–166. Springer (2010) find
  34. Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. CoRR abs/1109.0616 (2011) — [arXiv:1109.0616](https://arxiv.org/abs/1109.0616) find
  35. Urban, J., Sutcliffe, G.: Automated reasoning and presentation support for formalizing mathematics in Mizar. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC/MKM/Calculemus. Lecture Notes in Computer Science, vol. 6167, pp. 132–146. Springer (… find
  36. Urban, J., Sutcliffe, G., Pudlák, P., Vyskocil, J.: MaLARea SG1–machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR. Lecture Notes in Computer Science, vol. 5195, pp. 441–456. Springer (2008) find
  37. Urban, J., Vyskocil, J., Stepánek, P.: MaLeCoP: Machine learning connection prover. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX. Lecture Notes in Computer Science, vol. 6793, pp. 263–277. Springer (2011) find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/alama-2011-premise-selection-mathematics-corpus-analysis/