TacticToe: Learning to Prove with Tactics
This work addresses the problem of automating theorem proving for formal verification and mathematics, offering a significant improvement over existing methods.
The paper tackles automated theorem proving by learning suitable mathematical techniques from human proofs and using Monte Carlo tree search to explore tactic-level proof paths, achieving a 66.4% success rate on HOL4's standard library compared to 34.5% for E prover.
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.