{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,18]],"date-time":"2024-10-18T04:28:40Z","timestamp":1729225720411,"version":"3.27.0"},"reference-count":0,"publisher":"IOS Press","isbn-type":[{"value":"9781643685489","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,16]],"date-time":"2024-10-16T00:00:00Z","timestamp":1729036800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,10,16]]},"abstract":"<jats:p>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 significant challenge for SMT and are technically a source of undecidability. 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. Therefore, 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\u2019s holdout-set performance after training it on a large set of first-order problems collected from the Mizar Mathematical Library.<\/jats:p>","DOI":"10.3233\/faia241009","type":"book-chapter","created":{"date-parts":[[2024,10,17]],"date-time":"2024-10-17T13:55:09Z","timestamp":1729173309000},"source":"Crossref","is-referenced-by-count":0,"title":["Machine Learning for Quantifier Selection in cvc5"],"prefix":"10.3233","author":[{"given":"Jan","family":"Jakub\u016fv","sequence":"first","affiliation":[{"name":"Czech Technical University in Prague, Prague, Czech Republic"},{"name":"University of Innsbruck, Innsbruck, Austria"}]},{"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"additional","affiliation":[{"name":"Czech Technical University in Prague, Prague, Czech Republic"}]},{"given":"Jelle","family":"Piepenbrock","sequence":"additional","affiliation":[{"name":"Czech Technical University in Prague, Prague, Czech Republic"},{"name":"Radboud University, Nijmegen, Netherlands"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[{"name":"Czech Technical University in Prague, Prague, Czech Republic"}]}],"member":"7437","container-title":["Frontiers in Artificial Intelligence and Applications","ECAI 2024"],"original-title":[],"link":[{"URL":"https:\/\/ebooks.iospress.nl\/pdf\/doi\/10.3233\/FAIA241009","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,17]],"date-time":"2024-10-17T13:55:09Z","timestamp":1729173309000},"score":1,"resource":{"primary":{"URL":"https:\/\/ebooks.iospress.nl\/doi\/10.3233\/FAIA241009"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,16]]},"ISBN":["9781643685489"],"references-count":0,"URL":"https:\/\/doi.org\/10.3233\/faia241009","relation":{},"ISSN":["0922-6389","1879-8314"],"issn-type":[{"value":"0922-6389","type":"print"},{"value":"1879-8314","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,16]]}}}