Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

TacticToe: Learning to Prove with Tactics

Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish

TL;DR

The paper tackles the challenge of automating tactic-based proofs in interactive theorem proving by learning from human proofs to guide a Monte Carlo tree search over tactic sequences. It introduces TacticToe, which predicts tactics, premises, and goal lists using a k-NN-based predictor on rich HOL4 features, and couples this with an MCTS framework, orthogonalization, and tactic abstraction to efficiently explore proof paths. Key innovations include abstracting tactic arguments, asynchronous ATP integration (Metis and E prover), and a robust proof-recording pipeline enabling continual learning from discovered proofs. Empirically, TacticToe achieves 66.4% success on 7164 HOL4 theorems within 60 seconds on a single CPU, outperforming E prover alone and reaching 69.0% when combined, with strong gains on inductive and specialized theory domains.

Abstract

We implement a automated tactical prover TacticToe on top of the HOL4 interactive theorem prover. TacticToe learns from human proofs which mathematical technique is suitable in each proof situation. This knowledge is then used in a Monte Carlo tree search algorithm to explore promising tactic-level proof paths. On a single CPU, with a time limit of 60 seconds, TacticToe proves 66.4 percent of the 7164 theorems in HOL4's standard library, whereas E prover with auto-schedule solves 34.5 percent. The success rate rises to 69.0 percent by combining the results of TacticToe and E prover.

TacticToe: Learning to Prove with Tactics

TL;DR

The paper tackles the challenge of automating tactic-based proofs in interactive theorem proving by learning from human proofs to guide a Monte Carlo tree search over tactic sequences. It introduces TacticToe, which predicts tactics, premises, and goal lists using a k-NN-based predictor on rich HOL4 features, and couples this with an MCTS framework, orthogonalization, and tactic abstraction to efficiently explore proof paths. Key innovations include abstracting tactic arguments, asynchronous ATP integration (Metis and E prover), and a robust proof-recording pipeline enabling continual learning from discovered proofs. Empirically, TacticToe achieves 66.4% success on 7164 HOL4 theorems within 60 seconds on a single CPU, outperforming E prover alone and reaching 69.0% when combined, with strong gains on inductive and specialized theory domains.

Abstract

We implement a automated tactical prover TacticToe on top of the HOL4 interactive theorem prover. TacticToe learns from human proofs which mathematical technique is suitable in each proof situation. This knowledge is then used in a Monte Carlo tree search algorithm to explore promising tactic-level proof paths. On a single CPU, with a time limit of 60 seconds, TacticToe proves 66.4 percent of the 7164 theorems in HOL4's standard library, whereas E prover with auto-schedule solves 34.5 percent. The success rate rises to 69.0 percent by combining the results of TacticToe and E prover.

Paper Structure

This paper contains 35 sections, 24 equations, 2 figures.

Table of Contents

  1. Introduction
  2. The problem
  3. Goals and theorems.
  4. Theories and script files.
  5. Tactics in HOL4.
  6. Contributions
  7. Plan
  8. Search Tree
  9. Prediction
  10. Tactics
  11. Theorems as Arguments of Tactics
  12. Lists of Goals as Output of Tactics
  13. Feature Extraction and Similarity Measures
  14. Proof Search
  15. Proof exploration
  16. ...and 20 more sections

Figures (2)

  • Figure 1: Relation between modules of the learning and proving toolchains. Functions are represented by rectangles and objects by ellipses.
  • Figure 2: A node of a search tree $a_0$, the list of goals $g_0 \ldots g_n$ it contains and the nodes $a_1 \ldots a_m$ derived from the application of the tactics $t_1 \ldots t_m$ to $g_i$.

Theorems & Definitions (13)

  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • remark thmcounterremark
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • ...and 3 more