Large language models (LLMs) can often spot useful semantic structure in formal artifacts, yet their raw outputs cannot be trusted as proofs or solver decisions. We investigate a different approach: let an LLM guide a formal reasoning system through a narrow, solver‑verifiable interface. This idea is instantiated for quantified‑array SMT solving.
Modern instantiation‑based solvers may miss crucial ground terms and equalities because they are hidden behind auxiliary variables, axiom guards, or nested array terms. Empirically, many instances are driven by a small set of focal ground terms or constraints, reminiscent of backdoor sets in SAT solving.
We introduce LinguaArray, a framework that operates as follows:
- The LLM proposes a Semantic Focus Set containing a limited number of ground terms or constraints;
- A conventional SMT solver performs instantiation using this set, acting as the sole proof engine and certifying every LLM suggestion;
- If progress stalls within a bounded time, the system falls back to the backend solver to avoid regressions.
By feeding solver‑validated focal sets from the LLM, LinguaArray markedly expands solving capability, handling satisfiable and unsatisfiable instances that the backend alone cannot resolve. Evaluation on 1,015 SMT‑LIB benchmarks across five logics (1200 s timeout, including LLM latency) shows a solving rate up to 69.1%, representing a 105%–397% increase in solved instances over the respective backends.
Review: This work highlights the synergistic potential of combining LLMs’ semantic intuition with the rigor of traditional formal tools. By restricting LLM contributions to a verifiable focus set, it preserves soundness while substantially boosting SMT solving performance, especially for quantified array problems.