LLM-Assisted Bi-Approximate CHC Solving

Baiting Jiang

cs.LOOct 16, 2026

LLM-Assisted Bi-Approximate CHC Solving

Authors: Baiting Jiang

Organizations: Tsinghua University, China

Abstract

Constrained Horn clause (CHC) solvers often struggle to discover deep counterexamples whose derivations may require extensive rule unfolding. Although large language models (LLMs) can propose long-range symbolic relations, prior work on formally checked LLM-assisted verification has mainly focused on generating inductive invariants and concrete traces. We exploit this broader capability through Derivation Power Under-approximations (DPUs). Each DPU is a solver-certified under-approximation of the relation induced by a multi-step CHC derivation. An LLM proposes each DPU with symbolic intermediate-state witnesses that enable SMT validation without introducing additional quantifiers. Validated DPUs can be composed and reused soundly. Building on this mechanism, our LLM-assisted framework HornCraft combines invariant generation for over-approximation with DPU generation for under-approximation in CHC solving. On 260 linear and nonlinear integer-arithmetic CHC-COMP benchmarks left unresolved by a 30-minute Spacer run, HornCraft returns certified verdicts for 228 instances. It certifies 42 instances as unsafe, compared with 22 when DPU construction and reuse are disabled.

Figures & tables

Figure 2. DPU compression in the motivating example. A two-phase derivation connects the initial state to the bad state after 1,000 original transitions. Certified DPUs summarize two, four, and 500 transitions, reducing the number of represented steps.

Figure 3. Overview of the HornCraft framework. HornCraft first runs Spacer on the input CHCs. For unresolved instances, an LLM proposes invariant atoms, witness-carrying DPUs, and reach facts with derivations. Solver-backed checks admit certified artifacts across the trusted boundary for over-approximate safety and under-approximate reachability reasoning.

Figure 4. Compositional DPU certification for the motivating example. Two dependency chains certify increasingly long DPUs for the left and right phases. Previously certified powers are combined into two 500-step DPUs, which connect the initial state to the bad state.

1	$f\leftarrow\emptyset$
2	for each $c\in\mathcal{K}$ in submission order while $\Delta$ permits certification do
3	if not $\textsc{Ready}(c,\mathcal{C},\mathcal{D},\mathcal{R})$ then
4	record rejection in $f$ ; continue
5	end if
6	if $c$ is a DPU candidate $(\bar{r},\pi,D,w)$ then
7	$(B_{\pi},H_{\pi},\varphi_{n}^{\pi})\leftarrow\textsc{ComposeRules}(\bar{r},\pi)$

Algorithm 1 ReachStep : certifying a batch of DPUs and RFs

1	$\mathcal{B}\leftarrow\bigl(\emptyset,\emptyset,(\top)_{P\in\mathcal{P}}\bigr)$ ; $f\leftarrow\emptyset$
2	$(v,\mathcal{B},f)\leftarrow\textsc{RunSpacer}(\mathcal{C},\mathcal{B},\Delta)$
3	if $v\neq\texttt{unknown}$ then return $v$
4	while $\Delta$ permits interaction do
5	$a\leftarrow\textsc{NextLLMAction}(\mathcal{C},\mathcal{B},f,\Delta)$
6	if $a$ is a mixed candidate batch $(\mathcal{K},A)$ then
7	$(\mathcal{B},f)\leftarrow\textsc{CertifyBatch}(\mathcal{C},\mathcal{B},\mathcal{K},A,f,\Delta)$

Algorithm 2 HornCraft’s LLM-guided certification loop

Track	Expected safe	Expected unsafe	Expected unknown	Overall
LIA-Lin	137/149 (92%)	32/32 (100%)	17/21 (81%; 11 S + 6 U)	186/202 (92%)
LIA	30/36 (83%)	3/3 (100%)	9/19 (47%; 8 S + 1 U)	42/58 (72%)
Total	167/185 (90%)	35/35 (100%)	26/40 (65%; 19 S + 7 U)	228/260 (88%)

Table 1. HornCraft on Spacer-hard CHC-COMP instances.

