  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).

Artificial Intelligence;Machine Learning;Logic in Computer Science