Automated proof synthesis for propositional logic with deep neural networks
arXiv:1805.11799
Abstract
This work explores the application of deep learning, a machine learning technique that uses deep neural networks (DNN) in its core, to an automated theorem proving (ATP) problem. To this end, we construct a statistical model which quantifies the likelihood that a proof is indeed a correct one of a given proposition. Based on this model, we give a proof-synthesis procedure that searches for a proof in the order of the likelihood. This procedure uses an estimator of the likelihood of an inference rule being applied at each step of a proof. As an implementation of the estimator, we propose a proposition-to-proof architecture, which is a DNN tailored to the automated proof synthesis problem. To empirically demonstrate its usefulness, we apply our model to synthesize proofs of propositional logic. We train the proposition-to-proof model using a training dataset of proposition-proof pairs. The evaluation against a benchmark set shows the very high accuracy and an improvement to the recent work of neural proof synthesis.
arXiv comment25 pages
References in corpus (13)
- Neural Machine Translation by Jointly Learning to Align and Translate
- Sequence to Sequence Learning with Neural Networks
- Google's Neural Machine Translation System: Bridging the Gap between Human and Machine Translation
- On the Properties of Neural Machine Translation: Encoder-Decoder Approaches
- Convolutional Neural Networks over Tree Structures for Programming Language Processing
- Learning a SAT Solver from Single-Bit Supervision
- Language to Logical Form with Neural Attention
- DeepMath - Deep Sequence Models for Premise Selection
- A Syntactic Neural Model for General-Purpose Code Generation
- HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
- Graph Neural Networks and Boolean Satisfiability
- Can Neural Networks Understand Logical Entailment?
- Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic