Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning

Debargha Ganguly; Weicong Chen; Mohsen Hariri; Vikash Singh; Sreehari Sankar; Shouren Wang; Wang Yang; Biyao Zhang

cs.CLOct 11, 2026

Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning

Authors: Debargha Ganguly, Weicong Chen, Mohsen Hariri, Vikash Singh, Sreehari Sankar, Shouren Wang, Wang Yang, Biyao Zhang, +8 more

Organizations: Case Western Reserve University · UT Austin · Microsoft Research

Abstract

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.

Figures & tables

Figure 1: A toy example showing how Sequent-Prover turns an underspecified commonsense claim into a grounded, checkable inconsistency.

Figure 2: Post-training, especially DPO, shifts the models from merely sampling correct answers toward more reliable solver-grounded proof behavior. Hatched bars show each base checkpoint and colored overlays show the tuned-model gain: avg@N measures per-sample correctness, pass^k measures consistency by requiring all sampled trajectories to be correct, mean grounding measures how much of the problem is represented in SMT, and vcr_unsat measures correct answers backed by non-trivial UNSAT/refutation certificates. The remaining panels show the mechanism behind the gains: tuned models more often drive Z3 to UNSAT verdicts, avoid trivial SMT calls, and obtain more verified progress per tool call and per reasoning turn.

Figure 3: Sequent-Prover overview. The agent formalizes a task in SMT-LIB, calls Z3 over several turns, and uses solver feedback until it finishes. Successful trajectories train SFT, and preferred versus rejected trajectories train DPO.

Table 2: Performance transition and direct-comparison analyses for tuned checkpoints. In Table 2(a) , the three rates measure coverage gained on base-unsolved problems, conversion of partially correct problems to 4/4 correctness, and retention of already 4/4 problems. In Table 2(b) , metric deltas are macro-averages over shared datasets; DPO-only and SFT-only count paired problems solved by one tuned checkpoint and not the other.

Method	$K$	pass@ $K$ $\uparrow$	pass^K $\uparrow$	Tokens $\downarrow$
Base	4	0.848	0.395	110.9k
Base	16	0.911	0.139	443.7k
Base + self-refine	4	0.928	0.572	219.5k
Post-trained 4B	1	0.869	0.869	16.7k
Post-trained 4B	4	0.948	0.743	66.9k

Table 3: Post-training versus test-time sampling (4B, 180 held-out problems from six families). Tokens are per problem. Shaded rows are post-trained. Full results are in Table 16 .

Checkpoint	avg@ $N$ $\uparrow$	pass@4 $\uparrow$	pass^4 $\uparrow$	Stab. $\uparrow$
SFT (ours)	0.585	0.715	0.409	0.572
DPO (ours)	0.603	0.718	0.439	0.611
Answer-only SFT	0.407	0.654	0.126	0.193
Solver-verdict SFT	0.583	0.712	0.403	0.566
Continued SFT	0.591	0.700	0.440	0.629
Gold/Silver/Rej. DPO	0.586	0.699	0.419	0.599

Table 4: Data-selection ablations for 4B on five hard held-out benchmarks.

Table 5: Efficiency and SMT-scratchpad diagnostics. In Table 5(a) , Iter. is the average number of model iterations, SMT calls is the average number of solver invocations, Tokens is the average token count per problem attempt, Tok./correct normalizes token use by correct-attempt rate, and First VC iter. is the mean iteration index of the first verified-correct SMT signal. In Table 5(b) , Error and no-verdict measure unusable calls, UNSAT is the share of calls returning an UNSAT verdict, UNSAT

\mid

correct restricts to calls inside correct attempts, and Calls is total solver calls.

Fam	Dataset	Base pass^4	DPO pass^4	$\Delta$
4B	ProofWriter	0.074	0.926	+0.852
4B	ZebraLogic	0.120	0.715	+0.595
4B	RuleTaker	0.395	0.985	+0.590
4B	AR-LSAT	0.035	0.560	+0.525
4B	ProntoQA	0.445	0.955	+0.510
4B	SpartQA-MC	0.250	0.745	+0.495

Table 6: Largest representative dataset-level DPO gains on pass^4 within each model family.

