DeepMath - Deep Sequence Models for Premise Selection
arXiv:1606.04442
Abstract
We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving on a large scale.
References in corpus (1)
Cited by in corpus (35)
- Recent Advances in Deep Learning: An Overview
- QED at Large: A Survey of Engineering of Formally Verified Software
- Holophrasm: a neural Automated Theorem Prover for higher-order logic
- Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling
- Property Invariant Embedding for Automated Reasoning
- Hammering Mizar by Learning Clause Guidance
- Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
- Learning to Reason in Large Theories without Imitation
- NaturalProofs: Mathematical Theorem Proving in Natural Language
- Mathematical Reasoning in Latent Space
- Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning
- Learning Symbolic Rules for Reasoning in Quasi-Natural Language
- Learning to Prove Theorems by Learning to Generate Theorems
- Learning of Human-like Algebraic Reasoning Using Deep Feedforward Neural Networks
- Proof Artifact Co-training for Theorem Proving with Language Models
- Premise selection with neural networks and distributed representation of features
- Automated proof synthesis for propositional logic with deep neural networks
- From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group)
- Natural Language Premise Selection: Finding Supporting Statements for Mathematical Text
- A Study of Continuous Vector Representationsfor Theorem Proving
- Contrastive Reinforcement Learning of Symbolic Reasoning Domains
- An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic
- A machine learning based software pipeline to pick the variable ordering for algorithms with polynomial inputs
- On Learning to Prove
- ML + FV = ? A Survey on the Application of Machine Learning to Formal Verification
- Combining Axiom Injection and Knowledge Base Completion for Efficient Natural Language Inference
- Verifying Security Protocols using Dynamic Strategies
- SLDR-DL: A Framework for SLD-Resolution with Deep Learning
- The Uncanny Similarity of Recurrence and Depth
- Towards Concise, Machine-discovered Proofs of Gödel's Two Incompleteness Theorems
- Vampire With a Brain Is a Good ITP Hammer
- Trainable back-propagated functional transfer matrices
- Generating Symbolic Reasoning Problems with Transformer GANs
- Elementary Logic in Linear Space
- A Sequential Set Generation Method for Predicting Set-Valued Outputs