TacticToe: Learning to Reason with HOL4 Tactics

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F17%3A00319002" target="_blank" >RIV/68407700:21730/17:00319002 - isvavai.cz</a>

Výsledek na webu

<a href="https://easychair.org/publications/paper/WsM" target="_blank" >https://easychair.org/publications/paper/WsM</a>

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

TacticToe: Learning to Reason with HOL4 Tactics

Popis výsledku v původním jazyce

Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such “hammer” techniques complement traditional proof assistant automation as implemented by tactics and decision procedures. In this paper we present a unified proof assistant automation approach which attempts to automate the selection of appropriate tactics and tactic-sequences combined with an optimized small-scale hammering approach. We implement the technique as a tactic-level automation for HOL4: TacticToe. It implements a modified A*-algorithm directly in HOL4 that explores different tactic-level proof paths, guiding their selection by learning from a large number of previous tactic-level proofs. Unlike the existing hammer methods, TacticToe avoids translation to FOL, working directly on the HOL level. By combining tactic prediction and premise selection, TacticToe is able to re-prove 39% of 7902 HOL4 theorems in 5 seconds whereas the best single HOL(y)Hammer strategy solves 32% in the same amount of time.

Název v anglickém jazyce

TacticToe: Learning to Reason with HOL4 Tactics

Popis výsledku anglicky

Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such “hammer” techniques complement traditional proof assistant automation as implemented by tactics and decision procedures. In this paper we present a unified proof assistant automation approach which attempts to automate the selection of appropriate tactics and tactic-sequences combined with an optimized small-scale hammering approach. We implement the technique as a tactic-level automation for HOL4: TacticToe. It implements a modified A*-algorithm directly in HOL4 that explores different tactic-level proof paths, guiding their selection by learning from a large number of previous tactic-level proofs. Unlike the existing hammer methods, TacticToe avoids translation to FOL, working directly on the HOL level. By combining tactic prediction and premise selection, TacticToe is able to re-prove 39% of 7902 HOL4 theorems in 5 seconds whereas the best single HOL(y)Hammer strategy solves 32% in the same amount of time.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

R - Projekt Ramcoveho programu EK

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning

ISBN

—

ISSN

2398-7340

e-ISSN

—

Počet stran výsledku

19

Strana od-do

125-143

Název nakladatele

EasyChair Publications

Místo vydání

Manchester

Místo konání akce

Maun

Datum konání akce

7. 5. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—