Solver and track	Cases	Expected safe	Expected unsafe	Expected unknown	Overall
LoAT–LIA-Lin	52	18/21 (86%)	10/10 (100%)	17/21 (81%; 11 S + 6 U)	45/52 (87%)
Golem–LIA-Lin	118	80/91 (88%)	6/6 (100%)	17/21 (81%; 11 S + 6 U)	103/118 (87%)
Eldarica–LIA	35	10/15 (67%)	1/1 (100%)	9/19 (47%; 8 S + 1 U)	20/35 (57%)

Table 2. HornCraft on instances unresolved by other solvers in CHC-COMP 2026.

Figure 5. Input and output token use. Two scatter panels show 202 LIA-Lin executions on the left and 58 LIA executions on the right. Each point pairs input and output tokens on identical base-10 logarithmic axes. Open circles denote safe outcomes, crosses unsafe outcomes, and open triangles unresolved outcomes. Five input cache hit bands, below 70, 70 to 80, 80 to 90, 90 to 95, and at least 95 percent, progress from cool dark blue through purple and magenta to warm orange. LIA-Lin has many low-token safe and unsafe runs. Unresolved runs tend toward higher token use. Some closely neighboring points overlap.

Figure 6. Execution-time breakdown. Two columns show all 202 LIA-Lin and 58 LIA Full executions, including unresolved runs, sorted within each track by increasing wall-clock time. Each stacked bar gives the elapsed seconds of one execution. Light blue, ochre, and dark gray distinguish Agent, Formal Engine, and Other, respectively, in a fixed bottom-to-top order. Agent interaction accounts for most elapsed time in most runs, while some long runs have substantial formal-engine processing. The dashed line marks the 1800-second budget.

Family	(instances)	Spacer	Without DPU	Full	Time (s)	Tokens (M)
	Tested $n$	Maximum solved $n$			Full at maximum $n$
Hanoi (linear)	4–20 (9)	4	12	20	207.5	0.63 (93%)
Hanoi (path)	4–20 (9)	4	12	20	238.3	0.59 (91%)
Ackermann	3–10 (8)	4	6	8	841.3	3.34 (96%)
Chinese Rings	4–20 (9)	6	12	20	682.5	3.24 (95%)
Pascal	10–10,000 (7)	100	300	1,000	601.5	2.38 (96%)

Table 3. Maximum solved

n

across benchmark families.

Figure 7. Scalability across the six CHC families. Six panels in two rows show solving time against parameter n for Hanoi linear, Hanoi path, Ackermann, Chinese Rings, Pascal, and Tarai. All panels share a linear runtime scale from 0 to 1200 seconds, with an explicit axis break before a separate 1800-second budget line. Pascal and Tarai use logarithmic parameter axes. Blue circles represent Full, ochre squares represent Without DPU, and gray crosses represent Spacer. Curves connect solved runs. A marker on the dotted budget line identifies the first unsolved tested parameter for each configuration; all larger tested parameters are also unsolved. Unsolved includes unresolved runs, timeouts, and errors. These markers denote status, not measured runtimes. Nested outlines distinguish coincident boundaries. Each panel spans its family's full tested range. Full reaches larger parameters than Without DPU in five families. Full has lower time at the largest shared solved parameter in the two Hanoi encodings and Chinese Rings, and higher time there in Ackermann and Pascal. Both configurations reach n equal to 20 on Tarai with similar solving times.

Family	$n$	Used DPUs	Compact proof source uses	Expanded original clause uses	Largest used DPU expanded span
Hanoi (path)	20	20	82	2,097,153	2,097,150
Ackermann	8	122	3,922	2,785,999	40,630
Chinese Rings	20	83	213	1,398,103	1,398,100
Pascal	1,000	282	4,275	998,999	61,024
Tarai	20	0	3,478	$5.60\times 10^{14}$	—

Table 4. Derivation compression on selected nonlinear instances.

Track	Configuration	Safe	Unsafe	Solved / Cases
LIA-Lin	Full	148	38	186/202 (92%)
	Without DPU	146	17	163/202 (81%)
LIA	Full	38	4	42/58 (72%)
	Without DPU	34	5	39/58 (67%)
