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

We discuss standard First Order Logic (FOL) formula modulo theory $\mathcal{T}$, with a signature $\Sigma$ composed by constant symbols $\mathcal{A}$ (e.g., True $\top$ and False $\bot$), function symbols $\mathcal{F}$ (e.g., +, -, mod) and predicate symbols $\mathcal{P}$. A Constrained Horn Clause (CHC) $\mathcal{C}$ is a FOL formula modulo theory $\mathcal{T}$ in the following form:

where $\mathcal{X}$ stands for all variables in $T_{i}$ and $T$, $\phi$ represents a fixed constraint over $\mathcal{F},\mathcal{A}\text{ and }\mathcal{X}$ w.r.t. some background theory $\mathcal{T}$; $p_{i},h$ are uninterpreted predicate symbols⁵⁵5“Predicates” for short., and $p_{i}(T_{i})=p_{i}(t_{i,1},\cdots,t_{i,n})$ is an application of n-ary predicate symbol $p_{i}$ with first-order terms $t_{i,j}$ built from $\mathcal{F},\mathcal{A}\text{ and }\mathcal{X}$; $h(T)$ could be either $\mathcal{P}$-free (i.e., no predicate symbol appears in $h$) or akin to the definition of $p_{i}(T_{i})$.

In this work, we explain our framework using the background theory of Integer Arithmetic (IA) if it is not specified. For simplification, in our work, the universal quantifier “$\forall$” is omitted when the context is clear; and all terms $t_{i,j}$ represent single variables (e.g., $t_{1,1}=x$, $t_{1,2}=y$).

The structure of a CHC can be viewed as a split based on the implication symbol. The left hand side $\phi\wedge p_{1}(T_{1})\wedge\cdots\wedge p_{k}(T_{k})$ is called body and the right hand side $h(T)$ is called head. If the body of a CHC contains zero or one predicate symbol, the CHC is called linear. Otherwise, it is called non-linear.

In most cases, the terminology “CHC solving” refers to solving the satisfiability (SAT) problem for a CHC system that is a set of CHCs containing at least a query and a rule. A query $\mathcal{C}_{q}$ refers to a CHC that has a $\mathcal{P}$-free head, otherwise, it is called a rule $\mathcal{C}_{r}$. Particularly, a fact $\mathcal{C}_{f}$ refers to a rule that has a $\mathcal{P}$-free body. For instance, in Example 1, $\mathcal{C}_{0}$ is a fact and a rule, $\mathcal{C}_{1}$ is a rule, and $\mathcal{C}_{2}$ is a query. We define the clauses that both body and head are $\mathcal{P}$-free as trivial clauses because they can be simply reduced to $\top$ or $\bot$.

Then, we formally define the satisfiability of a CHC system $\mathcal{H}$:

If $\mathcal{H}$ is SAT, the proof is the corresponding interpretation $\mathcal{I}^{*}$, and $\mathcal{I}^{*}[p]$ is called a solution interpretation of the predicate $p$. If $\mathcal{H}$ is UNSAT, the proof is a refutation $\mathcal{R}$ demonstrating the nonexistence of a solution interpretation [3]. Therefore, the problem addressed in this work is to determine a solution for a given CHC system.

To harness data samples, we cast the CHC solving problem as a symbolic classification task by utilizing the samples to produce hypotheses. For clarity, we formally define the term hypothesis of a CHC system $\mathcal{H}$:

To determine a hypothesis for a specific predicate $p$ denoted as $\tilde{\mathcal{I}}\left[p\right]$, [45] introduces a lightweight machine learning toolchain that combines DT learning with the results of SVMs. In this data-driven pipeline, positive and negative samples are iteratively classified by SVMs until all samples are correctly categorized. The resulting hyperplanes of SVMs, $f(\boldsymbol{x})=w^{T}\boldsymbol{x}_{i}+b$, serve as attributes for the DT. The DT then selects an attribute $f(\boldsymbol{x}_{0})$ and a corresponding threshold $c$ in the form of $f(\boldsymbol{x}_{0})\leq c$ to create a new node in the way of maximizing the information gain $\gamma$. Adjusting the threshold $c$ and pruning the over-complicated attribute combinations enhances generalizability and mitigates overfitting risks. This process forms a DT, effectively segregating all samples into positive and negative categories. The DT generates a learned formula⁷⁷7The fundamentals of DT, SVM, and the formula generation is specified in Appendix 0.A., denoted as $\mathcal{L}_{p}$, which can be arbitrary linear inequalities and their combinations in disjunctive normal form (DNF). In our framework, this formula is termed a partition: a hypothesis proposed only by the learner.

