Automated proof synthesis for propositional logic with deep neural networks

2018/05/30 by Taro Sekiyama, Sekiyama, Taro, Kohei Suenaga +1 · 1 citation
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Machine Learning (cs.LG) #Natural Language Processing Techniques #Programming Languages (cs.PL) #Semantic Web and Ontologies

paper · pdf · doi:10.48550/arxiv.1805.11799

openalex publication_date 2018/05/30 · openalex created_date 2018/06/13 · openalex updated_date 2026/07/28

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.

Citations

• A Stochastic Approximation Method
• Long Short-Term Memory
• ImageNet Large Scale Visual Recognition Challenge
• Neural Machine Translation by Jointly Learning to Align and Translate
• Deep Neural Networks for Acoustic Modeling in Speech Recognition: The Shared Views of Four Research Groups
• ImageNet classification with deep convolutional neural networks
• A theory of type polymorphism in programming
• On the Properties of Neural Machine Translation: Encoder-Decoder Approaches
• Language to Logical Form with Neural Attention
• DeepMath - Deep Sequence Models for Premise Selection
• Google's Neural Machine Translation System: Bridging the Gap between Human and Machine Translation
• HolStep: A Machine Learning Dataset for Higher-order Logic Theorem\n Proving
• A Syntactic Neural Model for General-Purpose Code Generation
• Learning a SAT Solver from Single-Bit Supervision
• Can Neural Networks Understand Logical Entailment?
• Convolutional Neural Networks over Tree Structures for Programming Language Processing

Cited by

• Verifying Security Protocols using Dynamic Strategies

Related

• Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
• Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning
• Learning to Prove Theorems by Learning to Generate Theorems
• Deep Network Guided Proof Search
• A Survey on Deep Learning for Theorem Proving