Comparison	Small	Large	Tie	Win $\uparrow$
4B SFT / 9B Base	816	518	5,920	0.612
4B DPO / 9B Base	840	361	6,053	0.699
9B SFT / 27B Base	73	490	6,691	0.130
9B DPO / 27B Base	90	420	6,744	0.176
4B DPO / 27B Base	84	532	6,638	0.136

Table 7: Cross-scale paired comparison. Small and Large count paired problems where the smaller tuned checkpoint or larger base checkpoint has more correct attempts out of four. Win is the smaller tuned checkpoint’s non-tie win rate.

Appendix figures & tables11 assets

Supplementary material from the paper’s appendix.

Appendix

Dataset	pass@3	pass^3
AR-LSAT	0.727	0.484
FOLIO	0.853	0.738
ZebraLogic	0.999	0.901

Appendix

Table 8: Teacher (DeepSeek-v4 Flash) answer accuracy with three rollouts per training problem.

Attribute	Definition
any non trivial	$\bigvee_{i}\neg\,\texttt{is trivial}(z_{x}^{(r,i)})$
any grounded	$\bigvee_{i}\left(\texttt{grounding}(z_{x}^{(r,i)},x)\geq\lambda_{\mathrm{gnd}}\right)$
any real verdict	$\bigvee_{i}\left(\texttt{sat result}_{i}\in\{\textsc{sat},\textsc{unsat},\textsc{unknown}\}\right)$
any unsat	$\bigvee_{i}\left(\texttt{sat result}_{i}=\textsc{unsat}\right)$
first pass valid	$\texttt{sat result}_{1}\in\{\textsc{sat},\textsc{unsat},\textsc{unknown}\}$
max grounding	$\max_{i}\texttt{grounding}(z_{x}^{(r,i)},x)$

Appendix

Table 9: Per-attempt structural attributes computed from the sequence of SMT calls

(z_{x}^{(r,1)},\ldots,z_{x}^{(r,S_{x}^{(r)})})

in trace

\tau_{x}^{(r)}

. The grounding threshold is

\lambda_{\mathrm{gnd}}=0.25

. is trivial is the predicate defined in § B.3.2 .

Comparison	Shared	avg@ $N$	pass@4	pass^4	maj@4	AUC@4	Cons.
Qwen-4B-DPO $-$ Gemma-4B	33	+0.647	+0.524	+0.640	+0.720	+0.591	+0.568
Qwen-27B-DPO $-$ GPT-OSS-20B	35	+0.326	+0.067	+0.648	+0.408	+0.151	+0.699
Qwen-9B-DPO $-$ GPT-OSS-20B	33	+0.287	+0.053	+0.567	+0.372	+0.130	+0.625
Qwen-27B-DPO $-$ GPT-OSS-120B	35	+0.027	+0.021	+0.036	+0.028	+0.023	+0.017
Qwen-9B-DPO $-$ GPT-OSS-120B	33	$-$ 0.010	+0.006	$-$ 0.039	$-$ 0.008	+0.002	$-$ 0.054

Appendix

Table 10: Macro-averaged correctness deltas against external open-weight baselines. Deltas are computed over shared canonical datasets and are reported as Qwen-DPO minus the external model. Cons. is pass^4 /pass@4. Red marks a deficit.

Comparison	Sound.	Recov.	VCR	VCR-U	FP-Z3	Triv. SMT $\downarrow$	Ground.
Qwen-4B-DPO $-$ Gemma-4B	+0.444	+0.490	+0.615	+0.399	+0.164	$-$ 0.016	+0.399
Qwen-27B-DPO $-$ GPT-OSS-20B	+0.206	+0.181	+0.487	+0.345	+0.034	$-$ 0.032	+0.329
Qwen-9B-DPO $-$ GPT-OSS-20B	+0.172	+0.152	+0.487	+0.321	+0.023	$-$ 0.031	+0.353
Qwen-27B-DPO $-$ GPT-OSS-120B	$-$ 0.010	$-$ 0.020	+0.341	+0.196	+0.004	$-$ 0.011	+0.274
Qwen-9B-DPO $-$ GPT-OSS-120B	$-$ 0.036	$-$ 0.032	+0.349	+0.179	$-$ 0.008	$-$ 0.011	+0.299

