Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
This work addresses automated theorem proving for logic researchers, but it is incremental as it builds on existing neural translation techniques applied to a new domain.
The paper tackles the problem of proof synthesis in intuitionistic propositional logic by proposing a method that uses a neural machine translation model (seq2seq) to generate proof terms, with empirical results showing generated proofs are close to correct ones in terms of tree edit distance.
Inspired by the recent evolution of deep neural networks (DNNs) in machine learning, we explore their application to PL-related topics. This paper is the first step towards this goal; we propose a proof-synthesis method for the negation-free propositional logic in which we use a DNN to obtain a guide of proof search. The idea is to view the proof-synthesis problem as a translation from a proposition to its proof. We train seq2seq, which is a popular network in neural machine translation, so that it generates a proof encoded as a $λ$-term of a given proposition. We implement the whole framework and empirically observe that a generated proof term is close to a correct proof in terms of the tree edit distance of AST. This observation justifies using the output from a trained seq2seq model as a guide for proof search.