Automated proof synthesis for propositional logic with deep neural networks

Understand

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.