Appendix

Table 11: Macro-averaged verifier-use deltas. Sound. is

P(\mathrm{correct}\mid\mathrm{finish})

; Recov. is correctness after an initial SMT error; VCR is verified-correct rate; VCR-U additionally requires an UNSAT verdict; FP-Z3 is first-pass Z3 validity; Triv. SMT is trivial-SMT rate, where lower is better; Ground. is mean SMT grounding. Negative entries are green where lower is better and red otherwise.

Comparison	avg@ $N$	pass@4	pass^4	maj@4	FP-Z3	Sound.	Recov.
Qwen-4B-DPO $-$ Gemma-4B	32/0/1	32/1/0	33/0/0	33/0/0	33/0/0	27/1/5	27/1/5
Qwen-27B-DPO $-$ GPT-OSS-20B	35/0/0	33/1/1	35/0/0	35/0/0	35/0/0	29/1/5	27/2/6
Qwen-9B-DPO $-$ GPT-OSS-20B	33/0/0	31/1/1	33/0/0	33/0/0	29/3/1	26/2/5	23/5/5
Qwen-27B-DPO $-$ GPT-OSS-120B	28/7/0	23/9/3	24/6/5	25/9/1	22/9/4	16/14/5	14/15/6
Qwen-9B-DPO $-$ GPT-OSS-120B	16/17/0	22/8/3	6/26/1	15/16/2	3/29/1	8/20/5	6/21/6

Appendix

Table 12: Per-dataset win/loss/tie counts. Each entry is W/L/T after metric polarity is applied. Higher is better for all displayed metrics.

Category	4B $-$ Gemma	27B $-$ OSS20	9B $-$ OSS20	27B $-$ OSS120	9B $-$ OSS120
AGIEval	+0.795	+0.376	+0.331	+0.069	+0.024
Arithmetic	+0.686	+0.304	+0.283	+0.021	+0.001
Free-form QA	+0.611	+0.363	+0.312	+0.002	$-$ 0.049
Hard reasoning	+0.659	+0.346	+0.317	+0.035	$-$ 0.003
NLI/MCQ	+0.647	+0.346	+0.301	+0.044	+0.003
Other	+0.816	+0.307	+0.285	$-$ 0.008	$-$ 0.022

Appendix

Table 13: Mean avg@

N

delta by dataset category. Values are macro-averages over shared canonical datasets in each category.

Category	Bench.	Problems	%
Hard reasoning	6	1,054	14.53
Arithmetic	6	1,200	16.54
Spatial	3	600	8.27
NLI/MCQ	12	2,400	33.09
Free-form QA	4	800	11.03
Other	2	400	5.51

Appendix

Table 14: Composition of the 37-benchmark evaluation pool.

		avg@ $N$ $\uparrow$			pass^4 $\uparrow$
Family	Category	Base	SFT	DPO	Base	SFT	DPO
4B	Hard reasoning	0.630	0.920	0.931	0.346	0.820	0.839
	Arithmetic	0.899	0.984	0.987	0.691	0.952	0.964
	Spatial	0.735	0.867	0.895	0.372	0.670	0.708
	NLI/MCQ	0.899	0.977	0.985	0.688	0.926	0.953
	Free-form QA	0.956	0.988	0.992	0.841	0.960	0.971

Appendix

Table 15: Per-category results for Base, SFT , and DPO checkpoints. Values are micro-averages over the problems in each category.

Method	$K$	Accuracy [95% CI] $\uparrow$	pass@ $K$ $\uparrow$	pass^K $\uparrow$	Stab. $\uparrow$	Tokens/problem $\downarrow$	Cost $\downarrow$
Base + self-consistency	1	0.657 [0.623, 0.689]	0.657	0.657	1.000	27,729	1.7 $\times$
Base + self-consistency	2	0.657 [0.623, 0.689]	0.780	0.533	0.683	55,458	3.3 $\times$
Base + self-consistency	4	0.657 [0.623, 0.689]	0.848	0.395	0.466	110,915	6.6 $\times$
Base + self-consistency	8	0.657 [0.622, 0.689]	0.887	0.257	0.290	221,831	13.3 $\times$
Base + self-consistency	16	0.657 [0.623, 0.689]	0.911	0.139	0.152	443,662	26.5 $\times$
Base + decomposed	4	0.590 [0.550, 0.629]	0.828	0.267	0.322	117,070	7.0 $\times$

