TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning

TL;DR

TacticZero introduces a deep reinforcement learning framework for interactive theorem proving that learns proof strategies and predicts tactics, outperforming existing automated provers in HOL4 by efficiently exploring derivation paths.

Contribution

It presents a novel end-to-end deep RL approach for ITP, incorporating a backtracking mechanism and demonstrating superior performance over existing tools.

Findings

Outperforms existing HOL4 automated theorem provers on unseen problems

Introduces a backtracking mechanism for efficient proof search

Shows effectiveness of learned proof strategies through ablation studies

Abstract

We propose a novel approach to interactive theorem-proving (ITP) using deep reinforcement learning. The proposed framework is able to learn proof search strategies as well as tactic and arguments prediction in an end-to-end manner. We formulate the process of ITP as a Markov decision process (MDP) in which each state represents a set of potential derivation paths. This structure allows us to introduce a novel backtracking mechanism which enables the agent to efficiently discard (predicted) dead-end derivations and restart from promising alternatives. We implement the framework in the HOL4 theorem prover. Experimental results show that the framework outperforms existing automated theorem provers (i.e., hammers) available in HOL4 when evaluated on unseen problems. We further elaborate the role of key components of the framework using ablation studies.