Lightweight Online Learning for Sets of Related Problems in Automated Reasoning

要約

私たちは、関連する一連の問題の解決を伴う自動推論タスクのための軽量オンライン学習方法論である Self-Driven Strategy Learning (sdsl) を紹介します。
SDSL は、以前の問題を解決しながら、データセットの形式で情報を自動的に収集します。
学習したデータを利用して、取得したデータに機械学習モデルをその場で適合させることで、後の問題の解決戦略を調整します。
このアプローチを一連の抽象的な移行ルールとして正式に定義します。
データ生成に条件付きサンプリングを使用し、基礎となる機械学習モデルとしてランダム フォレストを使用する SDSL 計算の具体的なインスタンスについて説明します。
Kissat ソルバーの上にこのアプローチを実装し、最新のハードウェア モデル チェックから得られたベンチマークで、Kissat + sdsl の組み合わせがより大きな境界を証明し、他の最先端の有界モデル チェック アプローチよりも多くの反例を見つけることを示します。
コンペ。

要約(オリジナル)

We present Self-Driven Strategy Learning (sdsl), a lightweight online learning methodology for automated reasoning tasks that involve solving a set of related problems. sdsl automatically gathers information, in form of a dataset, while solving earlier problems. It utilizes the learned data to adjust the solving strategy for later problems by fitting a machine learning model to the obtained data on the fly. We formally define the approach as a set of abstract transition rules. We describe a concrete instance of the sdsl calculus which uses conditional sampling for generating data and random forests as the underlying machine learning model. We implement the approach on top of the Kissat solver and show that the combination of Kissat+sdsl certifies larger bounds and finds more counter-examples than other state-of-the-art bounded model checking approaches on benchmarks obtained from the latest Hardware Model Checking Competition.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google