ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
The result's identifiers
Result code in 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>
Alternative codes found
RIV/68407700:21730/18:00329539
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
Original language description
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.
Czech name
—
Czech description
—
Classification
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)
Result continuities
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)
Others
Publication year
2018
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Automated Reasoning
ISBN
978-3-319-94204-9
ISSN
0302-9743
e-ISSN
—
Number of pages
9
Pages from-to
566-574
Publisher name
Springer
Place of publication
Basel
Event location
Oxford
Event date
Jul 14, 2018
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000470004600037