Vampire with a Brain Is a Good ITP Hammer

Kód výsledku v IS VaVaI

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

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-86205-3_11" target="_blank" >https://doi.org/10.1007/978-3-030-86205-3_11</a>

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

Vampire with a Brain Is a Good ITP Hammer

Popis výsledku v původním jazyce

Vampire has been for a long time the strongest first-order automatic theorem prover, widely used for hammer-style proof automation in ITPs such as Mizar, Isabelle, HOL, and Coq. In this work, we considerably improve the performance of Vampire in hammering over the full Mizar library by enhancing its saturation procedure with efficient neural guidance. In particular, we employ a recently proposed recursive neural network classifying the generated clauses based only on their derivation history. Compared to previous neural methods based on considering the logical content of the clauses, our architecture makes evaluating a single clause much less time consuming. The resulting system shows good learning capability and improves on the state-of-the-art performance on the Mizar library, while proving many theorems that the related ENIGMA system could not prove in a similar hammering evaluation.

Název v anglickém jazyce

Vampire with a Brain Is a Good ITP Hammer

Popis výsledku anglicky

Vampire has been for a long time the strongest first-order automatic theorem prover, widely used for hammer-style proof automation in ITPs such as Mizar, Isabelle, HOL, and Coq. In this work, we considerably improve the performance of Vampire in hammering over the full Mizar library by enhancing its saturation procedure with efficient neural guidance. In particular, we employ a recently proposed recursive neural network classifying the generated clauses based only on their derivation history. Compared to previous neural methods based on considering the logical content of the clauses, our architecture makes evaluating a single clause much less time consuming. The resulting system shows good learning capability and improves on the state-of-the-art performance on the Mizar library, while proving many theorems that the related ENIGMA system could not prove in a similar hammering 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

Frontiers of Combining Systems

ISBN

978-3-030-86204-6

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

18

Strana od-do

192-209

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Birmingham

Datum konání akce

8. 9. 2021

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

WRD - Celosvětová akce

Kód UT WoS článku

000711401800011