Machine Learning for Quantifier Selection in cvc5

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F24%3A00380239" target="_blank" >RIV/68407700:21730/24:00380239 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.3233/FAIA241009" target="_blank" >https://doi.org/10.3233/FAIA241009</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.3233/FAIA241009" target="_blank" >10.3233/FAIA241009</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Machine Learning for Quantifier Selection in cvc5

Popis výsledku v původním jazyce

In this work we considerably improve the state-of-the-art SMT solving on first-order quantified problems by efficient machine learning guidance of quantifier selection. Quantifiers represent a sig nificant challenge for SMT and are technically a source of undecid ability. In our approach, we train an efficient machine learning model that informs the solver which quantifiers should be instantiated and which not. Each quantifier may be instantiated multiple times and the set of the active quantifiers changes as the solving progresses. There fore, we invoke the ML predictor many times, during the whole run of the solver. To make this efficient, we use fast ML models based on gradient boosted decision trees. We integrate our approach into the state-of-the-art cvc5 SMT solver and show a considerable increase of the system’s holdout-set performance after training it on a large set of first-order problems collected from the Mizar Mathematical Library.

Název v anglickém jazyce

Machine Learning for Quantifier Selection in cvc5

Popis výsledku anglicky

In this work we considerably improve the state-of-the-art SMT solving on first-order quantified problems by efficient machine learning guidance of quantifier selection. Quantifiers represent a sig nificant challenge for SMT and are technically a source of undecid ability. In our approach, we train an efficient machine learning model that informs the solver which quantifiers should be instantiated and which not. Each quantifier may be instantiated multiple times and the set of the active quantifiers changes as the solving progresses. There fore, we invoke the ML predictor many times, during the whole run of the solver. To make this efficient, we use fast ML models based on gradient boosted decision trees. We integrate our approach into the state-of-the-art cvc5 SMT solver and show a considerable increase of the system’s holdout-set performance after training it on a large set of first-order problems collected from the Mizar Mathematical Library.

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

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

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

Rok uplatnění

2024

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

ECAI 2024 - 27th European Conference on Artificial Intelligence

ISBN

978-1-64368-548-9

ISSN

0922-6389

e-ISSN

1879-8314

Počet stran výsledku

8

Strana od-do

4336-4343

Název nakladatele

IOS Press

Místo vydání

Oxford

Místo konání akce

Santiago de Compostela

Datum konání akce

19. 10. 2024

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

WRD - Celosvětová akce

Kód UT WoS článku

—