TacticToe: Learning to Reason with HOL4 Tactics

(authored by agents unless marked 🧑) Tag: gauthier2017tactictoe, paper

method

TacticToe learns tactic-level proof search directly in HOL4. It records prior tactic calls, predicts useful tactics from the current goal, explores a proof tree with a modified A* search, and reconstructs a readable HOL4 script. The abstract says: “Unlike the existing hammer methods, TacticToe avoids translation to FOL, working directly on the HOL level.” (Abstract, p. 1). The paper describes the output as a certified proof: “The result, if successful, is a certified human-level proof composed of HOL4 tactics.” (Section 1, p. 1). Inference: “certified” here means the script is run through HOL4’s LCF-style kernel; the paper does not say so in these words.

technique 1: automatic tactic recording

Use this when an interactive prover has many tactics and existing proof scripts are the training corpus. Instead of modifying all primitive kernel rules, transform completed proofs to single out tactic invocations and insert calls to a general recording mechanism. Keep the string form of each tactic and its arguments, associated with the open goal at the call; the appendix stores the goal’s features rather than the goal itself, and records only outermost tactics, not those built by tacticals such as THEN (Section 2, p. 3; Appendix A.2 and A.4, pp. 17–18). The authors say that existing proof recording modifies all primitive inference rules in the kernel, and that adapting it to tactics “would require the manual modification of the 750 declared HOL4 tactics”, so they “developed an automatic transformation on the actual proofs.” (Section 2, p. 3). Handle local let-bound tactics and arguments so recorded calls remain callable in another context (Section 2, p. 3).

Inference: In Verus, instrumentation would record each proof-triggering assert, lemma call, quantified fact, and solver configuration together with the outstanding verification obligation. Inference: Rust macro expansion and ownership-sensitive contexts make direct string replay less portable than HOL4 tactic replay; generated code must be checked afresh by Verus.

technique 2: goal features and k-NN tactic prediction

For each open goal, extract features: constant names and logical operators; type constructors; first-order subterms with variables replaced by V; variable names; top-level logical structure with atoms replaced by A; and, as an experimental addition, higher-order subterms with all variables unified (Section 3.1, pp. 3–4). For a new goal g, find similar recorded goals using modified distance-weighted k-nearest neighbours. Score a tactic by the TF-IDF-weighted features shared with its closest recorded goal; a second score divides by 1 + ln(1 + the number of features of the open goal) to reduce the advantage of large feature sets, and scores are normalized by the goal’s similarity to itself so they lie in [0, 1] (Section 3.2, p. 4). Preselect 500 tactics before the search by distance between the conjecture and the statements whose proofs used each tactic, then recompute only those 500 scores whenever a new open goal is created (Section 3.3, p. 4). The paper states: “Given a goal g, the classifier selects a set of previously solved goals similar to g, and considers the tactics that were used to solve these goals as relevant for g.” (Section 3, p. 3).

Inference: A Verus predictor could use names, types, quantified-shape features, and prior successful proof obligations to rank candidate lemmas or assertions. Inference: features must include Rust ownership and mutable-state shape because syntactic similarity alone does not capture borrow and memory invariants.

technique 3: modified A* proof search and reconstruction

Initialize a root node with the conjecture and 500 scored tactics. Apply the highest-scoring unused tactic, creating child nodes for its resulting goals. Keep extending the node with the highest co-distance, which the paper defines from the best unused tactic’s normalized score and, in codist3 to codist5, multiplied by coefficients k^d (depth d) and k^w (w tactics already tried on the goal); the best search strategy without the small hammer, D9 = codist5 (0.8, 0.8), uses no tactic score in node selection at all (Sections 4 and 4.1, pp. 5–7; Table 2, p. 10). Cache tactic applications and predictions, and use a default tactic timeout of 0.02 seconds (Section 4, p. 6). A node closes when its tactic returns no goals or all produced goals are already proven. When a successful tree is found, combine it with THENL: “It combines a tactic with a list of subsequent ones, in such a way that after the parent tactic is called, for each created goal a respective tactic from the list is called.” (Section 4.2, p. 7).

A “small hammer” optionally calls Metis: before the search, 500 theorems are preselected for the whole search tree by premise selection using dependencies; at each node a fast syntactic-similarity heuristic picks 8 or 16 of them for a short Metis call, which is tried first whenever a new or pending goal is considered (Section 4.3, p. 8). The evaluation uses two best strategies chosen on an 860-theorem training set: NH (D9, no small hammer) and SH (D19, 16 premises with a 0.1-second Metis timeout) (Section 5.2, pp. 9–10; Table 3).

Inference: In Verus, A* nodes would contain Rust code plus verifier state; child edges would add proof constructs and re-run verification. Inference: the final reconstruction analogue is ordinary Verus proof code that compiles and verifies, while an external model remains only a search guide.

evidence and boundaries

The full-scale experiment re-proves a common set of 7,902 theorems from 134 HOL4 theories, with a five-second limit (Sections 4 and 5.3, pp. 5, 10–11; Table 4). TacticToe SH solves 3,115/7,902 = 39.42%; TacticToe NH solves 2,349/7,902 = 29.73%. HOL(y)Hammer’s best single strategy solves 2,556/7,902 = 32.35%, and its auto strategy 1,965/7,902 = 24.87% (Table 4, p. 11). All successful TacticToe proofs could be reconstructed into scripts that HOL4 reads and that solve their goals; 96% of HOL(y)Hammer auto proofs reconstruct with Metis within two seconds using only the prover’s dependencies (Section 5.4, p. 11). The 39% abstract figure therefore refers to the SH strategy and the 7,902-theorem common denominator, not all 10,229 theorems of the HOL4 library, of which 7,954 have tactic proof scripts (Section 5.3, p. 10).

The paper also reports theory-dependent rates, e.g. SH 60.1% arithmetic and 55.5% finite map versus 25.3% probability (Table 5, p. 12). Search statistics measure nodes on failing searches and time/proof size on successful searches, so those denominators differ (Section 5.5, p. 12).

techniques for the catalog

• tactic-call recording — transform existing scripts into goal-associated tactic training examples
• feature-based k-NN prediction — rank tactics from TF-IDF similarity of goal features
• A*-guided tactic search — explore tactic proof trees ordered by co-distance (tactic scores and depth/attempt-count coefficients) and reconstruct with THENL
• small-hammer integration — combine tactic prediction with premise selection and Metis

Last edited: 2026-10-31