# Machine Learning for Quantifier Selection in cvc5

arXiv: https://arxiv.org/abs/2408.14338 · HTML: https://mlsanity.com/paper/2408.14338/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 14 of its 57 references that are in the map.
- First posted on arXiv 26 Aug 2024.

## Builds on (most cited first, 14 of 14)

- [ENIGMA: Efficient Learning-based Inference Guiding Machine](https://mlsanity.com/paper/1701.06532/) (2017)
- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [Hammering Mizar by Learning Clause Guidance](https://mlsanity.com/paper/1904.01677/) (2019)
- [Vampire With a Brain Is a Good ITP Hammer](https://mlsanity.com/paper/2102.03529/) (2021)
- [Fast and Slow Enigmas and Parental Guidance](https://mlsanity.com/paper/2107.06750/) (2021)
- [The Isabelle ENIGMA](https://mlsanity.com/paper/2205.01981/) (2022)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [MizAR 60 for Mizar 50](https://mlsanity.com/paper/2303.06686/) (2023)
- [BliStrTune: Hierarchical Invention of Theorem Proving Strategies](https://mlsanity.com/paper/1611.08733/) (2016)
- [Graph Sequence Learning for Premise Selection](https://mlsanity.com/paper/2303.15642/) (2023)
- [Fair and Adventurous Enumeration of Quantifier Instantiations](https://mlsanity.com/paper/2105.13700/) (2021)
- [GRUNGE: A Grand Unified ATP Challenge](https://mlsanity.com/paper/1903.02539/) (2019)
- [Regularization in Spider-Style Strategy Discovery and Schedule Construction](https://mlsanity.com/paper/2403.12869/) (2024)
- [Solving Hard Mizar Problems with Instantiation and Strategy Invention](https://mlsanity.com/paper/2406.17762/) (2024)

## Abstract (arXiv)

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 boosting 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.