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 |
| DOI: | 10.1007/s10817-020-09580-x |
| 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: |
|
Full text from SpringerLink