LLM-Assisted Bi-Approximate CHC Solving
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. Validat...
| Authors | Baiting Jiang |
|---|---|
| Primary category | cs.LO |
| Published | 16 October 2026 |
| Last updated at source | 16 October 2026 |
Popularity, last 4 days
0 now. Counts as reported by the source, snapshotted daily by Silytics.
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 23 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.