Chronosymbolic Learning, depicted in Fig. 2, extends the paradigm of “teacher⁸⁸8Also refers to a verification oracle, such as Microsoft Z3. and learner” [16], which solves a given CHC system by guessing and checking [15, 37]. In this paradigm, the teacher and learner engage in iterative communication. During each iteration, the learner formulates a hypothesis (refer to Definition 3) of an interpretation called partition. The teacher then verifies the hypothesis and provides instant feedback regarding its correctness. If incorrect, the teacher supplies a counterexample (see Definition 8) elucidating the reason for its inaccuracy.

In addition to this paradigm, in Chronosymbolic Learning, the learning procedure is enhanced by a reasoner. The reasoner maintains a safe zone and an unsafe zone, representing symbolic equivalents of positive and negative samples respectively. These zones offer three main advantages: 1) They can be integrated into the learner’s proposed hypothesis to enhance it; 2) They provide the learner with additional samples; 3) They significantly simplify the UNSAT checking of the CHC system⁹⁹9In program verification parlance, it refers to the unsafe check.. We will provide an instance of Chronosymbolic Learning, detailing the functionality and intercommunication of its modules as in Fig. 2. The learner we specify in Section 4.1 and reasoner in Section 4.2 can be replaced by other algorithms capable of generating partitions and zones, as discussed in Section 7. See Section 3.4 for the overall algorithm.

To introduce Chronosymbolic Learning, we first conceptualize samples and zones. We shed light on obtaining the samples and zones in Section 4.

Positive samples and negative samples in our framework are defined as generalizations of reachable program states from facts and queries, and implication samples are defined as borrowed from the concept in [16].

A lemma can be directly derived from the definitions, signifying that a solution interpretation should summarize the information within the samples, and a sample should always evaluate to a certain truth value when making a valid hypothesis.

For ease of notation, for a sample $s$ and a CHC $\mathcal{C}$, we use $s[\mathcal{C}]$ to denote the clause $\mathcal{C}$ after a substitution, which replaces a list of variables with values when there is no ambiguity of the variable list.

We now formally define safe and unsafe zones, borrowing the terms “safe” and “unsafe” from program verification.

The zones are often symbolically represented as expressions, such as inequalities and equations. They may include zero sample¹⁰¹⁰10In this case, the zone is $\bot$., or a finite or infinite number of samples. Notably, a positive sample can also be viewed as a safe zone, while a negative sample can be seen as an unsafe zone.

Chronosymbolic Learning is a framework that incorporates zones within the learning iterations. A Chronosymbolic Learner proposes the hypothesis $\tilde{\mathcal{I}}\left[p_{i}\right]$ considering currently reasoned safe zones $\mathcal{S}_{p_{i}}$, unsafe zones $\mathcal{U}_{p_{i}}$ from the reasoner with the inductive results (partitions) of the learner $\mathcal{L}_{p_{i}}$.

Several promising candidates of the hypothesis $\tilde{\mathcal{I}}\left[p_{i}\right]$ that can be made by Chronosymbolic Learner¹¹¹¹11This is the procedure makeHypothesis() in Algorithm 1. are listed in Table 1. Note that Equation (6) simply serves as an example of a Chronosymbolic hypothesis. It can be replaced by any symbolic classification algorithm taking samples and zones as input, providing a symbolic hypothesis as output. We have the following lemma:

