ENIGMA: Efficient Learning-Based Inference Guiding Machine

Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F17%3A00318950" target="_blank" >RIV/68407700:21730/17:00318950 - isvavai.cz</a>
Výsledek na webu
<a href="https://doi.org/10.1007/978-3-319-62075-6_20" target="_blank" >https://doi.org/10.1007/978-3-319-62075-6_20</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-62075-6_20" target="_blank" >10.1007/978-3-319-62075-6_20</a>

Jazyk výsledku
angličtina
Název v původním jazyce
ENIGMA: Efficient Learning-Based Inference Guiding Machine
Popis výsledku v původním jazyce
ENIGMA is a learning-based method for guiding given clause selection in saturation-based theorem provers. Clauses from many previous proof searches are classified as positive and negative based on their participation in the proofs. An efficient classification model is trained on this data, classifying a clause as useful or un-useful for the proof search. This learned classification is used to guide next proof searches prioritizing useful clauses among other generated clauses. The approach is evaluated on the E prover and the CASC 2016 AIM benchmark, showing a large increase of E’s performance.
Název v anglickém jazyce
ENIGMA: Efficient Learning-Based Inference Guiding Machine
Popis výsledku anglicky
ENIGMA is a learning-based method for guiding given clause selection in saturation-based theorem provers. Clauses from many previous proof searches are classified as positive and negative based on their participation in the proofs. An efficient classification model is trained on this data, classifying a clause as useful or un-useful for the proof search. This learned classification is used to guide next proof searches prioritizing useful clauses among other generated clauses. The approach is evaluated on the E prover and the CASC 2016 AIM benchmark, showing a large increase of E’s performance.

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)

Rok uplatnění
2017
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ů

Podobné výsledky(10)