ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F19%3A00339853" target="_blank" >RIV/68407700:21730/19:00339853 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-29436-6_12" target="_blank" >https://doi.org/10.1007/978-3-030-29436-6_12</a>

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E

Popis výsledku v původním jazyce

We describe an efficient implementation of given clause selection in saturation-based automated theorem provers, extending the previous ENIGMA approach. Unlike in the first ENIGMA implementation where a fast linear classifier is trained and used together with manually engineered features, we have started to experiment with more sophisticated state-of-the-art machine learning methods such as gradient boosted trees and recursive neural networks. In particular, the latter approach poses challenges in terms of efficiency of clause evaluation, however, we show that deep integration of the neural evaluation with the ATP data-structures can largely amortize this cost and lead to competitive real-time results. Both methods are evaluated on a large dataset of theorem proving problems and compared with the previous approaches. The resulting methods improve on the manually designed clause guidance, providing the first practically convincing application of gradient-boosted and neural clause guidance in saturation-style automated theorem provers.

Název v anglickém jazyce

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E

Popis výsledku anglicky

We describe an efficient implementation of given clause selection in saturation-based automated theorem provers, extending the previous ENIGMA approach. Unlike in the first ENIGMA implementation where a fast linear classifier is trained and used together with manually engineered features, we have started to experiment with more sophisticated state-of-the-art machine learning methods such as gradient boosted trees and recursive neural networks. In particular, the latter approach poses challenges in terms of efficiency of clause evaluation, however, we show that deep integration of the neural evaluation with the ATP data-structures can largely amortize this cost and lead to competitive real-time results. Both methods are evaluated on a large dataset of theorem proving problems and compared with the previous approaches. The resulting methods improve on the manually designed clause guidance, providing the first practically convincing application of gradient-boosted and neural clause guidance in saturation-style automated theorem provers.

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/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Umělá inteligence a uvažování</a><br>

Návaznosti

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

Rok uplatnění

2019

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 27

ISBN

978-3-030-29435-9

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

19

Strana od-do

197-215

Název nakladatele

Springer, Cham

Místo vydání

—

Místo konání akce

Natal

Datum konání akce

27. 8. 2019

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

WRD - Celosvětová akce

Kód UT WoS článku

000693450800012