Lemma 2 shows the order of the feasibility of becoming a solution interpretation. We give a proof sketch for $\tilde{\mathcal{I}}_{sl}\succeq\tilde{\mathcal{I}}_{l}$ and proofs for others are similar.

In practice, Equation (6) generally delivers the optimal result among the candidates, as it encapsulates more information summarized by both the learner and the reasoner¹²¹²12Appendix 0.B provides additional theoretical analysis on why Chronosymbolic Learning performs better from the perspective of the state and solution space.. Nevertheless, this does not apply to every individual instance, since the introduction of zones might alter the exploration of the state space¹³¹³13This depends on the algorithms used in the teacher (in our instance, an SMT solver) to get counterexamples. After incorporating zones, the teacher may also return counterexamples that lead to less progress for the learner.. To address this issue, we can manually apply adequate strategies on each instance, or use a scheduler to alternate those candidate hypotheses over time. Our experiments will demonstrate the performance improvement achieved by employing various strategies.

The overall algorithm is outlined in Algorithm 1, where the solid bullet points denote mandatory steps and the unfilled bullet points indicate optional steps, suggesting that they need not be executed in every iteration.

The algorithm takes a CHC system $\mathcal{H}$ as input and outputs a solution for it. Initialization of zones, hypotheses, UNSAT flag, and the dataset occurs in lines 1-4. The outer while loop, spanning lines 5 to 18, checks if a solution of $\mathcal{H}$ has been found. If not, it initiates a new epoch and continues solving. In line 5, SMTCheck($\tilde{\mathcal{I}}\left[\mathcal{C}_{i}\right]$) calls the backend SMT solver to check the satisfiability of a CHC $\mathcal{C}_{i}$ under current hypothesis interpretation $\tilde{\mathcal{I}}$. In line 6, the reasoner refines the zones and checks if the zones overlap (see Section 4.2). Line 7 involves the sampling procedure described in Section 4.1.2.

The for loop from lines 8-17 iteratively finds an UNSAT CHC and refines the hypothesis until it becomes SAT¹⁴¹⁴14An alternative design choice is to update the hypothesis only once and move to the next UNSAT CHC, which achieves better results in some cases.. In the inner while loop in lines 10-13, we find one or a batch of counterexamples, convert them into samples, and add them to the dataset after the UNSAT checking¹⁵¹⁵15For simplicity, the refutation proof generated when checking UNSAT is also represented as $\tilde{\mathcal{I}}$ in Algorithm 1. passes. SMTModel($\tilde{\mathcal{I}}\left[\mathcal{C}_{i}\right]$) in line 10 calls the backend SMT solver to return a counterexample that elucidates why the current hypothesis is invalid. Following dataset updates, in lines 14-15, the learner induces a new partition. We then update the Chronosymbolic hypothesis by combining the zonal information and the partition, as described in Section 3.3. The new hypothesis is more likely to be a solution interpretation (if the CHC system is SAT), as it integrates the newly acquired information gathered in this iteration¹⁶¹⁶16Here we do not consider approximation error in classification or tentative samples defined later..

The learner module in our framework leverages an induction-based and CEGAR-inspired [10] CHC solving scheme. It has two sub-modules: the dataset and the machine learning toolchain. The dataset stores the positive and negative samples and the corresponding predicates for inductive learning. The machine learning toolchain (an example introduced in Section 2.2) takes the samples in the dataset as input and outputs a partition that correctly classifies all these samples.

For the reasoner, we adopt a simple BMC-styled logical reasoning procedure for inferring safe and unsafe zones in our instance of Chronosymbolic Learning. The role of the reasoner is not to deduce a complete hypothesis but to furnish a “partial solution” in the form of safe and unsafe zones, collaborating well with the learner. The zones condense information within a bounded number of transitions. In our tool, the reasoner initializes the zones, expands the zones through image (or pre-image) computation, and does UNSAT checking.

In each of the subsequent lemmas, all variables utilized in the discussed CHC are denoted as $\mathcal{X}$. Among them, variables used by the discussed predicate are denoted as $\mathcal{X}_{\mu}\subseteq\mathcal{X}$. The other variables are called free variables, denoted as $\mathcal{X}_{\varphi}=\mathcal{X}\setminus\mathcal{X}_{\mu}\subseteq\mathcal{X}$.

