Title: Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic,
Abstract: 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
$\lambda$-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.