Verifiable LLM-Guided Focal SMT Solving for Quantified Arrays

1 Introduction

• Quantified array solving can stall when key indexes and relationships are obscured by quantifiers and complex array operations, leaving solvers with insufficient instantiations.In realistic formulas, witness terms may be buried under auxiliary definitions or appear as array-valued terms.Source: §1 · p. 2
• The paper frames the central challenge as choosing proof-relevant semantic focus points, which fixed syntactic triggers do not reliably recover from real-world formulas.Its contribution summary reports 105%–397% improvements over state-of-the-art solvers.Source: §1 · p. 2
• LinguaArray uses LLM-proposed Semantic Focus Sets in two branches: instantiation tuples guide UNSAT reasoning, while salient constraints guide SAT model construction.The backend validates candidates and certifies results; LLM interaction is time-bounded, with fallback to the original formula.Source: §1 · p. 2
• 69.1% of 1015 instances were solved with Z3 and LinguaArray, versus 13.9% with Z3 alone; CVC5 results were 64.9% versus 31.6%.The evaluation covered five logics with a 1200-second end-to-end timeout, including LLM latency.Source: §1 · p. 2

2.1 Quantified Arrays in SMT

• ArraysEx models arrays with index and element sorts, read and update operations, and universally quantified read-over-write axioms; quantified array formulas extend array formulas with quantifiers.For array disequalities, extensionality can be instantiated with a witness index; a quantified contradiction may likewise require instantiating at a witness index.Source: §2.1 · p. 3

2.2 Solving Quantified Array Formulas

• SMT solvers commonly reduce quantified formulas to ground instances using E-matching or MBQI, but there is generally no complete decision procedure across theories.E-matching uses trigger matches against ground terms; MBQI generates an instance from a counterexample witness in a candidate model.Source: §2.2 · p. 3

2.3 LLMs for Semantic Guidance

• LLMs can provide semantic insights and hypotheses in hybrid formal systems, while symbolic systems handle logical correctness and verification.Prompt design is described as important to eliciting desired LLM behavior.Source: §2.3 · p. 4

3.1 Motivating Example

• A 2D-array example motivates semantic focusing: cases based on whether i equals j expose how the formula can be simplified or shown unsatisfiable.The LLM proposes semantically motivated candidates, and the solver checks them using its standard procedure.Source: §3.1 · p. 4

3.2 Framework Overview

• The framework preprocesses formulas and asks the LLM for finite focus sets that identify where the solver should direct its reasoning.IFS terms and CFS constraints must use formula symbols and satisfy the relevant sort or construction requirements.Source: §3.2 · p. 5

3.3 Dual-Branch Reasoning

• For UNSAT, an Instantiation Focus Set supplies finite ground consequences; for SAT, a Constraint Focus Set adds assumptions that guide model construction.The UNSAT branch is sound because the finite instances are consequences of the formula; a SAT result under CFS constraints transfers to the original formula.Source: §3.3 · pp. 5–6

3.4 Feedback-Driven Refinement

• When guided solving stalls, solver feedback identifies arbitrary array assignments, unconstrained guards, or failed constraints for later LLM proposals.Rounds continue until a result is certified or the budget expires; the system then runs the baseline solver with the remaining time.Source: §3.4 · p. 6

3.5 LLM Interaction

• Each LLM query includes the formula, signature information, current focus set, and prior feedback; invalid or ill-typed proposals are rejected.Accepted proposals are canonicalized and deduplicated.Source: §3.5 · p. 6

3.6 Correctness Summary

• All returned results are solver-validated, and implication checks prevent a SAT-branch strengthening from producing a spurious UNSAT result.If guided attempts exhaust their budgets, the framework invokes the baseline solver directly.Source: §3.6 · p. 6, §3.3 · p. 6

4.1 Benchmarks

• The benchmark comprises 1015 SMT-LIB instances across ALIA, ABV, ABVFP, ABVFPLRA, and ANIA, sampled with a fixed seed where a logic exceeds 400 instances.Experiments use Z3 and CVC5 backends, two LLMs, and a 1200-second timeout including LLM latency; the default is 10 iterations.Source: §4.1 · p. 7, §4.2 · p. 7
• The study samples all instances for logics with fewer than 400 and uniformly samples 400 otherwise, yielding its five-logic benchmark.The timeout includes LLM latency, and the default configuration runs 10 iterations with both branches each round.Source: §4.1 · p. 7, §4.2 · p. 7

4.2 Experimental Setup

• Evaluation uses Z3 and CVC5, DeepSeek-V3.2 and Gemini-3-Flash, and identical hardware and software configurations for comparisons.CVC5 uses a tuned baseline and also reports its portfolio-based SMT-COMP 2025 configuration.Source: §4.2 · p. 7

4.3 RQ1: Overall Effectiveness

