Organizations: Laboratory of Parallel Software and Computational Science, ISCAS, Beijing, China · University of Chinese Academy of Sciences, Beijing, China · SKLCS and Key Laboratory of System Software, ISCAS, Beijing, China
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.
Figures & tables
Figure 1: Overview of LinguaArray.
ABV (400)
ABVFP (60)
ABVFPLRA (77)
ALIA (400)
ANIA (78)
Overall (1015)
Method
SAT
UNSAT
SR
SAT
UNSAT
SR
SAT
UNSAT
SR
SAT
UNSAT
SR
SAT
UNSAT
SR
Solved
SR
Z3 (Baseline)
34
11
11.25%
0
0
0.00%
0
0
0.00%
51
8
14.75%
28
9
47.44%
141
13.89%
CVC5 (Baseline)
93
15
27.00%
31
3
56.67%
45
1
59.74%
84
15
24.75%
27
7
43.59%
321
31.63%
CVC5 -COMP
130
82
53.00%
37
3
66.67%
47
2
63.64%
15
66
20.25%
4
2
7.69%
388
38.23%
Harness-only (Z3)
34
10
11.00%
0
0
0.00%
0
0
0.00%
52
8
15.00%
28
11
50.00%
143
14.09%
Randomized (Z3)
160
19
44.75%
0
0
0.00%
0
0
0.00%
181
17
49.50%
45
14
75.64%
436
42.96%
Table 1: Results on five logics with a 1200s timeout (including LLM latency). LinguaArray uses DeepSeek-V3.2-chat. For each logic, we report #SAT / #UNSAT and success rate (SR).
Figure 2: Comparison of solved instances across settings: (a) different LLMs; (b) iteration budget under a 1200s timeout. Each point in (b) reports cumulative instances solved within the given budget.
Appendix figures & tables4 assets
Supplementary material from the paper’s appendix.
Appendix
Term
CVC5 parameters
fmf
--finite-model-find
arr
--arrays-exp
fp
--fp-exp
mbqi
--mbqi
enum
--enum-inst
cegqi
--cegqi
Appendix
Table 2: Glossary of components and the corresponding CVC5 flags.
Configuration
SAT
UNSAT
Total
baseline
36
24
60
fmf
50
15
65
fmf_arr
51
15
66
fmf_arr_fp
51
15
66
Appendix
Table 3: Effect of base parameters.
Configuration
SAT
UNSAT
Total
fmf_arr_fp_mbqi_enum
280
41
321
fmf_arr_fp_mbqi
271
32
303
fmf_arr_fp_mbqi_enum_cegqi
260
39
299
fmf_arr_fp_mbqi_cegqi
249
33
282
fmf_arr_fp_enum_cegqi
53
136
189
fmf_arr_fp_enum_cegqi_sygus
137
49
186
Appendix
Table 4: Ablation results.
Method
Avg. total time
#Solved
Avg. time (solved only)
Z3 (Baseline)
1033.41s
141
0.79s
CVC5 (Baseline)
820.75s
321
0.80s
LinguaArray(Z3)
424.15s
701
76.63s
LinguaArray(CVC5)
469.91s
659
75.51s
Appendix
Table 5: Runtime statistics corresponding to the results in Table 1 . Unsolved instances are counted as 1200 seconds.
Formal tools such as SAT and SMT solvers are increasingly embedded in language model reasoning pipelines when a safety or security critical question can be formulated in logic. Unlike chain of thought whose steps are sampled from the model distribution without formal guarantee, a solver produces a sound and independently verifiable answer. However, the soundness guarantee can be lost in the interaction between the solver and the model. The hybrid pipeline has three components: formalizing the question, deciding it, and narrating the result. Prior work has studied the formalization and decision, but not narration, which is the step that turns a formal tool's output into the user answer. To fill the narration gap, we first model the LLM-solver loop as a verified decision procedure. We further evaluate five open-sourced models under prompt injection, and we find certificate gating makes the solver verdict sound, while an adversary can invert a verified conclusion across phrasings and channels. We study the mitigation through hardened prompt that reduces injection significantly but cannot eliminate it and still suffers under adaptive attack. Combining the formal analysis and empirical studies, we show in the LLM-solver loop, robustness does not reach to the answer that the user finally reads.
Zunchen Huang, Songgaojun Deng
Centrum Wiskunde & Informatica, Amsterdam, The Netherlands · Eindhoven University of Technology, Eindhoven, The Netherlands
Large language models (LLMs) have achieved strong performance in mathematical and logical reasoning, yet they still suffer from the curse of complexity and struggle as problem difficulty increases with the number of constraint interactions and the size of the search space. In contrast, satisfiability solvers such as Z3 provide scalable and verifiable reasoning through constraint solving under formal theories, but lack the flexibility to interpret natural-language problem descriptions. In this work, we propose SAT-RL, a reinforcement-learning (RL) framework that trains LLMs to interact with symbolic solvers through multi-turn tool execution. SAT-RL leverages synthetic data generation with verifiable solutions, supervised warm-up on solver-augmented traces, and solver-grounded reinforcement learning with tool-aware rewards. Experiments show that SAT-RL substantially improves symbolic reasoning with tools on both in-domain and out-of-domain logic tasks. Our code is available on https://github.com/sunjia72/SAT-RL.
We introduce Sequent-Prover, a family of verifier-using language-model agents, and the post-training framework that produces them. Agents reason in an executable SMT-LIB scratchpad: they write complete SMT-LIB programs, query Z3 across turns, inspect solver feedback, repair formalizations, and terminate with an explicit answer. Our recipe, verifier-conditioned trajectory distillation, bootstraps from a noisy teacher proposal policy by sampling multi-turn trajectories, retaining the successful tail that is correct, non-trivial, grounded, and executable, then applying supervised fine-tuning and trajectory-level preference optimization. Because solver success alone does not guarantee semantic faithfulness, we evaluate task accuracy, k-sample reliability, and SMT program quality. Across 37 benchmarks and 7,254 problems per model family, post-training raises the 4B model's per-attempt accuracy from 85.6% to 97.0% and four-sample all-correct reliability (pass^4}) from 64.1% to 91.7%. It also reduces average SMT calls from 4.10 to 2.52 and tokens per attempt from 18.97k to 12.72k. Sequent-Prover agents give answers backed by executable formal artifacts.
Debargha Ganguly, Weicong Chen, Mohsen Hariri +13
Case Western Reserve University · UT Austin · Microsoft Research