LLM enhances solving constrained Horn clauses with new under-approximation method
LLM-Assisted Bi-Approximate CHC Solving
Logic in Computer Science
Summary
Finding errors in certain computer logic rules can be very hard, especially when solutions require many steps to show. The authors combine a big AI language model with formal checking to create a way to guess and verify parts of these complex solutions more easily. Their new method lets the AI suggest small pieces of a solution that a solver then checks rigorously, making it possible to solve many hard logic problems that previous methods missed. This improves both the detection of errors and the proving of correctness in software verification.
What this means in practice
- •For software verification engineers: Produce certified proofs or counterexamples for challenging software verification tasks involving complex logic rules.
- •For automated theorem proving developers: Integrate LLM-generated under-approximations to improve solver performance on benchmarks with nonlinear integer arithmetic constraints.
Authors
Baiting Jiang
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.