Premise selection for mathematics by corpus analysis and kernel methods
From MaRDI portal
Publication:2352489
Abstract: 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.
Recommendations
- Overview and evaluation of premise selection techniques for large theory mathematics
- Mathematical Knowledge Management
- NLP-based detection of Mathematics Subject Classification
- NLP and large-scale information retrieval on mathematical texts
- A mathematical comparison between several single author corpora
- Mathematical aspects of concept analysis
- Mathematical text processing in EA-style: a sequent aspect
- A Computational Framework For Understanding Mathematical Discoursexy
- POS tagging and its applications for mathematics. Text analysis in mathematics
Cites work
- An introduction to support vector machines and other kernel-based learning methods.
- ATP and presentation service for Mizar formalizations
- Automated and human proofs in general mathematics: an initial comparison
- Automatic proof and disproof in Isabelle/HOL
- Co-regularized least-squares for label ranking
- Dependencies in formal mathematics: applications and extraction for Coq and Mizar
- Evaluation of automated theorem proving on the Mizar mathematical library
- scientific article; zbMATH DE number 5850143 (Why is no real title available?)
- scientific article; zbMATH DE number 1804115 (Why is no real title available?)
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle/HOL. A proof assistant for higher-order logic
- Large formal wikis: issues and solutions
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- MPTP 0.2: Design, implementation, and initial experiments
- MPTP-motivation, implementation, first experiments
- Obvious inferences
- Pattern recognition and machine learning.
- Pegasos: primal estimated sub-gradient solver for SVM
- Sine qua non for large theory reasoning
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Subsystems of second order arithmetic
- Theory of Reproducing Kernels
- Translating higher-order clauses to first-order clauses
Cited in
(48)- Hammer for Coq: automation for dependent type theory
- ATPboost: learning premise selection in binary setting with ATP feedback
- ATP and presentation service for Mizar formalizations
- HOL(y)Hammer: online ATP service for HOL Light
- Machine learning guidance for connection tableaux
- Guiding an automated theorem prover with neural rewriting
- Improving stateful premise selection with transformers
- The role of entropy in guiding a connection prover
- Eliminating models during model elimination
- Learning theorem proving components
- GRUNGE: a grand unified ATP challenge
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Semantics of Mizar as an Isabelle object logic
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Portfolio theorem proving and prover runtime prediction for geometry
- Extending E prover with similarity based clause selection strategies
- MizAR 40 for Mizar 40
- Overview and evaluation of premise selection techniques for large theory mathematics
- Random forests for premise selection
- Lemmatization for stronger reasoning in large theories
- Higher-order modal logics: automation and applications
- A learning-based fact selector for Isabelle/HOL
- Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
- System description: E.T. 0.1
- Learning-assisted theorem proving with millions of lemmas
- Theorem proving in large formal mathematics as an emerging AI field
- A study of continuous vector representations for theorem proving
- The 10th IJCAR automated theorem proving system competition -- CASC-J10
- Prolog Technology Reinforcement Learning Prover
- Logical analysis of emotions in text from natural language
- Hierarchical invention of theorem proving strategies
- The CADE-27 automated theorem proving system competition -- CASC-27
- mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
- Mining state-based models from proof corpora
- Premise selection in the Naproche system
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Learning Proof Transformations and Its Applications in Interactive Theorem Proving
- Machine-learned premise selection for Lean
- Graph sequence learning for premise selection
- Context-aware clause selection using symbol name meanings in theorem proving
- Constraint learning for non-confluent proof search
- Machine learning for quantifier selection in cvc5
- Stateful premise selection by recurrent neural networks
- An interactive SMT tactic in Coq using abductive reasoning
- Learning guided automated reasoning: a brief survey
- ATWGNNS: graph simplified representation and learning of logical formula for premise selection
- Types, Tableaus and Gödel’s God in Isabelle/HOL
- Vampire with a brain is a good ITP hammer
Describes a project that uses
Uses Software
This page was built for publication: Premise selection for mathematics by corpus analysis and kernel methods
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2352489)