Appendix

Table 16: Post-training versus test-time sampling on 180 held-out problems from six benchmark families. Cost is token use relative to the post-trained model at

K=1

Family	SFT $-$ Base	DPO $-$ Base
4B	+0.074	+0.081
9B	+0.051	+0.051
27B	+0.039	+0.036

Appendix

Table 17: Change in mean grounding after removing SMT comments.

	Across traj.	Within traj.
Comparison	$\Delta$ [95% CI] $\downarrow$	First–last $\downarrow$	Adjacent $\downarrow$
4B Base $\to$ SFT	$-0.023$ [ $-0.025$ , $-0.021$ ]	$-0.029$	$-0.011$
4B Base $\to$ DPO	$-0.019$ [ $-0.021$ , $-0.016$ ]	$-0.027$	$-0.008$
9B Base $\to$ SFT	$-0.019$ [ $-0.021$ , $-0.017$ ]	$-0.024$	$-0.010$
9B Base $\to$ DPO	$-0.016$ [ $-0.018$ , $-0.015$ ]	$-0.026$	$-0.010$
27B Base $\to$ SFT	$-0.008$ [ $-0.010$ , $-0.006$ ]	$-0.006$	$-0.005$

Appendix

Table 18: Paired change in structural (PCFG production) divergence over 1,382 tasks per comparison. Across-trajectory intervals use 4,000 bootstrap resamples, stratified by dataset. Within-trajectory columns are point estimates.

Explore similar work

SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner
Oct 6, 2026Hanchao Zhou, Jialei LiAutomated Theorem Proving Lean Theorem Proving
MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
May 26, 2026Jinzheng Li, Zeru Zhu, Yuanjie RenAutomated Theorem Proving Lean Theorem Proving
1Northeastern University · 2Stony Brook University · 3Massachusetts Institute of Technology
PrologMCP: A Standardized Prolog Tool Interface for LLM Agents
Jun 12, 2026Agnieszka Mensfelt, Adarsh Prabhakaran, Adrian Haret +2Logic Programming Symbolic Reasoning
Department of Computer Science, Royal Holloway, University of London, UK

Oct 6, 2026J/K move · Enter open · S save

SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner

Hanchao Zhou, Jialei Li

Automated Theorem Proving Lean Theorem Proving Efficient Language Model Reasoning

Open paper AskPDF arXiv

In proof assistants such as Lean, a generated proof must pass machine compilation checks, so evaluation needs no human scoring. Direct generation fails on multi-step numeric propositions: a proof is valid only if every content integer is correct, so the pass rate is bounded by the k-th power of the per-integer accuracy. Controlled corruption across 2,617 reference proofs confirms this power law. SCOPE (State-Conditioned Operator Planning and Execution) enforces the natural division of labor: the model plans over an operator vocabulary, a symbolic engine executes the numerics, and a compiler renders the proof. On a 218-problem suite it certifies 191/218 (87.6%) with a 135M backbone; the 7B DeepSeek-Prover-V1.5-RL certifies 18/218 at 27.5 times the tokens and 37.5 times the wall-clock, and DeepSeek-Prover-V2-7B certifies zero on a bidirectional dual suite. Multi-step thinking costs 6.12 discrete decision actions per problem and produces no natural-language thinking text. Replacing the lagged engine state in the decision frame with the current one lifts the pass rate from 117/218 to 191/218, while up-weighting the chain-end loss hurts. On the public Lean-Workbook library, 2,132 of 3,536 gradeable admissible problems certify (60.29%) with zero regression on the main suite. All readings come from a version-frozen review with independent rechecks and reverse verification. Restricting free generation and keeping decision-time information visible is a more direct route than enlarging the model.

Abstract

Explore similar work

SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving

PrologMCP: A Standardized Prolog Tool Interface for LLM Agents