Machine Learning for Quantifier Selection in cvc5

要約

この研究では、量化子選択の効率的な機械学習ガイダンスによって、一次量化問題を解決する最先端の SMT を大幅に改善しました。
量化子は SMT にとって大きな課題であり、技術的には決定不可能性の原因となります。
私たちのアプローチでは、どの量指定子をインスタンス化する必要があり、どれをインスタンス化すべきでないかをソルバーに通知する効率的な機械学習モデルをトレーニングします。
各量指定子は複数回インスタンス化される場合があり、アクティブな量指定子のセットは解決が進むにつれて変化します。
したがって、ソルバーの実行中、ML 予測子を何度も呼び出します。
これを効率的に行うために、勾配ブースティング デシジョン ツリーに基づく高速 ML モデルを使用します。
私たちのアプローチを最先端の cvc5 SMT ソルバーに統合し、Mizar Mathematical Library から収集された大規模な 1 次問題セットでシステムをトレーニングした後、システムのホールドアウトセットのパフォーマンスが大幅に向上することを示しました。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google