Learning to Reason with HOL4 tactics
Thibault Gauthier, Cezary Kaliszyk, Josef Urban

TL;DR
This paper introduces TacticToe, a novel HOL4 tactic automation method that combines machine learning with tactic-level proof search, achieving higher success rates than existing hammer techniques without translating to first-order logic.
Contribution
It presents TacticToe, a unified tactic-level automation for HOL4 that integrates machine learning-guided tactic selection with an optimized proof search algorithm, avoiding translation to FOL.
Findings
TacticToe re-proves 39% of theorems within 5 seconds.
It outperforms the HOL(y)Hammer strategy, which solves 32%.
The approach directly works on HOL level, bypassing translation to FOL.
Abstract
Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such "hammer" tech- niques complement traditional proof assistant automation as implemented by tactics and decision procedures. In this paper we present a unified proof assistant automation approach which attempts to automate the selection of appropriate tactics and tactic-sequences com- bined with an optimized small-scale hammering approach. We implement the technique as a tactic-level automation for HOL4: TacticToe. It implements a modified A*-algorithm directly in HOL4 that explores different tactic-level proof paths, guiding their selection by learning from a large number of previous tactic-level proofs. Unlike the existing hammer methods, TacticToe avoids translation to FOL, working directly on the HOL level. By combining tactic…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
