Learning-Assisted Automated Reasoning with Flyspeck
arXiv:1211.7012 · doi:10.1007/s10817-014-9303-3
Abstract
The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machine-learning premise selection methods trained on the proofs, producing an AI system capable of answering a wide range of mathematical queries automatically. The performance of this architecture is evaluated in a bootstrapping scenario emulating the development of Flyspeck from axioms to the last theorem, each time using only the previous theorems and proofs. It is shown that 39% of the 14185 theorems could be proved in a push-button mode (without any high-level advice and user interaction) in 30 seconds of real time on a fourteen-CPU workstation. The necessary work involves: (i) an implementation of sound translations of the HOL Light logic to ATP formalisms: untyped first-order, polymorphic typed first-order, and typed higher-order, (ii) export of the dependency information from HOL Light and ATP proofs for the machine learners, and (iii) choice of suitable representations and methods for learning from previous proofs, and their integration as advisors with HOL Light. This work is described and discussed here, and an initial analysis of the body of proofs that were found fully automatically is provided.
References in corpus (3)
Cited by in corpus (39)
- DeepMath - Deep Sequence Models for Premise Selection
- MizAR 40 for Mizar 40
- The Ramanujan Machine: Automatically Generated Conjectures on Fundamental Constants
- QED at Large: A Survey of Engineering of Formally Verified Software
- TacticToe: Learning to Prove with Tactics
- Premise Selection and External Provers for HOL4
- Property Invariant Embedding for Automated Reasoning
- Hammering Mizar by Learning Clause Guidance
- Proof Repair across Type Equivalences
- HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
- Tactic Learning and Proving for the Coq Proof Assistant
- The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
- Mathematical Reasoning via Self-supervised Skip-tree Training
- Learning to Reason with HOL4 tactics
- Developments in Formal Proofs
- Predicting SMT Solver Performance for Software Verification
- Learning Guided Automated Reasoning: A Brief Survey
- Formal Mathematics on Display: A Wiki for Flyspeck
- GRUNGE: A Grand Unified ATP Challenge
- Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
- TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
- Goal Translation for a Hammer for Coq (Extended Abstract)
- ProofWatch: Watchlist Guidance for Large Theories in E
- HOL(y)Hammer: Online ATP Service for HOL Light
- From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group)
- Teaching Temporal Logics to Neural Networks
- An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic
- Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
- Neural Circuit Synthesis from Specification Patterns
- Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving
- Proceedings Second International Workshop on Formal Integrated Development Environment
- JEFL: Joint Embedding of Formal Proof Libraries
- Generating Symbolic Reasoning Problems with Transformer GANs
- Lassie: HOL4 Tactics by Example
- Learning-assisted Theorem Proving with Millions of Lemmas
- Lemma Mining over HOL Light
- ENIGMA: Efficient Learning-based Inference Guiding Machine
- Computer-Assisted Proving of Combinatorial Conjectures Over Finite Domains: A Case Study of a Chess Conjecture
- Machine Learning Guidance and Proof Certification for Connection Tableaux