Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning

要約

Constrained Horn Clauses (CHC) を解決することは、幅広い検証および分析タスクの背後にある基本的な課題です。
データ駆動型のアプローチは、さまざまなヒューリスティックの作成や調整といった骨の折れる手作業を必要とせずに、CHC の解決を改善する上で大きな期待をもたらします。
ただし、データ駆動型 CHC ソルバーと記号推論ベースのソルバーの間には、大きなパフォーマンスのギャップが存在します。
この研究では、CHC システムを効率的に解くために記号情報と数値データ ポイントを統合する、シンプルだが効果的なフレームワーク「時間記号学習」を開発します。
また、データ駆動型学習器と BMC スタイルの推論器を使用した時間記号学習の簡単なインスタンスも紹介します。
比較的単純であるにもかかわらず、実験結果は私たちのツールの有効性と堅牢性を示しています。
非線形整数演算を使用する多くのインスタンスを含む 288 のベンチマークで構成されるデータセット上で、最先端の CHC ソルバーよりも優れたパフォーマンスを発揮します。

要約(オリジナル)

Solving Constrained Horn Clauses (CHCs) is a fundamental challenge behind a wide range of verification and analysis tasks. Data-driven approaches show great promise in improving CHC solving without the painstaking manual effort of creating and tuning various heuristics. However, a large performance gap exists between data-driven CHC solvers and symbolic reasoning-based solvers. In this work, we develop a simple but effective framework, ‘Chronosymbolic Learning’, which unifies symbolic information and numerical data points to solve a CHC system efficiently. We also present a simple instance of Chronosymbolic Learning with a data-driven learner and a BMC-styled reasoner. Despite its relative simplicity, experimental results show the efficacy and robustness of our tool. It outperforms state-of-the-art CHC solvers on a dataset consisting of 288 benchmarks, including many instances with non-linear integer arithmetics.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google