Pith. sign in

REVIEW 1 cited by

TacticToe: Learning to Prove with Tactics

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1804.00596 v2 pith:JFDPJ6EM submitted 2018-04-02 cs.AI cs.LO

Thibault Gauthier , Cezary Kaliszyk , Josef Urban , Ramana Kumar , Michael Norrish This is my paper
classification cs.AIcs.LO
keywords tactictoeproverpercenthol4proofalgorithmauto-scheduleautomated
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original 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.

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Automating Formal Verification with Reinforcement Learning and Recursive Inference

    cs.LG 2026-05 unverdicted novelty 5.0 of 10

    RLVR training raises verified Dafny pass rates from 9.7% to 31.1% on a filtered benchmark while a Lean proof scaffold lifts success from 46.2% to 69.2% on a pilot set and solves 7 of 42 prior unsolved tasks.

Pith tools