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

要約

タイトル：Chronosymbolic Learning：シンボリック推論と帰納学習による効率的なCHCソルバーの解決方法
要約：
– CHC（Constrained Horn Clauses）を解決することは、さまざまな検証および分析タスクにおける基本的な課題である。
– データ駆動型のアプローチは、さまざまなヒューリスティックを作成して微調整する手間を省いて、CHC問題の解決を改善するという有望な結果を示している。
– しかし、データ駆動型のCHCソルバーとシンボリック推論ベースのソルバーの間には、大きな性能差が存在している。
– 本研究では、シンボリック情報と数値データポイントを統合することで、効率的にCHCシステムを解決するための「Chronosymbolic Learning」というシンプルで効果的なフレームワークを開発した。
– また、データ駆動型の学習者とBMCスタイルの推論システムを持つChronosymbolic Learningの単純なインスタンスも提供する。
– 大変シンプルであるにもかかわらず、実験結果は、Chronosymbolic Learningが高い効果と堅牢性を示すことを示している。
– 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 great 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, OpenAI