Improving ENIGMA-style Clause Selection while Learning From History

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F21%3A00353738" target="_blank" >RIV/68407700:21730/21:00353738 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-79876-5_31" target="_blank" >https://doi.org/10.1007/978-3-030-79876-5_31</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-79876-5_31" target="_blank" >10.1007/978-3-030-79876-5_31</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Improving ENIGMA-style Clause Selection while Learning From History

Popis výsledku v původním jazyce

We re-examine the topic of machine-learned clause selection guidance in saturation-based theorem provers. The central idea, recently popularized by the ENIGMA system, is to learn a classifier for recogniz ing clauses that appeared in previously discovered proofs. In subsequent runs, clauses classified positively are prioritized for selection. We pro pose several improvements to this approach and experimentally confirm their viability. For the demonstration, we use a recursive neural network to classify clauses based on their derivation history and the presence or absence of automatically supplied theory axioms therein. The auto matic theorem prover Vampire guided by the network achieves a 41 % improvement on a relevant subset of SMT-LIB in a real time evaluation.

Název v anglickém jazyce

Improving ENIGMA-style Clause Selection while Learning From History

Popis výsledku anglicky

We re-examine the topic of machine-learned clause selection guidance in saturation-based theorem provers. The central idea, recently popularized by the ENIGMA system, is to learn a classifier for recogniz ing clauses that appeared in previously discovered proofs. In subsequent runs, clauses classified positively are prioritized for selection. We pro pose several improvements to this approach and experimentally confirm their viability. For the demonstration, we use a recursive neural network to classify clauses based on their derivation history and the presence or absence of automatically supplied theory axioms therein. The auto matic theorem prover Vampire guided by the network achieves a 41 % improvement on a relevant subset of SMT-LIB in a real time evaluation.

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

<a href="/cs/project/GJ20-06390Y" target="_blank" >GJ20-06390Y: Zlepšování automatických dokazovačů vět pomocí strojového učení</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2021

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

Automated Deduction – CADE 28

ISBN

978-3-030-79875-8

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

19

Strana od-do

543-561

Název nakladatele

Springer, Cham

Místo vydání

—

Místo konání akce

Pittsburgh

Datum konání akce

12. 7. 2021

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

WRD - Celosvětová akce

Kód UT WoS článku

000693448800031