ProofWatch Meets ENIGMA: First Experiments

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F18%3A00329388" target="_blank" >RIV/68407700:21230/18:00329388 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/68407700:21730/18:00329388

Výsledek na webu

<a href="https://easychair.org/publications/paper/28xp" target="_blank" >https://easychair.org/publications/paper/28xp</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.29007/z7qx" target="_blank" >10.29007/z7qx</a>

Jazyk výsledku

angličtina

Název v původním jazyce

ProofWatch Meets ENIGMA: First Experiments

Popis výsledku v původním jazyce

Watchlist (also hint list) is a technique that allows lemmas from related proofs to guide a saturation-style proof search for a new conjecture. ProofWatch is a recent watchlist-style method that loads many previous proofs inside the ATP, maintains their completion ratios during the proof search and focuses the search by following the most completed proofs. In this work, we start to use the dynamically changing vector of proof completion ratios as additional information about the saturation-style proof state for statistical machine learning methods that evaluate the generated clauses. In particular, we add the proof completion vectors to ENIGMA (e_cient learning-based inference guiding machine) and evaluate the new method on the MPTP Challenge benchmark, showing moderate improvement in E's performance over ProofWatch and ENIGMA.

Název v anglickém jazyce

ProofWatch Meets ENIGMA: First Experiments

Popis výsledku anglicky

Watchlist (also hint list) is a technique that allows lemmas from related proofs to guide a saturation-style proof search for a new conjecture. ProofWatch is a recent watchlist-style method that loads many previous proofs inside the ATP, maintains their completion ratios during the proof search and focuses the search by following the most completed proofs. In this work, we start to use the dynamically changing vector of proof completion ratios as additional information about the saturation-style proof state for statistical machine learning methods that evaluate the generated clauses. In particular, we add the proof completion vectors to ENIGMA (e_cient learning-based inference guiding machine) and evaluate the new method on the MPTP Challenge benchmark, showing moderate improvement in E's performance over ProofWatch and ENIGMA.

Druh

J_ost - Ostatní články v recenzovaných periodicích

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í

2018

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 periodika

Kalpa Publications in Computing

ISSN

2515-1762

e-ISSN

2515-1762

Svazek periodika

1

Číslo periodika v rámci svazku

9

Stát vydavatele periodika

GB - Spojené království Velké Británie a Severního Irska

Počet stran výsledku

8

Strana od-do

15-22

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—