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

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

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

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

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

Project

<a href="/en/project/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Artificial Intelligence and Reasoning</a><br>

Continuities

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

Publication year

2019

Confidentiality

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

Article name in the collection

Automated Deduction – CADE 27

ISBN

978-3-030-29435-9

ISSN

0302-9743

e-ISSN

1611-3349

Number of pages

19

Pages from-to

197-215

Publisher name

Springer, Cham

Place of publication

—

Event location

Natal

Event date

Aug 27, 2019

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000693450800012