ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback

Kód výsledku v IS VaVaI

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

Nalezeny alternativní kódy

RIV/68407700:21730/18:00329539

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007/978-3-319-94205-6_37" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-319-94205-6_37</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-94205-6_37" target="_blank" >10.1007/978-3-319-94205-6_37</a>

Jazyk výsledku

angličtina

Název v původním jazyce

ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback

Popis výsledku v původním jazyce

ATPboost is a system for solving sets of large-theory problems by interleaving ATP runs with state-of-the-art machine learning of premise selection from the proofs. Unlike many approaches that use multi-label setting, the learning is implemented as binary classification that estimates the pairwise-relevance of (theorem, premise) pairs. ATPboost uses for this the fast state-of-the-art XGBoost gradient boosting algorithm. Learning in the binary setting however requires negative examples, which is nontrivial due to many alternative proofs. We discuss and implement several solutions in the context of the ATP/ML feedback loop, and show significant improvement over the multi-label approach.

Název v anglickém jazyce

ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback

Popis výsledku anglicky

ATPboost is a system for solving sets of large-theory problems by interleaving ATP runs with state-of-the-art machine learning of premise selection from the proofs. Unlike many approaches that use multi-label setting, the learning is implemented as binary classification that estimates the pairwise-relevance of (theorem, premise) pairs. ATPboost uses for this the fast state-of-the-art XGBoost gradient boosting algorithm. Learning in the binary setting however requires negative examples, which is nontrivial due to many alternative proofs. We discuss and implement several solutions in the context of the ATP/ML feedback loop, and show significant improvement over the multi-label approach.

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í

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 statě ve sborníku

Automated Reasoning

ISBN

978-3-319-94204-9

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

9

Strana od-do

566-574

Název nakladatele

Springer

Místo vydání

Basel

Místo konání akce

Oxford

Datum konání akce

14. 7. 2018

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

WRD - Celosvětová akce

Kód UT WoS článku

000470004600037