Chronosymbolic Learning

🔍 Chronosymbolic Learning: A New Paradigm for CHC Solving, with Machine Learning and Symbolic Synergy

At SAIV, we introduce a novel framework for solving Constrained Horn Clauses (CHCs)—a foundational formalism in program verification. Our approach, Chronosymbolic Learning, rethinks CHC solving by synergizing symbolic reasoning with machine learning approaches. Let’s walk through what this means, and why it matters.

🧩 What Are CHCs, and Why Do They Matter?

CHCs are logical formulas—fragments of first-order logic (FOL)—that underpin many program verification tasks (but not limited to). Crucially, programs can be automatically transformed into CHCs, reducing verification to a constraint-solving problem. CHCs elegantly capture constructs like loop invariants (corresponding to CHCs’ solution interpretation of predicates), making them a fundamental tool for formal reasoning.

⚖️ Black-Box or White-Box? Why Not Both?

CHC solvers today often fall into two camps:

• Black-box approaches leverage machine learning to build abstractions from data, but tend to be sample inefficient.
• White-box approaches use symbolic reasoning directly on CHCs, but often lack flexibility dealing with data points which can be easily sampled sometimes.

Each has complementary strengths and limitations.

🔄 Our Approach: Unifying the Two Worlds

Chronosymbolic Learning provides a modular framework where black-box and white-box methods cooperate. We identify and formalize key concepts like samples, zones, and counterexamples (definition and examples see slides, page 13-18), and show how they can interact seamlessly. The result: a solver pipeline that is both data-aware and logically grounded.

🔁 Iterative CHC Solving Algorithm

1. Zone & Partition Proposal
   Learner and reasoner propose new zones and partitions from current zones and samples.

2. Hypothesis Generation
   Construct a hypothesis (see Table 1) based on proposed zones and samples.

3. Satisfiability Check

   • Check satisfiability for one interpreted CHC.
   • If SAT, move to the next CHC.
   • If UNSAT, return a counterexample and convert it into new data samples.

4. Global Consistency Check
   Use samples and zones to check UNSAT for the CHC system (cf. Lemmas 5, 6, 11).

5. Sampling
   Generate additional samples from current zones.

6. Termination
   If all CHCs are SAT, return the solution interpretation (loop invariant).

🛠️ From Concept to Implementation

We provide a minimal, proof-of-concept instance of our framework and conduct a thorough evaluation to validate its promise. Our findings show that this hybrid design can offer practical advantages in efficiency of CHC solving.

Everything is built from scratch and fully pythonic! 🔗 -> Artifact available here

Takeaway: Chronosymbolic Learning bridges symbolic rigor and learning flexibility—reshaping how we verify programs.