Fast and Slow Enigmas and Parental Guidance

Result code in IS VaVaI

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

Result on the web

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

DOI - Digital Object Identifier

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

Result language

angličtina

Original language name

Fast and Slow Enigmas and Parental Guidance

Original language description

We describe several additions to the ENIGMA system that guides clause selection in the E automated theorem prover. First, we significantly speed up its neural guidance by adding server-based GPU evaluation. The second addition is motivated by fast weight-based rejection filters that are currently used in systems like E and Prover9. Such systems can be made more intelligent by instead training fast versions of ENIGMA that implement more intelligent pre-filtering. This results in combinations of trainable fast and slow thinking that improves over both the fast-only and slow-only methods. The third addition is based on “judging the children by their parents”, i.e., possibly rejecting an inference before it produces a clause. This is motivated by standard evolutionary mechanisms, where there is always a cost to producing all possible offsprings in the current population. This saves time by not evaluating all clauses by more expensive methods and provides a complementary view of the generated clauses. The methods are evaluated on a large benchmark coming from the Mizar Mathematical Library, showing good improvements over the state of the art.

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

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

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

Publication year

2021

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

Frontiers of Combining Systems

ISBN

978-3-030-86204-6

ISSN

0302-9743

e-ISSN

1611-3349

Number of pages

19

Pages from-to

173-191

Publisher name

Springer

Place of publication

Cham

Event location

Birmingham

Event date

Sep 8, 2021

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000711401800010