cvc5 中量子选择的机器学习

在本工作中，我们通过高效的机器学习指导量子选择，大幅提升了 first-order 量子问题的 SMT 求解器性能。量子是 SMT 求解的主要挑战，也是不可判定性的技术来源。在我们的方法中，我们训练一个高效的机器学习模型，以指示求解器应实例化哪些量子以及哪些不应实例化。每个量子可能被实例化多次，且活跃量子的集合会随求解进程而变化。因此，我们需要在求解器整个运行期间多次调用 ML 预测器。为实现效率，我们使用基于梯度提升决策树的快速 ML 模型。我们将方法集成到领先的 cvc5 SMT 求解器中，并在从 Mizar 数学图书馆收集的大型 first-order 问题集合上训练后，显示出显著提升的系统 holdout 集性能。