Pith. sign in

REVIEW

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 · ORCID
classification cs.AIcs.LO
keywords tactictoeproverpercenthol4proofalgorithmauto-scheduleautomated
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

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). Continue with ORCID to comment.

Pith tools