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

TL;DR

This work addresses the challenge of solving Constrained Horn Clauses (CHCs), which are central to program verification, and the performance gap between symbolic reasoning-based solvers and data-driven approaches. The authors propose Chronosymbolic Learning, a modular framework that combines a data-driven learner with a reasoner that maintains safe and unsafe zones, enabling mutual refinement of hypotheses. They present a simple Python-based instance featuring a data-driven learner, a BMC-style reasoner, and a verification oracle, and demonstrate that it outperforms several state-of-the-art CHC solvers on a dataset of 288 benchmarks, including non-linear integer arithmetic. Ablation studies show that both the learner and reasoner, and the zone information, contribute to performance, with Chronosymbolic single configuration solving more instances than baselines and Chronosymbolic cover further improving results across varied configurations. The work suggests a promising direction for integrating modern ML techniques with automated reasoning in CHC solving, with potential extensions to larger CHC systems and non-linear domains.

Abstract

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.

Figures (1)

• Figure 1: Overview of different approaches through the lens of learning from positive and negative samples.