A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving

TL;DR

This paper introduces TRAIL, a deep reinforcement learning system for first-order logic theorem proving that uses novel neural representations and attention-based policies, outperforming previous RL-based provers by 15%.

Contribution

It presents a new neural state representation and an attention-based inference policy for reinforcement learning in theorem proving, improving performance.

Findings

TRAIL outperforms previous RL-based theorem provers by 15%.

The system achieves significant improvements on two benchmark datasets.

Novel neural and attention mechanisms enable better proof search guidance.

Abstract

Automated theorem provers have traditionally relied on manually tuned heuristics to guide how they perform proof search. Deep reinforcement learning has been proposed as a way to obviate the need for such heuristics, however, its deployment in automated theorem proving remains a challenge. In this paper we introduce TRAIL, a system that applies deep reinforcement learning to saturation-based theorem proving. TRAIL leverages (a) a novel neural representation of the state of a theorem prover and (b) a novel characterization of the inference selection process in terms of an attention-based action policy. We show through systematic analysis that these mechanisms allow TRAIL to significantly outperform previous reinforcement-learning-based theorem provers on two benchmark datasets for first-order logic automated theorem proving (proving around 15% more theorems).