Total	Full	186	42	228/260 (88%)
	Without DPU	180	22	202/260 (78%)

Table 5. DPU ablation on Spacer-hard CHC-COMP instances.

Figure 8. Runtime comparison with and without DPU. Two scatter plots compare Without DPU on the horizontal axis with Full on the vertical axis, for LIA-Lin and LIA. Blue circles denote safe outcomes and ochre crosses denote unsafe outcomes. Points below the diagonal indicate faster Full runs. Shaded margins marked U are categorical unresolved outcomes, not runtimes. Points in the right margin are solved only by Full. Points in the top margin are solved only without DPU. The right margin for LIA-Lin contains 21 unsafe instances solved only by Full.

Formal Verification

Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.

See all 345 papers

Formalize, Don't Optimize: The Heuristic Trap in LLM-Generated Combinatorial Solvers
May 12, 2026Haoyu Wang, Yuliang Song, Tao Li +5Large Language Model-Guided Optimization LLM-Based Program Synthesis
University of Pennsylvania · University of Toronto · Google DeepMind +1
Can LLM Aid in Solving Constraints with Inductive Definitions?
Mar 4, 2026Weizhi Feng, Shidong Shen, Jiaxiang Liu +3Automated Theorem Proving Neuro-Symbolic Reasoning
Key Laboratory of System Software (Chinese Academy of Sciences), Institute of Software, Chinese Academy of Sciences, Beijing, China · University of Chinese Academy of Sciences, Beijing, China · Birkbeck, University of London, United Kingdom +1
Analyzing the Narration Gap in LLM-Solver Loops
Jun 17, 2026Zunchen Huang, Songgaojun DengAdversarial Attacks on LLMs Formal Verification
Centrum Wiskunde & Informatica, Amsterdam, The Netherlands · Eindhoven University of Technology, Eindhoven, The Netherlands

May 12, 2026J/K move · Enter open · S save

Formalize, Don't Optimize: The Heuristic Trap in LLM-Generated Combinatorial Solvers

Haoyu Wang, Yuliang Song, Tao Li, Zhiwei Deng+4

University of Pennsylvania · University of Toronto · Google DeepMind+1

Large Language Model-Guided Optimization LLM-Based Program Synthesis Combinatorial Optimization Natural Language to Optimization Modeling Constraint Programming

Open paper AskPDF arXiv

Large Language Models (LLMs) struggle to solve complex combinatorial problems through direct reasoning, so recent neuro-symbolic systems increasingly use them to synthesize executable solvers. A central design question is how the LLM should represent the solver, and whether it should also attempt to optimize search. We introduce CP-SynC-XL, a benchmark of 100 combinatorial problems (4,577 instances), and evaluate three solver-construction paradigms: native algorithmic search (Python), constraint modeling through a Python solver API (Python + OR-Tools), and declarative constraint modeling (MiniZinc + OR-Tools). We find a consistent representational divergence: Python + OR-Tools attains the highest correctness across LLMs, while MiniZinc + OR-Tools has lower absolute coverage despite using the same OR-Tools back-end. Native Python is the most likely to return a schema-valid solution that fails verification, whereas solver-backed paths preserve higher conditional fidelity. On the heuristic axis, prompting for search optimization yields only small median speed-ups (1.03-1.12x) and a strongly bimodal effect: many instances slow down, and correctness drops sharply on a long tail of problems. A paired code-level audit traces these regressions to a recurring heuristic trap. Under an efficiency-oriented prompt, the LLM may replace complete search with local approximations (Python), inject unverified bounds (Python + OR-Tools), or add redundant declarative machinery that overwhelms or over-constrains the model (MiniZinc + OR-Tools). These findings support a conservative design principle for LLM-generated combinatorial solvers: use the LLM primarily to formalize variables, constraints, and objectives for verified solvers, and separately check any LLM-authored search optimization before use.

Abstract

Formal Verification

Explore similar work

Formalize, Don't Optimize: The Heuristic Trap in LLM-Generated Combinatorial Solvers

Can LLM Aid in Solving Constraints with Inductive Definitions?

Analyzing the Narration Gap in LLM-Solver Loops