Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning

Understand

The problem-solving in automated theorem proving (ATP) can be interpreted as a search problem where the prover constructs a proof tree step by step.

• In this paper, we propose a deep reinforcement learning algorithm for proof search in intuitionistic propositional logic.
• The most significant challenge in the application of deep learning to the ATP is the absence of large, public theorem database.
• We, however, overcame this issue by applying a novel data augmentation procedure at each iteration of the reinforcement learning.