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

arXiv: https://arxiv.org/abs/2305.01206 · HTML: https://mlsanity.com/paper/2305.01206/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 8 of its 51 references that are in the map.
- First posted on arXiv 2 May 2023.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 8 of 8)

- [Interpretable Scientific Discovery with Symbolic Regression: A Review](https://mlsanity.com/paper/2211.10873/) (2022)
- [An Approach to Symbolic Regression Using Feyn](https://mlsanity.com/paper/2104.05417/) (2021)
- [Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)](https://mlsanity.com/paper/2003.07959/) (2020)
- [SMT-based Model Checking for Recursive Programs](https://mlsanity.com/paper/1405.4028/) (2014)
- [RustHorn: CHC-based Verification for Rust Programs (full version)](https://mlsanity.com/paper/2002.09002/) (2020)
- [Global Guidance for Local Generalization in Model Checking](https://mlsanity.com/paper/2005.13301/) (2020)
- [A Counterexample-guided Approach to Finding Numerical Invariants](https://mlsanity.com/paper/1903.12113/) (2019)
- [Automatic Abstraction in SMT-Based Unbounded Software Model Checking](https://mlsanity.com/paper/1306.1945/) (2013)

## Abstract (arXiv)

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.