Timezone: »

 
Poster
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
Minchao Wu · Michael Norrish · Christian Walder · Amir Dezfouli

Wed Dec 08 12:30 AM -- 02:00 AM (PST) @
in Poster Session 3 »

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 the derivation from promising alternatives. We implement the framework in the HOL theorem prover. Experimental results show that the framework using learned search strategies outperforms existing automated theorem provers (i.e., hammers) available in HOL when evaluated on unseen problems. We further elaborate the role of key components of the framework using ablation studies.

Keywords: Reinforcement Learning and Planning

Author Information

Minchao Wu (Australian National University)
Michael Norrish (CSIRO)
Christian Walder (DATA61)
Amir Dezfouli (Data61, CSIRO)

More from the Same Authors