Automated proof synthesis for the minimal propositional logic with deep neural networks

DOI10.1007/978-3-030-02768-1_17zbMATH Open1519.68315arXiv1805.11799OpenAlexW2896461135MaRDI QIDQ6166153FDOQ6166153

Authors: Taro Sekiyama, Kohei Suenaga 

Publication date: 2 August 2023

Published in: Programming Languages and Systems (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1805.11799

Recommendations

• Deep network guided proof search
• Guiding an automated theorem prover with neural rewriting
• Towards the automatic mathematician
• A neurally-guided, parallel theorem prover
• Tree neural networks in HOL4

zbMATH Keywords

deep learningneural networksautomated theorem proving

Mathematics Subject Classification ID

Artificial neural networks and deep learning (68T07) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited In (2)

• Guiding an automated theorem prover with neural rewriting
• Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT

This page was built for publication: Automated proof synthesis for the minimal propositional logic with deep neural networks

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166153)