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.

翻译：本研究通过高效的机器学习指导量词选择，显著提升了在一阶量化问题上的SMT求解技术水平。量词是SMT求解中的主要挑战之一，在技术上也是不可判定性的来源。在我们的方法中，我们训练了一个高效的机器学习模型，用于指导求解器判断哪些量词应被实例化、哪些不应。每个量词可能被多次实例化，且活跃量词集合会随着求解进程动态变化。因此，我们在求解器的整个运行过程中多次调用机器学习预测器。为实现高效预测，我们采用基于梯度提升决策树的快速机器学习模型。我们将该方法集成到当前最先进的cvc5 SMT求解器中，并在从Mizar数学库收集的大规模一阶问题上进行训练后，展示了系统在保留集上性能的显著提升。