LLM-Assisted Bi-Approximate CHC Solving.

arXiv:2610.23771v1 Announce Type: cross 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 symboli