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

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.

References in corpus (14)

• Auto-Encoding Variational Bayes
• A formally verified compiler back-end
• Learning a SAT Solver from Single-Bit Supervision
• Learning-Assisted Automated Reasoning with Flyspeck
• MizAR 40 for Mizar 40
• GamePad: A Learning Environment for Theorem Proving
• TacticToe: Learning to Prove with Tactics
• Generative Language Modeling for Automated Theorem Proving
• Natural-Parameter Networks: A Class of Probabilistic Neural Networks
• Premise Selection and External Provers for HOL4
• Learning to Prove Theorems via Interacting with Proof Assistants
• Learning to Reason in Large Theories without Imitation
• Proof Artifact Co-training for Theorem Proving with Language Models
• Training a First-Order Theorem Prover from Synthetic Data

Cited by in corpus (3)

• Peano: Learning Formal Mathematical Reasoning
• QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
• BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving