Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866916280479514624 |
|---|---|
| author | Luo, Ziyan Si, Xujie |
| author_facet | Luo, Ziyan Si, Xujie |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2305_01206 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning Luo, Ziyan Si, Xujie Logic in Computer Science Artificial Intelligence Machine Learning Programming Languages Symbolic Computation 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. |
| title | Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning |
| topic | Logic in Computer Science Artificial Intelligence Machine Learning Programming Languages Symbolic Computation |
| url | https://arxiv.org/abs/2305.01206 |