Language models guide solvers to handle complex array problems better
Verifiable LLM-Guided Focal SMT Solving for Quantified Arrays
Artificial Intelligence
Summary
Formal logic solvers are good at checking mathematical statements but can get stuck when these statements hide important details behind complex structures. The authors show that large language models (LLMs) can suggest key parts of these problems to focus on, helping the solver find answers more effectively. Their system, LinguaArray, uses LLM suggestions but still verifies all results with traditional solver checks. This approach solved many more problems than solvers working alone in tests.
What this means in practice
- •For software verification teams: Solve complex logical formulas involving arrays faster by incorporating LLM-guided term selection in formal verification workflows.
- •For automated reasoning developers: Integrate LLM-driven semantic focus sets into SMT solvers to enhance their ability to handle quantified array benchmarks effectively.
Authors
Kunhang Lv, Rui Han, Fuqi Jia, Yuhang Dong, Feifei Ma, Jian Zhang
Abstract
Large language models can often identify useful semantic structure in formal artifacts, but their outputs cannot be trusted as proofs or solver decisions. We study whether LLMs can instead guide formal reasoning systems through a narrow, solver-verifiable interface. We instantiate this idea in quantified array SMT solving, where modern instantiation-based techniques can fail when key ground terms and equalities are hidden by auxiliary variables, axiom guards, and nested array terms. We observe that many instances are largely driven by a small set of focal ground terms or constraints, similar to the backdoor sets in SAT solving. Building on this, we present LinguaArray, a framework where an LLM proposes a small Semantic Focus Set (ground terms/constraints), while a conventional SMT solver remains the sole proof engine and certifies all results. LinguaArray uses these LLM-suggested, solver-validated finite sets to significantly enhance solver capability, solving additional satisfiable and unsatisfiable instances that the backend alone fails to solve. It interacts within a finite time and then falls back to the backend solver to mitigate potential regressions. Evaluation on 1015 SMT-LIB instances across five logics under 1200s timeout (including LLM latency) shows that LinguaArray solves up to 69.1% of instances and increases solved-instance counts by 105%--397% over the corresponding backends.