• 69.06% success rate: LINGUAARRAY(Z3) solves 701 instances, compared with 141 for Z3 alone, under the same 1200-second end-to-end timeout.LINGUAARRAY(CVC5) reaches 64.93%, improving 105% over its base solver.Source: Table 1 · p. 7, §4.3 · p. 8
• LINGUAARRAY(Z3) solves 256 instances outside the 623-instance virtual-best union of Z3, CVC5-COMP, and 20 CVC5 configurations.Harness-only variants solve 143 and 322 instances, while randomized proposers solve 436 and 445; Z3 also errors on all ABVFP and ABVFPLRA instances.Source: §4.3 · p. 8

4.4 RQ2: Impact of Different LLMs

• All three evaluated LLMs improve over baselines, but long reasoning-model outputs constrain iterations while concise Gemini outputs allow more refinement.The virtual-best results solve 775 instances for Z3 and 747 for CVC5, exceeding the best single LLM by 74 and 80 instances, respectively.Source: §4.4 · p. 8, Figure 2 · p. 8

4.5 RQ3: Effect of Iteration Budget

• 50.1% success rate after one iteration for Z3 using DeepSeek-Chat, versus the 13.9% baseline; most gains arrive within three iterations and later returns diminish.Gemini-3-Flash performs better in the first round, while DeepSeek-Chat improves more steadily across rounds.Source: §4.5 · p. 9

4.6 Discussion

• The authors report that deepest theory interactions remain formula-complexity bound, and LLM inference quality can produce ineffective proposals and overhead.They report three DeepSeek-V4-Flash runs with Z3 solving 689.7 ± 4.0 instances on average, with 602 solved in every run.Source: §4.6 · p. 9

Related work

• Quantifier-instantiation methods include counterexample-guided enumeration, QSMA’s abstraction-refinement loop, and the decidable Array Property Fragment; formulas outside that fragment typically need heuristic guidance.The Array Property Fragment restricts quantifiers to arithmetic index guards and value constraints.Source: §5 · p. 9
• Learning-based SMT work guides quantifier selection, ranks candidate ground terms, or chooses which generated instances reach the ground solver.AquaForte uses LLMs to synthesize complete function definitions for solver verification, primarily targeting SAT with limited UNSAT improvement.Source: §5 · p. 9
• LinguaArray proposes local focus sets rather than complete candidate solutions, using IFS over-approximations for UNSAT and CFS strengthening for SAT with implication checks.The framework uses solver-certified reasoning in both directions.Source: §5 · p. 10

6 Conclusion

• LINGUAARRAY uses Instantiation Focus Sets to guide UNSAT proofs and Constraint Focus Sets to guide SAT model construction, with the solver verifying all results.The framework presents Semantic Focus Sets as an interface between LLM reasoning and SMT solver certification.Source: §6 · p. 10
• Solve rates rise from less than 32% to approximately 70%, with reported improvements of 397% over Z3 and 105% over CVC5.The framework's effectiveness varies with the LLM model and problem characteristics, and its adaptability to broader, more complex theories is limited.Source: §6 · p. 10
• Future work includes extending the framework beyond arrays, incorporating uninterpreted functions, and developing more unified focus-set specifications.The paper also identifies learned refinement strategies and tighter coupling with solver internals as possible directions.Source: §6 · p. 10

A Detailed Algorithm

• The algorithm iterates through UNSAT and SAT branches, using feedback from unsuccessful solver calls to refine later LLM proposals.It falls back to the backend solver with the remaining timeout after the iterations.Source: A Detailed Algorithm · p. 13

B SMT Solver Backends and Configurations

• Z3 uses its default configuration, while the CVC5 baseline is tuned for quantified formulas and theory reasoning; a separate SMT-COMP portfolio configuration is also evaluated.The CVC5 options include model-based quantifier instantiation, finite model finding, enumerative instantiation, and experimental array and floating-point support.Source: B SMT Solver Backends and Configurations · pp. 13–14

C.1 Flag glossary

• Table 2 is a glossary of components and their corresponding CVC5 flags.The supplied passage identifies the table's scope but does not give its entries.Source: Table 2 · p. 14

C.2 Base setting (fmf/arr/fp)

• The CVC5 parameter study selects fmf_arr_fp as its default backbone because enabling fmf, arr, and fp together achieves the best overall solved count.The reported comparison is in Table 3.Source: §C.2 · p. 14, Table 3 · p. 14

C.3 Component ablation

• The ablation covers all 16 combinations of mbqi, enum, cegqi, and sygus instantiation.Configuration names indicate enabled components; disabled components use the corresponding no-options.Source: §C.3 · p. 15
• fmf_arr_fp_mbqi_enum attains the largest solved count among the tested configurations.The passage identifies it as the best-performing configuration.Source: §C.3 · p. 15
• Table 4 summarizes the ablation results across those component combinations.The caption identifies the table as ablation results.Source: Table 4 · p. 15, §C.3 · p. 15