State-of-the-art CHC solvers can be classified into three categories: reasoning-based, synthesis-based, and induction-based solvers (see Section 6). We compare our method against the representatives of each type as follows:

The performance comparison ²⁷²⁷27For detailed timing of each instance, see https://github.com/Chronosymbolic/Chronosymbolic-Learning/blob/main/experiment/comparison.xlsx is shown in Table 2. “Chronosymbolic-single” configuration stands for the best result from a single run of our solver, where all instances are tested using a fixed set of hyperparameters. “Chronosymbolic-cover” encompasses all solved benchmarks achieved through 13 runs²⁸²⁸28The details are included in Appendix 0.D.2. using different strategies and hyperparameters, demonstrating the potential capability of our framework when selecting an adequate configuration for each instance. Timing information for this setting is not included because the time to solve a certain benchmark varies among different runs. Fig. 3 shows the solved instances for compared methods as the running time increases, and Fig. 4 shows the runtime comparison per instance.

Our tool, even in the Chronosymbolic-single setting, solves $17$ more instances than the best competing solver, GSpacer, and generally outperforms other solvers in terms of speed, even though it is implemented in Python. This result shows that our tool performs considerably better even without careful tuning for each CHC instance. In the Chronosymbolic-cover setting, our approach shows significant improvements, emphasizing the need for tailored strategies for different instances. Among other approaches, GSpacer performs the best on solved instances and time consumed, as reported in prior literature. Nevertheless, Spacer, GSpacer, and LinearArbitrary struggle with most instances involving non-linear arithmetic. FreqHorn can solve some of them, but fails in all unsafe instances without resorting to another procedure “expl”. Our approach can also handle limited non-linearity because our reasoner can induce non-linear zones.

From Fig. 3, we note that Chronosymbolic-single outperforms FreqHorn and LinearArbitrary under any timeout within 360 seconds, showing the enhanced efficiency of our method. It is also expected that Spacer and GSpacer perform the best under an extremely short time limit as they do not involve time-consuming inductive learning.

For CHC-COMP, most benchmarks represent large transition systems with a substantial number of Boolean variables. Reasoning-based approaches inherently suit these benchmarks better, and unsurprisingly, invoking the machine learning toolchain in each iteration is an inefficient design choice. An experiment shows that by filtering out benchmarks in CHC-COMP-22-LIA with excessively large sizes (e.g., exceeding 100 rules or 200 variables), our results are on par with the state-of-the-art (Chronosymbolic-cover 129/208 vs. GSpacer 130/208).

We further study the effectiveness of the critical parts of our framework: the learner and the reasoner. For the reasoner, we compare the result when safe zones are not provided, when unsafe zones are not provided, and when neither are provided. Additionally, we assess the performance when entirely removing the learner and running our tool solely with the reasoner. Throughout this ablation study, all other settings remain consistent with Chronosymbolic-single.

From Table 4, as expected, Chronosymbolic-single comprehensively outperforms all other configurations, which shows that each component of our framework is indispensable. It is also clear that each zone provides useful information to the hypothesis, making the result of Chronosymbolic without both zones worse than without safe and unsafe zones. As discussed in Section 4.2.2 and Appendix 0.C.2, our lightweight reasoner is intended to aid the learner. Thus, not utilizing a learner yields the poorest result, but at a faster computation speed. The result also shows that our learner²⁹²⁹29“Without both zones” indicates that the reasoner does not participate. performs much better than LinearArbitrary, as we have a more comprehensive converting and sampling scheme.

Another experiment in Table 4, “parallel”, reveals that if we run our learner and reasoner individually and simultaneously for $360$ seconds, they only solve a total of $180$ safe and $36$ unsafe instances. This number is significantly lower than what our proposed method achieves, which underscores the mutual benefit of the reasoner and learner in Chronosymbolic Learning.