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

Understand

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.