Automated proof synthesis for propositional logic with deep neural networks

TL;DR

This paper introduces a deep neural network-based approach for automated proof synthesis in propositional logic, demonstrating high accuracy and improvements over recent methods through empirical evaluation.

Contribution

It presents a novel DNN architecture for proof synthesis, combining statistical likelihood modeling with a proof search procedure, advancing neural methods in automated theorem proving.

Findings

High accuracy in proof synthesis for propositional logic

Significant improvement over recent neural proof methods

Effective use of a proposition-to-proof neural architecture

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.