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

DOI10.1007/978-3-030-02768-1_17MaRDI QIDQ6166153zbMATH OpenOpenAlexFDO

Authors Taro Sekiyama, Kohei Suenaga

Publication date 2 August 2023

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

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

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)

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.

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

Cited in

(8)

• Guiding an automated theorem prover with neural rewriting
• Deep network guided proof search
• Transformer-based deep neural language modeling for construct-specific automatic item generation
• Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT
• Towards the automatic mathematician
• Invariant neural architecture for learning term synthesis in instantiation proving
• A formal proof of the expressiveness of deep learning
• A formal proof of the expressiveness of deep learning

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)