D Runtime Analysis

• Table 5 reports runtime statistics corresponding to Table 1's results.Unsolved instances are counted as 1200 seconds.Source: Table 5 · p. 15, D Runtime Analysis · p. 15
• LINGUAARRAY solves more instances within the shared end-to-end budget, despite higher average time on solved instances than the baseline solvers.Its extra cost comes from LLM calls and repeated solver checks; the passage says this cost is useful when guidance helps avoid long unsuccessful searches.Source: D Runtime Analysis · p. 15
• Baseline-solved instances usually finish within a few seconds or run until the 1200-second timeout.The runtime passage describes these two baseline behaviors as the context for LINGUAARRAY's higher average runtime on solved instances.Source: D Runtime Analysis · p. 15

D.1 Run-to-Run Stability

• The three runs solve 685, 692, and 692 instances, for a mean of 689.7 and sample standard deviation of 4.0 (67.95% success rate).The runs use the same 1015 instances, non-reasoning mode, temperature 0, 10 refinement rounds, and a 1200-second timeout.Source: §D.1 · pp. 15–16
• 602 instances are solved in all three runs, while 762 are solved in at least one run.Source: §D.1 · p. 16
• For the 602 consistently solved instances, average end-to-end runtime is 44.6 seconds; individual runtimes remain variable, with median coefficient of variation 61%.The median per-instance runtime standard deviation is 18.2 seconds.Source: §D.1 · p. 16

E Non-LLM Proposer Baselines

• The randomized proposer samples typed ground terms for IFS and constructs atomic constraints for CFS, retaining validation, certification, refinement, and fallback under the same 1200-second budget.The harness-only baseline uses empty focus sets while retaining preprocessing, dual-branch execution, validation, and fallback.Source: E Non-LLM Proposer Baselines · p. 16

F LLM Details

• The implementation documents prompt templates, output schemas, response parsing, proposal validation, and cross-round feedback.Source: F LLM Details · p. 16

F.1 Prompt Format

• Each branch receives the preprocessed formula and its objective; SAT requests ground constraints, while UNSAT requests witness terms for eligible quantified variables.The SAT prompt forbids new symbols and bound variables and favors small concrete constraints; witness terms must pass validation.Source: §F.1 · pp. 16–17

F.2 Response Parsing

• When direct JSON parsing fails, recovery removes reasoning tags, extracts a fenced block, repairs simple formatting, or uses the longest parseable prefix; unrecoverable output is empty.The system does not issue another LLM call solely to repair formatting errors.Source: §F.2 · p. 17

F.3 Proposal Validation

• Proposals are checked before use: constraints must parse and use allowed symbols, while instantiations must match an existing quantifier and assign well-typed terms to every bound variable.Invalid items are discarded rather than rewritten.Source: §F.3 · p. 17

F.4 Cross-Round Feedback

• Uncertified proposals are fed back in later rounds, with separate histories for SAT constraints and UNSAT instantiations; feedback is prompt context, not evidence of satisfiability.Source: §F.4 · p. 18

• 13.2% of DeepSeek-V3.2 IFS proposals are invalid, versus 1.65% of CFS proposals; Gemini’s invalid rates are 10.2% for IFS and 3.7% for CFS.For DeepSeek-V3.2 IFS, 12.5% have parsing or type errors and 0.7% omit bound variables.Source: §F.5 · p. 18
• 59.5% of CFS items and 65.1% of IFS items in later rounds have appeared in previous rounds; such repetitions may still help when solving requires combinations of proposals.Source: §F.5 · p. 18

• The checklist answers yes that the abstract and introduction accurately reflect the paper’s contributions and scope, and that theoretical results include proofs.It reports that both Theorem 1 and Theorem 2 have proofs.Source: NeurIPS Paper Checklist · pp. 19–20
• The authors report that detailed configurations and complete code are available, and that the experimental setting is described; the LLMs are fixed black-box proposal generators without model training.Source: NeurIPS Paper Checklist · pp. 20–21
• The authors acknowledge that they provide no error bars, confidence intervals, or formal significance tests, despite using deterministic decoding and judging observed gains large and consistent.They identify statistical uncertainty analysis as possible future work.Source: NeurIPS Paper Checklist · p. 21
• The checklist notes that the paper discusses positive application domains but has no dedicated discussion of negative societal impacts; it also reports limitations in the Discussion and Conclusion.Source: NeurIPS Paper Checklist · pp. 19, 22
• The checklist reports that existing assets are credited and new assets documented, and that the paper declares LLM use because models generate focus sets for SMT solving.Source: NeurIPS Paper Checklist · pp. 23–25