TacticToe: Learning to Prove with Tactics

Autor:	Josef Urban, Cezary Kaliszyk, Thibault Gauthier, Michael Norrish, Ramana Kumar
Rok vydání:	2020
Předmět:	FOS: Computer and information sciences Computer Science - Logic in Computer Science Theoretical computer science Computer Science - Artificial Intelligence Computer science Monte Carlo tree search Proof assistant 020207 software engineering 0102 computer and information sciences 02 engineering and technology Gas meter prover Time limit Mathematical proof 01 natural sciences Logic in Computer Science (cs.LO) Artificial Intelligence (cs.AI) TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics 010201 computation theory & mathematics Artificial Intelligence TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering Software
Zdroj:	Journal of Automated Reasoning
ISSN:	1573-0670 0168-7433
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4e9fcce9e1b1554e6a03463b44d2cfd4 https://doi.org/10.1007/s10817-020-09580-x Zobrazit plný text záznamu Full text from SpringerLink