Paper deep dive
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, Chaoda Song, Alexander Nemecek, Kai Ye, Osama Zafar, Erman Ayday, Joe Stubbs, Srinivasan Iyengar, Vipin Chaudhary
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2610.15258v1
- Canonical: https://arxiv.org/abs/2610.15258v1
Trouble viewing inline? Open PDF directly →
Full Text
124,636 characters extracted from source content.
Expand or collapse full text
Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning Debargha Ganguly1, Weicong Chen1, Mohsen Hariri1, Vikash Singh1, Sreehari Sankar1, Shouren Wang1, Van Yang1, Biyao Zhang1, Chaoda Song1, Alexander Nemecek1, Kai Ye1, Osama Zafar1, Erman Ayday1, Joe Stubbs2, Srinivasan Iyengar3, Vipin Chaudhary1 1Case Western Reserve University, 2UT Austin, 3Microsoft Research Sequent-Prover-4B,9B,27B proofofthought 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. 1 Introduction Large language models can produce fluent multi-step reasoning, but fluency is not executable evidence that a conclusion follows from the stated assumptions (Wei et al., 2022; Kojima et al., 2022; Turpin et al., 2023; Lanham et al., 2023). A natural alternative is to make reasoning checkable: translate an input into explicit assumptions, constraints, and claims, then verify the resulting obligation with a symbolic backend (Pan et al., 2023; Ye et al., 2023; Olausson et al., 2023; Ganguly et al., 2024). SMT solvers such as Z3 are especially attractive because SMT-LIB can encode logical entailment, arithmetic, datatypes, arrays, bit-vectors, and program constraints, while solver execution returns concrete feedback such as sat, unsat, countermodels, parser errors, and type errors (de Moura and Bjørner, 2008; Barrett and Tinelli, 2018; Barrett et al., 2025). Figure 1: A toy example showing how Sequent-Prover turns an underspecified commonsense claim into a grounded, checkable inconsistency. However, solver access alone does not make reasoning reliable. Recent work by Ganguly et al. (2026) shows that SMT-based autoformalization can improve premise-explicit reasoning but degrade performance when the generated artifact misrepresents the input. The core problem is the autoformalization gap: real tasks arrive as natural language, specifications, and informal intent, not as already-correct proof obligations. A solver checks only the artifact it receives; if the model omits a premise, reverses entailment, introduces inconsistent assumptions, or encodes a different problem, the solver may return a valid result for the wrong object. Reliable verifier use therefore requires models that construct grounded, non-vacuous, executable formalizations through multi-turn tool use. We introduce Sequent-Prover, a family of post-trained language models for SMT-verifiable reasoning. Rather than using the solver as a test-time wrapper (Ganguly et al., 2024; Singh et al., 2026; Feng et al., 2025), we use solver interaction as a training substrate: we sample candidate formalization traces, execute them with Z3, reject malformed or vacuous artifacts, and convert supported traces into supervised and preference data. Post-training turns inconsistent SMT tool use into more dependable multi-sample correctness and yields agents that write more grounded, non-trivial, executable SMT programs. In particular, we find that: 1. Post-training substantially improves SMT reasoning: models that previously achieved only inconsistent solver-aided success become more reliable under multi-sample evaluation. 2. Supervised fine-tuning improves proof discipline: tuned agents produce higher-quality SMT-LIB programs that are better grounded in the input, less vacuous, and structurally more consistent across samples. 3. Post-training strengthens more demanding proof strategies, including refutational reasoning, where agents increasingly formulate proof obligations by contradiction and correctly interpret the resulting unsat evidence. 4. Preference optimization with DPO further improves stability, grounding, proof quality, and efficiency beyond supervised fine-tuning: DPO-tuned agents solve problems earlier, with fewer tokens and fewer solver-interaction rounds per correct answer. 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. 2 Methodology Overview. We frame verifier-guided reasoning as success-conditioned policy bootstrapping. A teacher model need not be reliable on every rollout; it only needs a nonzero probability on trajectories that use the verifier correctly. Sampling the teacher in an SMT-LIB scratchpad exposes a sparse successful tail: rollouts that construct and revise executable formalizations, use Z3 feedback, and terminate with the correct answer. We condition on this tail so the student learns verifier-mediated search behavior that the teacher produces only sporadically. Our method, verifier-conditioned trajectory distillation, has three stages. First, we sample teacher trajectories under the same z3-solve/finish interface used at evaluation time. Second, we curate them with an acceptance predicate that combines answer correctness with executable scratchpad evidence: solver execution, non-triviality, grounding, and protocol completion. Third, we train by supervised fine-tuning on accepted traces and by DPO on trajectory-level pairs that contrast accepted traces with rejected or weakly supported ones. The resulting policy amortizes rare successful verifier-mediated searches into more reliable inference. 2.1 Problem Formulation Each task instance is x=(,q)x=(C,q), where =p1,…,pmC=\p_1,…,p_m\ contains the natural-language premises, program fragments, or specifications, and q is the query. The model must produce a final answer y matching y⋆y and, when possible, support it with an executable SMT-LIB artifact. We use ϕφ for the model’s formalization map: ϕ _C encodes assumptions from C, and ϕc _c encodes a candidate claim c. Context consistency is checked by SAT(ϕ)SAT( _C); claim compatibility by SAT(ϕ∧ϕc)SAT( _C _c); and entailment by refutation, requiring SAT(ϕ)=trueSAT( _C)=true and SAT(ϕ∧¬ϕc)=falseSAT( _C _c)=false. Thus, a claim is entailed only when the formalized context is satisfiable and the claim’s negation is inconsistent with it, making unsat the proof signal for refutational entailment. 2.2 The SMT Scratchpad Interface A central design choice is to expose the SMT-LIB backend from Ganguly et al. (2024) as an executable scratchpad: a workspace in which the model constructs, tests, and revises formal artifacts across turns. We define the tool environment as ℰSMT=(,),=z3-solve,finish.E_SMT=(A,O),A=\ z3-solve, finish\. The z3-solve action executes a self-contained SMT-LIB script with declarations and a check-sat command. A single action can express context checks, candidate-claim tests, counterexample searches, model construction, semantic-equivalence checks, or refutational proof obligations. Z3 returns an observation in O, such as sat, unsat, unknown, a model, a parser/type error, or a timeout, which is appended to the interaction history. The finish action is separate from scratchpad execution: it terminates the episode with a final answer after the model judges that the accumulated solver feedback is sufficient. A trajectory is therefore a multi-turn record τ=(m1,o1,…,mT,oT),τ=(m_1,o_1,…,m_T,o_T), where model messages may contain natural-language reasoning, SMT-LIB code, tool calls, repairs, or the final answer, and the policy πθ _θ maps the current history to the next token or tool action. We do not require every scratchpad call to constitute a complete proof; early calls may be exploratory or diagnostic. However, accepted training traces must contain meaningful scratchpad evidence: at least one Z3 invocation with an executable, non-trivial, input-grounded SMT-LIB program that obtains a real solver verdict. 2.3 Verifier Feedback and Trace Semantics Each z3-solve call converts a generated SMT-LIB artifact into a structured observation that the agent can use to interpret, repair, or commit to a formalization. We write SAT(ψ)∈sat,unsat,unknownSAT(ψ)∈\ sat, unsat, unknown\ for the Z3 verdict on a formula or script ψ, and treat parser errors, type errors, timeouts, malformed scripts, and solver failures as unresolved observations. For a candidate claim cic_i with context encoding ϕ _C and claim encoding ϕci _c_i, the verifier first separates inconsistent contexts from meaningful claim statuses: if SAT(ϕ)=unsatSAT( _C)= unsat, the artifact receives the inconsistent-context status σI _I. Otherwise, when SAT(ϕ)=satSAT( _C)= sat, the claim is entailed (σE _E) if SAT(ϕ∧¬ϕci)=unsatSAT( _C _c_i)= unsat, contradictory (σC _C) if SAT(ϕ∧ϕci)=unsatSAT( _C _c_i)= unsat, and possible but not forced (σP _P) if both SAT(ϕ∧ϕci)=satSAT( _C _c_i)= sat and SAT(ϕ∧¬ϕci)=satSAT( _C _c_i)= sat. We use σU _U for states in which no semantic status can be assigned, including unknown, timeout, solver failure, or parse/type errors. The same scratchpad also supports comparison between alternative formalizations: given formulas ϕa _a and ϕb _b over a shared signature and background theory Σ , they are equivalent when SATΣ(¬(ϕa↔ϕb))=unsatSAT_ ( ( _a _b))= unsat. Solver feedback is richer than a binary success signal: sat can expose a witness or countermodel, unsat provides refutational evidence, and execution errors identify artifacts that must be repaired. When constraints are labeled or instrumented, this feedback can be augmented with unsat cores or approximate correction sets, but the main training signal comes from executable SMT-LIB interaction and solver feedback. Teacher Rollout Generation. For each training instance x=(,q)x=(C,q), we sample KTK_T trajectories from a teacher proposal model MTM_T under the same SMT-scratchpad interface used at evaluation time. The teacher is given only the problem instance x, not the target answer y⋆y ; the target is reserved for offline curation. Thus, the teacher is not an oracle annotator, but a stochastic proposal distribution pT(τ∣x)p_T(τ x) over executable reasoning traces. Each sampled trajectory is stored as τ=(x,hT,y^,μ),hT=(m1,o1,…,mT,oT),τ=(x,h_T, y,μ),h_T=(m_1,o_1,…,m_T,o_T), where hTh_T is the interaction transcript, y y is the answer emitted through finish, and μ records protocol metadata such as solver-call counts, solver verdicts, execution errors, token usage, and termination status. These rollouts provide the candidate pool from which verifier-conditioned trace curation selects training examples. Verifier-Conditioned Trace Curation. The offline curator converts teacher rollouts into training data by applying a trajectory-level acceptance predicate A(x,y⋆,τ)A(x,y ,τ). A rollout is accepted when it reaches the correct task answer through finish and contains meaningful scratchpad evidence: an executable z3-solve interaction that obtains a solver verdict and passes the structural checks for non-triviality, grounding, and detectable non-vacuity. We label accepted rollouts as Gold. Rollouts that reach the correct answer but provide weak formal support are labeled Silver, while rollouts that fail the answer, protocol, executability, or scratchpad-quality conditions are labeled Rejected. This partition separates task success from verifier-use quality, so that only fully supported traces become demonstrations while weak or failed traces remain available as a contrastive signal. Formally, if pT(τ∣x)p_T(τ x) is the teacher proposal distribution and ZT(x)=Prτ∼pT(⋅∣x)[A(x,y⋆,τ)=1]Z_T(x)= _τ p_T(· x)[A(x,y ,τ)=1], then the gold supervision distribution is pgold(τ∣x)=pT(τ∣x)A(x,y⋆,τ)ZT(x)=pT(τ∣x,A(x,y⋆,τ)=1).p_gold(τ x)= p_T(τ x)A(x,y ,τ)Z_T(x)=p_T(τ x,A(x,y ,τ)=1). Trace curation defines the success-conditioned target that SFT imitates, with Silver and Rejected traces supplying the negative side of the preference data. 2.4 Training SFT on Executable Traces. Gold trajectories define the supervised corpus goldD_gold. We train the student policy πθ _θ by maximum likelihood over the model-generated actions in each accepted transcript: ℒSFT(θ)=−∑τ∈gold∑t∈ℐ(τ)logπθ(at∣ht),L_SFT(θ)=- _τ _gold _t (τ) _θ(a_t h_t), where hth_t is the interaction history, ata_t is the next model token or tool-use action, and ℐ(τ)I(τ) indexes positions generated by the model. Solver observations remain in the conditioning history but are masked from the prediction loss. SFT amortizes the curated successful tail: the student learns the action patterns by which accepted traces construct evidence, respond to verifier feedback, and commit to a correct answer. Trajectory Preference Optimization. After SFT, we further refine the student with trajectory-level preferences. For each problem x with at least one Gold trace and at least one contrastive trace, we form triples (x,τ+,τ−)(x,τ^+,τ^-), where τ+τ^+ is an accepted trajectory and τ−τ^- is either Rejected or Silver. Silver traces serve as hard negatives because they may reach the correct answer with weaker scratchpad support; Rejected traces capture answer, protocol, executability, or verifier-use failures. Gold traces define what to favor, while Silver and Rejected traces define nearby behaviors to suppress. We optimize Direct Preference Optimization with the frozen SFT model πref _ref as reference. Let rθ(τ,x)=logπθ(τ∣x)−logπref(τ∣x)r_θ(τ,x)= _θ(τ x)- _ref(τ x). The objective is ℒDPO(θ)=−(x,τ+,τ−)logσ(β[rθ(τ+,x)−rθ(τ−,x)]),L_DPO(θ)=-E_(x,τ^+,τ^-) σ\! (β [r_θ(τ^+,x)-r_θ(τ^-,x) ] ), where β controls the strength of the preference update. As in SFT, trajectory likelihoods are computed over model-generated tokens and tool actions, with solver observations used as conditioning context. This stage raises the probability of complete, verifier-supported traces and lowers the probability of correct-looking but weakly supported or failed ones. Policy Bootstrapping. The success-conditioned bootstrapping mechanism relies on the teacher’s support under the acceptance predicate. Let ZT(x)=Prτ∼pT(⋅∣x)[A(x,y⋆,τ)=1]Z_T(x)= _τ p_T(· x)[A(x,y ,τ)=1] denote the teacher’s probability of producing an accepted trajectory for problem x. When ZT(x)>0Z_T(x)>0, sampling KTK_T rollouts exposes at least one Gold trace with probability 1−(1−ZT(x))KT1-(1-Z_T(x))^K_T. Trace curation turns these rare successes into a high-precision target: SFT amortizes accepted search behavior, while DPO uses Silver and Rejected traces to suppress nearby failure modes. Inference. At test time, the student uses the same SMT-scratchpad protocol as teacher sampling and training. Given x=(,q)x=(C,q), it generates tool-use actions until finish or the interaction budget. We score the final answer against y⋆y and retain the full trajectory for process analysis: solver invocation, verdict quality, non-triviality, grounding, and protocol completion. For multi-sample evaluation, we draw K independent trajectories per problem and aggregate answer and scratchpad-quality metrics. 3 Results Evaluation protocol. We present evaluations of nine Sequent-Prover checkpoints: base, supervised fine-tuned (SFT), and further preference-optimized (DPO) variants of the Qwen3.5–4B, Qwen3.5–9B, and Qwen3.6–27B families. Each model is evaluated with K=4K=4 stochastic SMT-scratchpad trajectories per problem. The final paired pool contains 37 benchmarks and 7,254 problems per model family. The suite covers logical and constraint reasoning (ProofWriter, RuleTaker, FOLIO, ProntoQA, AR-LSAT, ZebraLogic, ReClor, StrategyQA), arithmetic and spatial reasoning (GSM8K, SVAMP, MAWPS, ASDiv, AQuA-RAT, DROP, SpartQA-MC, SpartQA-YN, StepGame), NLI and multiple-choice commonsense/knowledge tasks (ANLI, BoolQ, WinoGrande, CommonsenseQA, OpenBookQA, QASC, ARC-Challenge, MMLU, HellaSwag), domain and reading-comprehension QA (MedQA, MedMCQA, PolicyQA, HotpotQA, MuSiQue, SQuAD, TriviaQA), and AGIEval LSAT/SAT subsets (LSAT-LR, LSAT-RC, SAT-Math, SAT-EN). Metrics. We report avg@N, the per-attempt accuracy over all sampled trajectories; pass@4, the probability that at least one of four samples solves the problem; and pass^4, the probability that all four samples solve the problem. We use pass^4 as the main reliability metric because deployed stochastic agents should produce correct behavior consistently, rather than only under best-of-K selection. We also report stability=pass^4/pass@4, which normalizes all-sample consistency by four-sample coverage. For process analysis, we use the SMT-quality metrics from Section 2: first-pass Z3 validity, non-trivial grounded solver use, solver verdict distributions, and token/iteration efficiency. Research questions. The results address four questions. RQ1: does verifier-conditioned post-training improve single-sample accuracy and multi-sample reliability, beyond what extra test-time sampling gives? RQ2: how do SFT and DPO differ, and which parts of the recipe matter? RQ3: how does post-training change the solver-agent process? RQ4: where are the gains largest across tasks and model scales? Aggregate performance Family Ckpt. avg@N ↑ pass@4 ↑ pass^4 ↑ Stab. ↑ Δ ^4 4B Base 0.856 0.970 0.641 0.661 – 4B SFT 0.960 0.995 0.892 0.896 +0.251 4B DPO 0.970 0.998 0.917 0.919 +0.277 9B Base 0.948 0.994 0.858 0.863 – 9B SFT 0.972 0.997 0.923 0.926 +0.065 9B DPO 0.977 0.998 0.934 0.936 +0.076 27B Base 0.991 0.998 0.977 0.979 – 27B SFT 0.989 0.999 0.971 0.972 −-0.006 27B DPO 0.995 1.000 0.986 0.986 +0.009 pass@k scaling Model @1 @2 @3 @4 4B Base 0.856 0.943 0.963 0.970 4B DPO 0.970 0.992 0.996 0.998 9B Base 0.948 0.984 0.991 0.994 9B DPO 0.977 0.994 0.997 0.998 27B Base 0.991 0.996 0.998 0.998 27B DPO 0.995 0.999 1.000 1.000 Table 1: Aggregate performance and pass@k scaling on the 37-benchmark paired evaluation pool. Each family is compared against its own base checkpoint. pass@4 measures four-sample coverage, while pass^4 requires all four sampled trajectories to be correct. The pass@k panel shows that a single 4B DPO sample matches the 4B base model’s four-sample coverage. Bold marks the best checkpoint within each family; Δ is relative to Base, with gains and losses colored. 3.1 Aggregate accuracy and reliability Table 1 shows the main comparison. Verifier-conditioned post-training yields the largest improvements for the 4B model: DPO raises avg@N from 0.856 to 0.970 and pass^4 from 0.641 to 0.917, a 27.7-point increase in all-sample reliability. The 9B model follows the same pattern from a stronger starting point, with DPO improving pass^4 from 0.858 to 0.934. The 27B base model is already close to saturation on the aggregate pool, and DPO still reaches the best value in the family for every reported metric, including pass^4 of 0.986. The distinction between pass@4 and pass^4 captures the central effect. The base checkpoints already have high four-sample coverage, especially at 9B and 27B, due to the multi-option nature of most of these tasks. Post-training concentrates probability mass on the correct trajectory mode, producing large gains in pass^4 and stability. For 4B, stability rises from 0.661 to 0.919 under DPO; for 9B, it rises from 0.863 to 0.936. This shows that the trained policies improve single-run reliability as well as best-of-four coverage. Table 1 presents the pass@k curves for the base and DPO checkpoints. The 4B result is especially clear: 4B DPO reaches 0.970 at pass@1, matching the 4B base model’s pass@4 value. At 9B, DPO raises pass@1 from 0.948 to 0.977 and nearly saturates pass@4. At 27B, the curve is near the ceiling throughout, with DPO reaching 1.000 by pass@3. ((a)) Problem-level transitions grouped by base-model correctness. Family Tune n0/4n_0/4 P(≥1/4∣0/4)P(≥ 1/4 0/4) n1−3/4n_1-3/4 P(4/4∣1CLOSEP(4/4 1–3/4)3/4) n4/4n_4/4 P(4/4∣4/4)P(4/4 4/4) 4B SFT 215 0.930 2,379 0.839 4,660 0.942 4B DPO 215 0.958 2,379 0.867 4,660 0.965 9B SFT 41 0.780 970 0.753 6,243 0.954 9B DPO 41 0.780 970 0.787 6,243 0.962 27B SFT 13 0.846 153 0.536 7,088 0.982 27B DPO 13 0.923 153 0.719 7,088 0.993 ((b)) Direct DPO–SFT comparison. Deltas are macro-averages over shared datasets; DPO-only/SFT-only paired solves are 25/8, 13/8, and 7/0 for 4B, 9B, and 27B. Family Δ @N Δ ^4 Δ . Δ Δ _ unsat 4B +0.005 +0.009 +0.007 +0.050 +0.013 9B +0.006 +0.008 +0.011 +0.036 +0.026 27B +0.005 +0.012 +0.016 +0.046 +0.050 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. 3.2 Problem-level consistency transitions Table 2(a) decomposes the reliability gains by the number of correct base-model attempts. Across 4B and 9B, the largest source of improvement is the middle tier: problems with one to three correct base attempts become correct on all four tuned attempts. For 4B DPO, this happens for 86.7% of the 2,379 partially correct base problems. For 9B DPO, it happens for 78.7% of the 970 partially correct base problems. The tuned models also preserve most problems that were already reliable: DPO retains 96.5%, 96.2%, and 99.3% of base 4/4 problems in the 4B, 9B, and 27B families, respectively. The transition table also clarifies the role of scale. The 4B base model has 2,379 partially correct problems, so post-training has substantial headroom to improve reliability. The 27B base model has only 153 partially correct problems and 13 zero-correct problems, so aggregate gains are naturally smaller. Within that restricted headroom, DPO still improves the middle-tier conversion rate from 53.6% under SFT to 71.9%, and it preserves nearly all already reliable examples. 3.3 Training-stage ablation Table 2(b) compares DPO directly against SFT on shared datasets. Preference optimization improves every family on avg@N, pass^4, stability, and verified-correct rate. The coverage overlap is large: for example, 4B SFT and 4B DPO both solve 7,213 problems at least once, while DPO adds 25 DPO-only problems and SFT adds 8 SFT-only problems. The most consistent DPO gains are in reliability and trace quality. At 27B, the DPO stage is particularly useful: it adds +0.012 macro pass^4, +0.016 stability, +0.046 verified-correct rate, and +0.050 UNSAT-restricted verified-correct rate over SFT. Method K pass@K ↑ pass^K ↑ Tokens ↓ 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 ↑ pass@4 ↑ pass^4 ↑ Stab. ↑ 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. 3.4 Test-time sampling and data ablations Post-training versus more samples. We compare the 4B models on 180 held-out problems, 30 each from ProntoQA, FOLIO, AR-LSAT, GSM8K, StepGame, and ARC-Challenge, with the same harness, temperature, and iteration limit for every method (Appendix D.2). At matched K=4K=4, post-training raises pass@4 by 10.1 points and pass^4 by 34.8 points over base self-consistency, with fewer tokens (Table 3). The post-trained model at K=4K=4 also beats the base model at K=16K=16 on both metrics while using 6.6× fewer tokens. From K=1K=1 to K=16K=16, base pass@K rises from 0.657 to 0.911, but pass^K falls from 0.657 to 0.139. Extra sampling raises coverage but lowers all-sample reliability. Self-refinement, the strongest prompting baseline, still trails the post-trained model while using 3.3× more tokens. Which parts of the recipe matter. We train four 4B variants and evaluate them on ReClor, SpartQA-MC, SpartQA-YN, StepGame, and AGIEval-LSAT-LR (200 problems each, K=4K=4; Table 4). Answer-only SFT keeps only the final answer, and pass^4 falls from 0.409 (full-trajectory SFT) to 0.126, so the gains do not come from label exposure. Solver-verdict SFT removes the grounding and non-triviality checks and is lower on every metric. Continued SFT replaces DPO with more SFT at matched training FLOPs. It ties DPO on pass^4 and is slightly higher on stability, but lower on avg@N and pass@4. Gold/Silver/Rejected DPO uses the three tiers as separate preference levels and is below our DPO on every metric. Our full recipe leads on avg@N and pass@4. ((a)) Solver-agent efficiency. Family Ckpt. Iter. ↓ SMT calls ↓ Tokens ↓ Tok./ correct ↓ First VC iter. ↓ 4B Base 4.97 4.10 18.97k 26.73k 2.00 4B SFT 3.76 2.78 13.70k 15.23k 1.33 4B DPO 3.51 2.52 12.72k 13.89k 1.29 9B Base 4.37 3.41 15.69k 19.53k 1.62 9B SFT 3.52 2.54 12.31k 14.16k 1.24 9B DPO 3.33 2.34 11.85k 13.27k 1.22 27B Base 2.92 1.90 9.51k 10.28k 1.19 27B SFT 2.85 1.86 7.92k 8.52k 1.08 27B DPO 2.58 1.58 6.78k 7.01k 1.07 ((b)) SMT scratchpad diagnostics. Family Ckpt. Error ↓ No verdict ↓ UNSAT ↑ UNSAT |correct ↑ Calls 4B Base 41.3% 10.3% 12.3% 12.9% 122.6k 4B SFT 19.1% 0.3% 35.0% 36.2% 82.0k 4B DPO 19.0% 0.4% 35.3% 36.3% 73.3k 9B Base 26.0% 0.4% 22.7% 23.0% 101.1k 9B SFT 13.9% 0.3% 38.7% 39.7% 75.0k 9B DPO 14.4% 0.4% 40.0% 41.0% 68.7k 27B Base 16.9% 0.7% 25.0% 25.2% 59.8k 27B SFT 5.8% 0.1% 44.5% 45.8% 55.0k 27B DPO 5.5% 0.1% 49.1% 49.7% 46.9k 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∣ restricts to calls inside correct attempts, and Calls is total solver calls. 3.5 Solver-agent process quality Table 5(a) shows that post-training improves the computational profile of the agent loop. The 4B DPO checkpoint reduces average iterations from 4.97 to 3.51, SMT calls from 4.10 to 2.52, and tokens from 18.97k to 12.72k. Normalizing by successful attempts, tokens per correct answer fall from 26.73k to 13.89k. The 9B and 27B families show the same pattern, with DPO giving the lowest token and solver-call cost within each family. The first verified-correct SMT signal also arrives earlier after tuning. The mean first-success iteration drops from 2.00 to 1.29 for 4B DPO, from 1.62 to 1.22 for 9B DPO, and from 1.19 to 1.07 for 27B DPO. Under a two-iteration budget, 4B DPO reaches a verified-correct rate of 0.902, above the 4B base model’s full-budget rate of 0.765; 9B DPO reaches 0.929 by iteration two, above the 9B base full-budget rate of 0.908. These early-exit curves show that post-training improves both endpoint accuracy and the efficiency frontier of the interactive solver loop. Table 5(b) shows that the tuned policies emit cleaner SMT programs and obtain stronger solver signals. For 4B, the error rate falls from 41.3% to 19.0% under DPO, and no-verdict calls fall from 10.3% to 0.4%. For 27B, the error rate falls from 16.9% to 5.5%. The same table shows a shift toward refutational solver evidence: UNSAT calls increase from 12.3% to 35.3% for 4B DPO, from 22.7% to 40.0% for 9B DPO, and from 25.0% to 49.1% for 27B DPO. The UNSAT share inside correct attempts rises in parallel, reaching 49.7% for 27B DPO. The grounding gains hold with SMT comments removed (+0.081 for 4B DPO; Appendix D.3). Post-training also lowers the structural (PCFG) divergence between independent SMT programs in all six Base-to-tuned comparisons, with every 95% interval below zero (Appendix D.4). Such structural variation predicts autoformalization errors (Ganguly et al., 2026). Fam Dataset Base pass^4 DPO pass^4 Δ 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 9B AR-LSAT 0.235 0.640 +0.405 9B ZebraLogic 0.410 0.790 +0.380 9B QASC 0.840 1.000 +0.160 9B WinoGrande 0.845 0.990 +0.145 9B CommonsenseQA 0.845 0.980 +0.135 9B ARC-Challenge 0.870 0.985 +0.115 27B ZebraLogic 0.825 0.965 +0.140 27B AR-LSAT 0.785 0.920 +0.135 27B StepGame 0.825 0.860 +0.035 27B ReClor 0.960 0.985 +0.025 Table 6: Largest representative dataset-level DPO gains on pass^4 within each model family. 3.6 Benchmark-level trends Table 6 reports representative per-dataset improvements for DPO. The highest-gain tasks are those with explicit symbolic or relational structure. At 4B, pass^4 improves by 85.2 points on ProofWriter, 59.0 points on RuleTaker, 52.5 points on AR-LSAT, 59.5 points on ZebraLogic, and 51.0 points on ProntoQA. At 9B, the largest gains include AR-LSAT, ZebraLogic, QASC, WinoGrande, CommonsenseQA, and ARC-Challenge. At 27B, aggregate scores are close to ceiling, and the clearest remaining gains are on ZebraLogic and AR-LSAT. On AR-LSAT, all three DPO students exceed the teacher’s pass^3 of 0.484, reaching 0.560, 0.640, and 0.920 (Appendix D.5). These dataset-level results align with the scratchpad interpretation of the method. The strongest gains occur where the task contains latent constraints, relational structure, arithmetic structure, or entailment structure that can be made executable. Broad QA and domain tasks also benefit in the smaller model families, with improvements on ARC-Challenge, CommonsenseQA, MedQA, MedMCQA, OpenBookQA, QASC, and WinoGrande. The aggregate effect spans more than formal logic benchmarks while remaining largest on tasks with natural SMT structure. At 4B and 9B, DPO improves avg@N and pass^4 in every category, and hard reasoning is only 14.5% of the pool (Appendix D.1). Comparison Small Large Tie Win ↑ 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. Post-training and scale. Table 7 compares tuned smaller models against larger base models. The 4B tuned agents compare favorably with the 9B base model: 4B SFT wins 61.2% of non-tied paired comparisons, and 4B DPO wins 69.9%. The 27B base model sets a higher aggregate ceiling, and the tuned 9B models win fewer non-tied comparisons against it. Combining scale and post-training gives the strongest overall checkpoints: 27B DPO has the highest aggregate avg@N, pass@4, pass^4, and SMT-quality profile in the sweep. 4 Related Works Verifier-Integrated Formal Reasoning. Recent progress in formal theorem proving has shown that language models can benefit greatly from emitting machine-checkable artifacts rather than only natural-language explanations. Systems such as Goedel Prover, DeepSeek-Prover, and Kimina-Prover combine long-form reasoning with formal verification and iterative refinement (Lin et al., 2025b; Ren et al., 2025; Wang et al., 2025). Our work is inspired by this paradigm, but shifts the target language from Lean to SMT-LIB and focuses on compact models that must operate across multiple SMT logics. Solver-Based Symbolic Reasoning and Synthesis. SMT solvers such as Z3 and cvc5 are central tools for formal verification, constraint solving, and program synthesis (de Moura and Bjørner, 2008; Barbosa et al., 2022). Classical symbolic systems rely on hand-written encodings or search procedures over formal objects. Our setting is different: the primary generator is a language model trained to emit solver-executable artifacts directly, while a symbolic backend is used to validate outputs and to synthesize additional training data. The use of SymPy as a controllable symbolic front-end is especially important for scaling supervision across diverse logic fragments (Meurer et al., 2017). Self-Repair and Tool Feedback. Outside theorem proving, a large body of work studies how models can improve outputs by reacting to execution feedback, compiler messages, or explicit critics (Yao et al., 2023; Shinn et al., 2023; First et al., 2023; Olausson et al., 2024; Chen et al., 2024; Bouzenia et al., 2025). We adopt the same high-level intuition, but the repair channel here is solver-native: parser errors, sort mismatches, failed assertions, and counterexamples. This makes the feedback more structured than free-form critique and better aligned with symbolic correctness. Reinforcement Learning for Verifiable Outputs. RL has recently become an effective way to improve pass@1 performance in reasoning and formal generation tasks (Shao et al., 2024; Liu et al., 2025; Yu et al., 2025). Our work extends that lesson to SMT-native generation. Because repair is serial and strongly depends on first-round quality, improving the expected solver reward is particularly useful in our setting. 5 Conclusion Sequent-Prover shows that solver use can be learned as a formal-reasoning policy. By filtering trajectories with executable SMT feedback and contrasting successful traces against failed ones, our method amortizes solver-guided search into the model: it learns to formulate proof obligations, encode them in SMT-LIB, interpret Z3 responses, repair formal artifacts, and commit with evidence. Empirically, post-training turns sample-dependent solver successes into stable behavior, produces more grounded and non-vacuous SMT programs, and shifts correct traces toward refutational unsat evidence. The scale-dependent results show where this training helps most: when a base model has latent solver-use competence but lacks consistency. Training on solver interaction is a direct way to make language-model reasoning checkable. 6 Limitations Sequent-Prover inherits a basic limit of formal verification: a solver can check a formal artifact, but it cannot decide whether the chosen abstraction is the intended one. Expert verification engineers face the same problem when they decide what to model, what to omit, which predicates or theories to use, and which specification captures the informal task. Sequent-Prover makes this step executable and learnable: it trains models to build grounded, non-trivial SMT artifacts, use solver feedback, and revise failed abstractions. Most tasks have no reference formalization, and semantic equivalence is co-NP-complete in propositional logic and undecidable in first-order logic. No automatic check can certify meaning preservation, so our grounding, non-triviality, and structural-uncertainty measures (Appendix D.4) serve as strong proxies for it. Learning the right level of formal abstraction remains an open problem. References Barbosa et al. (2022) H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, A. Ozdemir, M. Preiner, A. Reynolds, Y. Sheng, C. Tinelli, and Y. Zohar cvc5: A Versatile and Industrial-Strength SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, p. 415–442. External Links: Document, Link Cited by: §4. Barrett et al. (2025) C. Barrett, P. Fontaine, and C. Tinelli The SMT-LIB standard: version 2.7. Technical report Department of Computer Science, The University of Iowa. Note: Available at https://smt-lib.org External Links: Link Cited by: §1. Barrett and Tinelli (2018) C. Barrett and C. Tinelli Satisfiability modulo theories. Handbook of model checking, p. 305–343. Cited by: §1. Beyer (2023) D. Beyer Competition on software verification and witness validation: SV-COMP 2023. In Tools and Algorithms for the Construction and Analysis of Systems, p. 495–522. External Links: Document, Link Cited by: §A.3. Bouzenia et al. (2025) I. Bouzenia, P. Devanbu, and M. Pradel RepairAgent: an autonomous, LLM-based agent for program repair. In International Conference on Software Engineering, p. 2188–2200. External Links: Document, Link Cited by: §4. Chen et al. (2021) M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. D. O. Pinto, J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman, et al. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374. Cited by: §B.1. Chen et al. (2024) X. Chen, M. Lin, N. Schärli, and D. Zhou Teaching large language models to self-debug. In International Conference on Learning Representations, External Links: Link Cited by: §4. Clark et al. (2019) C. Clark, K. Lee, M. Chang, T. Kwiatkowski, M. Collins, and K. Toutanova Boolq: exploring the surprising difficulty of natural yes/no questions. In Proceedings of the 2019 conference of the north American chapter of the association for computational linguistics: Human language technologies, volume 1 (long and short papers), p. 2924–2936. Cited by: §A.3. Clark et al. (2018) P. Clark, I. Cowhey, O. Etzioni, T. Khot, A. Sabharwal, C. Schoenick, and O. Tafjord Think you have solved question answering? try arc, the ai2 reasoning challenge. arXiv preprint arXiv:1803.05457. Cited by: §A.3. Clark et al. (2020) P. Clark, O. Tafjord, and K. Richardson Transformers as soft reasoners over language. arXiv preprint arXiv:2002.05867. Cited by: §A.3. Cobbe et al. (2021) K. Cobbe, V. Kosaraju, M. Bavarian, M. Chen, H. Jun, L. Kaiser, M. Plappert, J. Tworek, J. Hilton, R. Nakano, et al. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168. Cited by: §A.3. de Moura and Bjørner (2008) L. de Moura and N. Bjørner Z3: an efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, p. 337–340. External Links: Document, Link Cited by: §1, §4. Dua et al. (2019) D. Dua, Y. Wang, P. Dasigi, G. Stanovsky, S. Singh, and M. Gardner DROP: a reading comprehension benchmark requiring discrete reasoning over paragraphs. In Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long and Short Papers), p. 2368–2378. Cited by: §A.3. Feng et al. (2025) Y. Feng, N. Weir, K. Bostrom, S. Bayless, D. Cassel, S. Chaudhary, B. Kiesl-Reiter, and H. Rangwala VeriCoT: neuro-symbolic chain-of-thought validation via logical consistency checks. arXiv preprint arXiv:2511.04662. Cited by: §1. First et al. (2023) E. First, M. N. Rabe, T. Ringer, and Y. Brun Baldur: whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, p. 1229–1241. External Links: Document, Link Cited by: §4. Ganguly et al. (2024) D. Ganguly, S. Iyengar, V. Chaudhary, and S. Kalyanaraman PROOF OF THOUGHT : neurosymbolic program synthesis allows robust and interpretable reasoning. In The First Workshop on System-2 Reasoning at Scale, NeurIPS’24, External Links: Link Cited by: §A.4, §1, §1, §2.2. Ganguly et al. (2026) D. Ganguly, V. Singh, S. Sankar, B. Zhang, X. Zhang, S. Iyengar, X. Han, A. Sharma, S. Kalyanaraman, and V. Chaudhary Grammars of formal uncertainty: when to trust LLMs in automated reasoning tasks. In The Thirty-ninth Annual Conference on Neural Information Processing Systems, External Links: Link Cited by: §A.4, §D.4, §1, §3.5. Geva et al. (2021) M. Geva, D. Khashabi, E. Segal, T. Khot, D. Roth, and J. Berant Did aristotle use a laptop? a question answering benchmark with implicit reasoning strategies. Transactions of the Association for Computational Linguistics 9, p. 346–361. External Links: Document, Link Cited by: §A.3. Han et al. (2024) S. Han, H. Schoelkopf, Y. Zhao, Z. Qi, M. Riddell, W. Zhou, J. Coady, D. Peng, Y. Qiao, L. Benson, et al. Folio: natural language reasoning with first-order logic. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, p. 22017–22031. Cited by: §A.3, §A.3. Hendrycks et al. (2020) D. Hendrycks, C. Burns, S. Basart, A. Zou, M. Mazeika, D. Song, and J. Steinhardt Measuring massive multitask language understanding. arXiv preprint arXiv:2009.03300. Cited by: §A.3. Hertzberg et al. (2025) N. Hertzberg, M. Sevenhuijsen, L. Kåreborn, and A. Lokrantz CASP: an evaluation dataset for formal verification of C code. arXiv preprint arXiv:2508.18798. External Links: 2508.18798, Link Cited by: §A.3. Joshi et al. (2017) M. Joshi, E. Choi, D. S. Weld, and L. Zettlemoyer Triviaqa: a large scale distantly supervised challenge dataset for reading comprehension. In Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), p. 1601–1611. Cited by: §A.3. Kazemi et al. (2025) M. Kazemi, B. Fatemi, H. Bansal, J. Palowitch, C. Anastasiou, S. V. Mehta, L. K. Jain, V. Aglietti, D. Jindal, P. Chen, N. Dikkala, G. Tyen, X. Liu, U. Shalit, S. Chiappa, K. Olszewska, Y. Tay, V. Q. Tran, Q. V. Le, and O. Firat BIG-Bench Extra Hard. arXiv preprint arXiv:2502.19187. External Links: 2502.19187, Link Cited by: §A.3. Khot et al. (2020) T. Khot, P. Clark, M. Guerquin, P. Jansen, and A. Sabharwal Qasc: a dataset for question answering via sentence composition. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 34, p. 8082–8090. Cited by: §A.3. Kojima et al. (2022) T. Kojima, S. (. Gu, M. Reid, Y. Matsuo, and Y. Iwasawa Large language models are zero-shot reasoners. In Advances in Neural Information Processing Systems, S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh (Eds.), Vol. 35, p. 22199–22213. External Links: Link Cited by: §1. Koncel-Kedziorski et al. (2016) R. Koncel-Kedziorski, S. Roy, A. Amini, N. Kushman, and H. Hajishirzi MAWPS: a math word problem repository. In Proceedings of the 2016 conference of the north american chapter of the association for computational linguistics: human language technologies, p. 1152–1157. Cited by: §A.3. Lanham et al. (2023) T. Lanham, A. Chen, A. Radhakrishnan, B. Steiner, C. Denison, D. Hernandez, D. Li, E. Durmus, E. Hubinger, J. Kernion, et al. Measuring faithfulness in chain-of-thought reasoning. arXiv preprint arXiv:2307.13702. Cited by: §1. Lin et al. (2025a) B. Y. Lin, R. Le Bras, K. Richardson, A. Sabharwal, R. Poovendran, P. Clark, and Y. Choi ZebraLogic: on the scaling limits of LLMs for logical reasoning. arXiv preprint arXiv:2502.01100. External Links: 2502.01100, Link Cited by: §A.3, §A.3. Lin et al. (2025b) Y. Lin, S. Tang, B. Lyu, J. Wu, H. Lin, K. Yang, J. Li, M. Xia, D. Chen, S. Arora, and C. Jin Goedel-Prover: a frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640. External Links: 2502.07640, Link Cited by: §4. Ling et al. (2017) W. Ling, D. Yogatama, C. Dyer, and P. Blunsom Program induction by rationale generation: learning to solve and explain algebraic word problems. In Proceedings of the 55th annual meeting of the association for computational linguistics (volume 1: Long papers), p. 158–167. Cited by: §A.3. Liu et al. (2025) Z. Liu, C. Chen, W. Li, P. Qi, T. Pang, C. Du, W. S. Lee, and M. Lin Understanding R1-Zero-like training: a critical perspective. arXiv preprint arXiv:2503.20783. External Links: 2503.20783, Link Cited by: §4. Loughridge et al. (2024) C. Loughridge, Q. Sun, S. Ahrenbach, F. Cassano, C. Sun, Y. Sheng, A. Mudide, M. R. H. Misu, N. Amin, and M. Tegmark DafnyBench: a benchmark for formal software verification. arXiv preprint arXiv:2406.08467. External Links: 2406.08467, Link Cited by: §A.3. Meurer et al. (2017) A. Meurer, C. P. Smith, M. Paprocki, O. Čertík, S. B. Kirpichev, M. Rocklin, A. Kumar, S. Ivanov, J. K. Moore, S. Singh, T. Rathnayake, S. Vig, B. E. Granger, R. P. Muller, F. Bonazzi, H. Gupta, S. Vats, F. Johansson, F. Pedregosa, M. J. Curry, A. R. Terrel, Š. Roučka, A. Saboo, I. Fernando, S. Kulal, R. Cimrman, and A. Scopatz SymPy: symbolic computing in Python. PeerJ Computer Science 3, p. e103. External Links: Document, Link Cited by: §4. Miao et al. (2020) S. Miao, C. Liang, and K. Su A diverse corpus for evaluating and developing english math word problem solvers. In Proceedings of the 58th annual meeting of the Association for Computational Linguistics, p. 975–984. Cited by: §A.3. Mihaylov et al. (2018) T. Mihaylov, P. Clark, T. Khot, and A. Sabharwal Can a suit of armor conduct electricity? a new dataset for open book question answering. In Proceedings of the 2018 conference on empirical methods in natural language processing, p. 2381–2391. Cited by: §A.3. Mirzaee et al. (2021) R. Mirzaee, H. R. Faghihi, Q. Ning, and P. Kordjamshidi SPARTQA: a textual question answering benchmark for spatial reasoning. In Proceedings of the 2021 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, p. 4582–4598. Cited by: §A.3. Olausson et al. (2023) T. X. Olausson, A. Gu, B. Lipkin, C. E. Zhang, A. Solar-Lezama, J. B. Tenenbaum, and R. Levy LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers. arXiv preprint arXiv:2310.15164. Cited by: §1. Olausson et al. (2024) T. X. Olausson, J. P. Inala, C. Wang, J. Gao, and A. Solar-Lezama Is self-repair a silver bullet for code generation?. In International Conference on Learning Representations, External Links: Link Cited by: §4. Pan et al. (2023) L. Pan, A. Albalak, X. Wang, and W. Y. Wang Logic-LM: empowering large language models with symbolic solvers for faithful logical reasoning. In Findings of the Association for Computational Linguistics: EMNLP 2023, p. 3806–3824. External Links: Link Cited by: §1. Patel et al. (2021) A. Patel, S. Bhattamishra, and N. Goyal Are nlp models really able to solve simple math word problems?. In Proceedings of the 2021 conference of the North American chapter of the association for computational linguistics: human language technologies, p. 2080–2094. Cited by: §A.3. Rajpurkar et al. (2016) P. Rajpurkar, J. Zhang, K. Lopyrev, and P. Liang Squad: 100,000+ questions for machine comprehension of text. In Proceedings of the 2016 conference on empirical methods in natural language processing, p. 2383–2392. Cited by: §A.3. Ren et al. (2025) Z. Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang, Z. F. Wu, Z. Gou, S. Ma, H. Tang, Y. Liu, W. Gao, D. Guo, and C. Ruan DeepSeek-Prover-V2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801. External Links: 2504.21801, Link Cited by: §D.5, §4. Roy and Roth (2015) S. Roy and D. Roth Solving general arithmetic word problems. In Proceedings of the 2015 conference on empirical methods in natural language processing, p. 1743–1752. Cited by: §A.3. Sakaguchi et al. (2021) K. Sakaguchi, R. L. Bras, C. Bhagavatula, and Y. Choi Winogrande: an adversarial winograd schema challenge at scale. Communications of the ACM 64 (9), p. 99–106. Cited by: §A.3. Saparov and He (2022) A. Saparov and H. He Language models are greedy reasoners: a systematic formal analysis of chain-of-thought. arXiv preprint arXiv:2210.01240. Cited by: §A.3. Shao et al. (2024) Z. Shao, P. Wang, Q. Zhu, R. Xu, J. Song, X. Bi, H. Zhang, M. Zhang, Y. K. Li, Y. Wu, and D. Guo DeepSeekMath: pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300. External Links: 2402.03300, Link Cited by: §4. Shi et al. (2022) Z. Shi, Q. Zhang, and A. Lipani Stepgame: a new benchmark for robust multi-hop spatial reasoning in texts. In Proceedings of the AAAI conference on artificial intelligence, Vol. 36, p. 11321–11329. Cited by: §A.3. Shinn et al. (2023) N. Shinn, F. Cassano, E. Berman, A. Gopinath, K. Narasimhan, and S. Yao Reflexion: language agents with verbal reinforcement learning. In Advances in Neural Information Processing Systems, Vol. 36. External Links: Link Cited by: §4. Si et al. (2018) X. Si, H. Dai, M. Raghothaman, M. Naik, and L. Song Learning loop invariants for program verification. In Advances in Neural Information Processing Systems, Vol. 31. External Links: Link Cited by: §A.3. Singh et al. (2026) V. Singh, D. Cassel, N. Weir, N. Feng, and S. Bayless VERGE: formal refinement and guidance engine for verifiable llm reasoning. arXiv preprint arXiv:2601.20055. Cited by: §A.4, §1. Tafjord et al. (2021) O. Tafjord, B. Dalvi, and P. Clark Proofwriter: generating implications, proofs, and abductive statements over natural language. In Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021, p. 3621–3634. Cited by: §A.3. Talmor et al. (2019) A. Talmor, J. Herzig, N. Lourie, and J. Berant Commonsenseqa: a question answering challenge targeting commonsense knowledge. In Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long and Short Papers), p. 4149–4158. Cited by: §A.3. Trivedi et al. (2022) H. Trivedi, N. Balasubramanian, T. Khot, and A. Sabharwal MuSiQue: multihop questions via single-hop question composition. Transactions of the Association for Computational Linguistics 10, p. 539–554. Cited by: §A.3. Turpin et al. (2023) M. Turpin, J. Michael, E. Perez, and S. Bowman Language models don’t always say what they think: unfaithful explanations in chain-of-thought prompting. Advances in Neural Information Processing Systems 36, p. 74952–74965. Cited by: §1. Wang et al. (2025) H. Wang, M. Unsal, X. Lin, M. Baksys, J. Liu, M. Dos Santos, F. Sung, M. Vinyes, Z. Ying, Z. Zhu, J. Lu, H. de Saxcé, B. Bailey, C. Song, C. Xiao, D. Zhang, E. Zhang, F. Pu, H. Zhu, J. Liu, J. Bayer, J. Michel, L. Yu, L. Dreyfus-Schmidt, L. Tunstall, L. Pagani, M. Machado, P. Bourigault, R. Wang, S. Polu, T. Barroyer, W. Li, Y. Niu, Y. Fleureau, Y. Hu, Z. Yu, Z. Wang, Z. Yang, Z. Liu, and J. Li Kimina-Prover preview: towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354. External Links: 2504.11354, Link Cited by: §4. Wei et al. (2022) J. Wei, X. Wang, D. Schuurmans, M. Bosma, F. Xia, E. Chi, Q. V. Le, D. Zhou, et al. Chain-of-thought prompting elicits reasoning in large language models. Advances in neural information processing systems 35, p. 24824–24837. Cited by: §1. Yang et al. (2018) Z. Yang, P. Qi, S. Zhang, Y. Bengio, W. Cohen, R. Salakhutdinov, and C. D. Manning HotpotQA: a dataset for diverse, explainable multi-hop question answering. In Proceedings of the 2018 conference on empirical methods in natural language processing, p. 2369–2380. Cited by: §A.3. Yao et al. (2023) S. Yao, D. Yu, J. Zhao, I. Shafran, T. L. Griffiths, Y. Cao, and K. Narasimhan Tree of Thoughts: deliberate problem solving with large language models. In Advances in Neural Information Processing Systems, Vol. 36. External Links: Link Cited by: §4. Ye et al. (2023) X. Ye, Q. Chen, I. Dillig, and G. Durrett SATLM: Satisfiability-Aided Language Models using Declarative Prompting. In Proceedings of the International Conference on Neural Information Processing Systems, Cited by: §1. Yu et al. (2025) Q. Yu, Z. Zhang, R. Zhu, Y. Yuan, X. Zuo, Y. Yue, W. Dai, T. Fan, G. Liu, L. Liu, X. Liu, H. Lin, Z. Lin, B. Ma, G. Sheng, Y. Tong, C. Zhang, M. Zhang, W. Zhang, H. Zhu, J. Zhu, J. Chen, J. Chen, C. Wang, H. Yu, Y. Song, X. Wei, H. Zhou, J. Liu, W. Ma, Y. Zhang, L. Yan, M. Qiao, Y. Wu, and M. Wang DAPO: an open-source LLM reinforcement learning system at scale. arXiv preprint arXiv:2503.14476. External Links: 2503.14476, Link Cited by: §4. Yu et al. (2020) W. Yu, Z. Jiang, Y. Dong, and J. Feng Reclor: a reading comprehension dataset requiring logical reasoning. arXiv preprint arXiv:2002.04326. Cited by: §A.3. Zellers et al. (2019) R. Zellers, A. Holtzman, Y. Bisk, A. Farhadi, and Y. Choi Hellaswag: can a machine really finish your sentence?. In Proceedings of the 57th annual meeting of the association for computational linguistics, p. 4791–4800. Cited by: §A.3. Zhong et al. (2024) W. Zhong, R. Cui, Y. Guo, Y. Liang, S. Lu, Y. Wang, A. Saied, W. Chen, and N. Duan Agieval: a human-centric benchmark for evaluating foundation models. In Findings of the association for computational linguistics: NAACL 2024, p. 2299–2314. Cited by: §A.3. Zhong et al. (2021) W. Zhong, S. Wang, D. Tang, Z. Xu, D. Guo, J. Wang, J. Yin, M. Zhou, and N. Duan AR-LSAT: investigating analytical reasoning of text. arXiv preprint arXiv:2104.06598. External Links: 2104.06598, Link Cited by: §A.3. Appendix A Background: Agent, Solver & Training We first describe three pieces of background: (1) what Z3 actually computes, (2) how the language model interacts with it, and (3) how the two post-training recipes differ in what they teach. The metric definitions that follow depend on these choices. A.1 The Z3 SMT Solver and the Two Proof Modes Z3 is a Satisfiability Modulo Theories (SMT) solver: given a quantifier-free first-order formula φ over a combination of background theories (linear/non-linear integer or real arithmetic, fixed-size bit-vectors, equality with uninterpreted functions, strings, arrays, datatypes), Z3 returns one of • sat: φ has a model under the theory combination, and Z3 (optionally) returns it as (define-fun x…)( define-fun x…) definitions; • unsat: φ is unsatisfiable in the theory combination, so no assignment can make it true; • unknown: Z3’s procedure was incomplete or timed out; • an error string: the input did not parse, used a symbol Z3 cannot interpret, or violated the declared sort. Our agent uses Z3 in two operationally distinct modes; the distinction is central to how to read the verdict mix in §B.3. Direct constraint-satisfaction (the sat mode). The agent encodes the problem’s premises as constraints and the candidate answer as an additional assertion, then queries (check-sat). A return of sat establishes that the candidate answer is consistent with the premises and the agent may extract a satisfying model from Z3’s (get-model) output. For an open-ended constraint-search task (e.g., ZebraLogic, where the agent must find “the house with the cat”), the witness is the answer. For a deductive task (e.g., ProofWriter, where the agent must say whether “p entails q”), a sat verdict on Γ∪q ∪\q\ only tells us that q is not contradicted by Γ , which is a strictly weaker claim than Γ⊧q q. Proof by contradiction (the unsat mode). The deductively-strong way to use Z3 for an entailment question is to assert the premises together with the negation of the candidate conclusion, Γ∪¬q ∪\ q\, and check satisfiability. A return of unsat establishes that Γ∪¬q ∪\ q\ has no model, i.e. Γ⊧q q in the theory. This is the standard refutational argument that underlies essentially all SMT-based theorem proving. An agent that systematically produces unsat verdicts on deductive tasks is using the solver as a prover; an agent that systematically produces sat verdicts on the same tasks is using it as a model-finder and is, in the worst case, verifying nothing more than internal consistency. The pair of metrics vcrvcr and vcrunsatvcr_ unsat introduced in §B.3 make this distinction quantitative: a delta in vcrunsatvcr_ unsat larger than the delta in vcrvcr indicates that post-training is shifting the agent toward refutational rather than model-finding use of the solver, even when the underlying correctness count is unchanged. A.2 The Tool-Calling Agent Loop The agent harness uses an OpenAI-compatible tool-calling protocol exposed by vLLM. At each iteration τ the model receives the cumulative conversation ℋτ=(m1,m2,…)H_τ= (m_1,m_2,… ) consisting of the system prompt, the user problem, every prior model turn, and the structured payload from every prior tool call. The model may emit one of two output shapes: 1. a tool call to z3_solve with arguments smt_code:sτ,timeout:int\ smt\_code:s_τ,\, timeout: int\, parsed by Qwen’s qwen3_coder tool grammar; or 2. a free-text reply containing the final answer. Reasoning content (Qwen’s ⟨ ⟩ …⟨ /think⟩ block) is parsed by the qwen3 reasoning parser and is not re-emitted to subsequent turns; only the model’s user-visible reply plus its tool-call schema is carried forward, which prevents the context window from growing quadratically in TmaxT_ . When the agent calls z3_solve, the harness runs sτs_τ under a 30-second wall-clock cap and a 256-MB memory cap, captures the full stdout/stderr, and returns the payload (success,output,sat_result,error)( success, output, sat\_result, error) as a tool-response message. The sat_result field is taken from the exit line of (check-sat) and normalised to one of \sat, unsat, unknown\. The original output is kept separately so the agent (and our analyzer) can recover (get-model)( get-model) witnesses or error stacks. The loop terminates when the model produces an attempt without a tool call (success), when it explicitly emits the special finish terminator (success), or when τ reaches Tmax=10T_ =10 (timeout). The terminating attempt’s free-text answer is run through the dataset-specific check_correct extractor (which handles option-letter matching for MCQ, multiset matching for ZebraLogic, exact-string for arithmetic, etc.) to produce the correctness bit cp(k)c_p^(k). The boolean attribute verified on each JSONL row is not the correctness bit. It records whether the agent terminated by producing an answer (verified = True) or by hitting the iteration cap and being forced to extract whatever the model last said (verified = False); the metrics soundness and completeness in §B.2 treat verified as a confidence/commitment signal, not as correctness. A.3 Datasets. We sample 1,000 questions each from the training splits of three hard reasoning datasets: AR-LSAT (Zhong et al., 2021), FOLIO (Han et al., 2024), and ZebraLogic (Lin et al., 2025a). For diversity, we add a small hand-curated set from BBEH (Kazemi et al., 2025), CASP (Hertzberg et al., 2025), Code2Inv (Si et al., 2018), DafnyBench (Loughridge et al., 2024), and SV-COMP (Beyer, 2023). The three core datasets were chosen because they require different forms of symbolic reasoning: AR-LSAT consists of analytical reasoning problems with combinatorial constraints, FOLIO requires reasoning over first-order logical premises, and ZebraLogic contains constraint-satisfaction puzzles with latent entity–attribute assignments. This gives the model supervision on problems where success typically requires constructing and checking an explicit symbolic state, rather than relying only on lexical or parametric associations. At evaluation time, we enforce strict decontamination: no problem used for training is included in evaluation, and evaluation examples are drawn from held-out splits whenever labels are available. We therefore distinguish between in-distribution evaluation, which consists only of held-out examples from the same three core dataset families used during training, and out-of-distribution evaluation, which covers all other benchmark sources. This distinction is at the dataset-family level rather than the instance level: even the in-distribution setting is instance-disjoint from training, while the out-of-distribution setting tests transfer to new annotation protocols, answer formats, domains, and reasoning styles. The evaluation suite is broad. In addition to the three core training benchmarks, we evaluate on logical and rule-based reasoning tasks such as StrategyQA, ProntoQA, ProofWriter, ReClor, and RuleTaker; arithmetic and discrete reasoning benchmarks such as GSM8K, SVAMP, MultiArith, ASDiv, AQuA-RAT, MAWPS, and DROP; spatial reasoning tasks including SpartQA and StepGame; commonsense and science multiple-choice benchmarks including OpenBookQA, QASC, ARC-Challenge, CommonsenseQA, and WinoGrande; broad-coverage multiple-choice benchmarks including MMLU, HellaSwag, BoolQ, MedQA, and MedMCQA; and free-form multi-hop QA datasets including HotpotQA, MuSiQue, SQuAD, and TriviaQA (Geva et al., 2021; Saparov and He, 2022; Tafjord et al., 2021; Han et al., 2024; Zhong et al., 2024; Lin et al., 2025a; Yu et al., 2020; Clark et al., 2020; Cobbe et al., 2021; Patel et al., 2021; Roy and Roth, 2015; Miao et al., 2020; Ling et al., 2017; Koncel-Kedziorski et al., 2016; Dua et al., 2019; Mirzaee et al., 2021; Shi et al., 2022; Mihaylov et al., 2018; Khot et al., 2020; Clark et al., 2018; Talmor et al., 2019; Sakaguchi et al., 2021; Hendrycks et al., 2020; Zellers et al., 2019; Clark et al., 2019; Yang et al., 2018; Trivedi et al., 2022; Rajpurkar et al., 2016; Joshi et al., 2017). The resulting split tests whether post-training on a small set of hard symbolic datasets teaches a general solver-use behavior that transfers beyond the observed training distribution, rather than merely improving accuracy on the benchmark families used for supervision. A.4 Reproducibility. We have released the SMT harness and its code (https://github.com/DebarghaG/proofofthought). We have also released the post-trained 4B, 9B, and 27B models (https://huggingface.co/saccha-ai). Training Data. Our trajectory dataset contains a total of 14,307 training samples, containing 10,785 gold, 2,995 reject, 464 silver, and 63 discarded infrastructure-error trajectories. This data was generated by using our verifier-conditioned trajectory distillation from a Deepseek-v4 Flash model. Temperature during both dataset curation and all evaluation was maintained at 0.9. Teacher rollouts and acceptance. We sample three teacher rollouts per training problem (eight for part of AR-LSAT). Table 8 gives the teacher’s answer accuracy on the three core datasets. A trace is Gold only when the final answer matches the label, the trace ends with finish, the SMT is non-trivial and grounded, and Z3 returns a real verdict. Labels are checked with the same dataset-specific check_correct extractor used at evaluation. Rejected traces are incorrect, unfinished, malformed, or have no SMT call. On AR-LSAT, many rejected traces keep calling z3-solve without finishing; others contain real formalization errors. A few correct answers were rejected because they did not match the exact output format. On FOLIO, failures are more semantic: the teacher translates premises into predicates inconsistently and mixes up True, False, and Uncertain. We de-duplicate training and evaluation problems, so no training problem appears in the test pool. Dataset pass@3 pass^3 AR-LSAT 0.727 0.484 FOLIO 0.853 0.738 ZebraLogic 0.999 0.901 Table 8: Teacher (DeepSeek-v4 Flash) answer accuracy with three rollouts per training problem. Training details. We post-train models using full-parameter fine-tuning with DeepSpeed ZeRO-3. For supervised fine-tuning, we optimize the autoregressive language-modeling objective over pre-rendered Qwen3.5 chat-template traces. Each training example is stored as a single text sequence that preserves the exact interleaving of reasoning, tool calls, and solver outputs, including <think>...</think>, <tool_call>...</tool_call>, and <tool_response>...</tool_response> spans. We use this representation directly rather than converting through an OpenAI- or ShareGPT-style message format, since the latter can discard assistant reasoning text when tool calls are also present. This ensures that the model is trained on the same rendered traces that it is expected to produce at inference time. The supervised run uses the base checkpoint, full fine-tuning, bfloat16 precision, gradient checkpointing, FlashAttention, and a maximum sequence length of 16,384 tokens. We enable sequence packing for throughput. Training is performed for two epochs on 8×A100-80GB GPUs or H200 GPUs according to SLURM availability with per-device batch size 1 and gradient accumulation 8, giving an effective batch size of 64. We use AdamW with learning rate 3×10−63× 10^-6, cosine learning-rate decay, warmup ratio 0.03, weight decay 0, and gradient clipping at norm 1.0. Checkpoints are saved every 10 optimizer steps, retaining the three most recent checkpoints. We then apply Direct Preference Optimization (DPO) starting from the last supervised checkpoint, where the supervised loss had plateaued in our run. The preference data consists of chosen/rejected SMT autoformalization traces. We train on the entire assistant trajectory, while preserving the same Qwen3.5 chat-template rendering. We use the standard sigmoid DPO objective with β=0.1β=0.1. DPO is also performed with full-parameter fine-tuning, bfloat16 precision, gradient checkpointing, FlashAttention, and DeepSpeed ZeRO-3. Because DPO evaluates chosen and rejected continuations separately and does not use packing, we set the cutoff length to 8,192 tokens and discard preference pairs whose prompt-plus-response length exceeds this limit, avoiding truncation inside tool-call spans. The DPO run is trained for two epochs on 8×A100-80GB GPUs with per-device batch size 1 and gradient accumulation 4, giving an effective batch size of 32. We use learning rate 5×10−75× 10^-7, cosine decay, warmup ratio 0.1, weight decay 0, and gradient clipping at norm 1.0. Scope, Design Choices and Limitations We note six scope decisions. First, Sequent-Prover builds on the SMT-LIB backend of Proof-of-Thought (Ganguly et al., 2024), and our contribution is the post-training recipe. We do not compare against Grammars of Formal Uncertainty or VERGE (Singh et al., 2026; Ganguly et al., 2026), which sample hundreds of programs per question, since a fair comparison would need a similar test-time budget. Section 3.4 instead compares our 4B model against its base model with up to sixteen samples and against three prompting baselines. Second, each component ablation needs a full post-training and evaluation sweep, so we do not ablate every design choice at every scale. We ablate the main data-selection choices at 4B on five held-out benchmarks (Section 3.4). Across nine checkpoints and 37 benchmarks, the full recipe improves reliability, grounding, and refutational solver use, and tuning individual components may give further gains. Third, the largest improvements are on the smaller models and on tasks with latent symbolic structure. The 27B Qwen3.6 base model is already a strong tool-caller and code generator, and post-training still brings it near ceiling on the aggregate pool. Most remaining headroom lies in tasks harder than the current suite. Fourth, we report most metrics in aggregate over 7,254 problems per family. This keeps the paper readable, and the pool is large enough for stable deltas. Appendix D.1 gives per-category results for all three families. The auxiliary measures in Appendix B, such as soundness, recovery, calibration, and skeleton diversity, follow the same trends as the main reliability and verifier-use metrics. The predicted SFT-induced drop in soundness does not lower reliability (Appendix D.6). Fifth, curation and evaluation share the same grounding and triviality predicates. These permissive, substring-based criteria apply equally to every checkpoint, including the untrained baselines, so if anything they favor the baselines. The grounding trends also hold when SMT comments are removed (Appendix D.3). Finally, all base models and the DeepSeek-v4-Flash teacher use their own chat-template format, and the mixed point-release versions within a family are the actual base models we used. We have released the SMT harness and the post-trained checkpoints, and will release the 14,307 curated trajectories and prompts, so that the results can be reproduced with the same harness. License, Compute Budget, Risks All evaluation benchmarks are public datasets used under their original research licenses; Z3 (MIT), and the Qwen base models (under their respective open model licenses) are used in accordance with their terms, and our harness and checkpoints are released, and our trajectories will be released, under a permissive open-source license for research use. Across prototyping, repeated iteration, teacher rollout generation, SFT, DPO for all three model families, the full sweep used approximately 1000 GPU-hours on A100-80GB/H200 hardware. Our work studies formal reasoning over public academic benchmarks and introduces no new data, deployment surface, or generative capability that poses foreseeable risk of harm. Appendix B Evaluation Metrics Let D be a dataset with M=||M=|D| problems, each problem x∈x having a gold answer yx⋆y_x . For each problem the model produces K i.i.d. samples; the r-th attempt yields a trace τx(r) _x^(r) and a final answer y^x(r) y_x^(r), plus a sequence of SMT calls (zx(r,1),…,zx(r,Sx(r))) (z_x^(r,1),…,z_x^(r,S_x^(r)) ) with associated Z3 responses (ρx(r,1),…,ρx(r,Sx(r))). ( _x^(r,1),…, _x^(r,S_x^(r)) ). We write χx(r):=[check correct(y^x(r),yx⋆)] _x^(r):=1\! [ check correct ( y_x^(r),y_x ) ] χx:=∑r=1Kχx(r)∈0,1,…,K. _x:= _r=1^K _x^(r)∈\0,1,…,K\. χx _x is the number of correct attempts on problem x, and χ¯x:=χx/K χ_x:= _x/K is the per-problem accuracy. The boolean κx(r) _x^(r) denotes the commitment event, i.e. the verified JSONL field of §A.2; Tx(r)T_x^(r) denotes the iteration count; and Sx(r)S_x^(r) denotes the number of SMT calls. Unless stated otherwise we use K=4K=4. We use r for the sample index and reserve n for the sample budget inside metrics such as pass@n and maj@n. We group metrics into three families: sample-based correctness (§B.1), which depend only on the bag of correctness indicators χx(r)\ _x^(r)\; agent-reliability measures (§B.2), which characterize the relationship between the agent’s internal commitment signal and its actual correctness; and SMT-program quality (§B.3), which inspect the structural and semantic properties of the SMT-LIB code that the agent emitted, independent of whether the final answer was correct. B.1 Sample-Based Correctness The metrics in this subsection depend only on the multiset χx(r)x,r\ _x^(r)\_x,r; they do not inspect the agent trace. Each is a moment of the per-problem correctness count χx∈0,…,K _x∈\0,…,K\ under a different functional form, designed to isolate different facets of the underlying success distribution. avg@N. The per-attempt expected accuracy, computed as the empirical mean of χ¯x χ_x across problems: avg@N=1M∑x∈χ¯x=1MK∑x,rχx(r). avg@N= 1M _x χ_x= 1MK _x,r _x^(r). (1) avg@N avg@N has the operational interpretation of single-attempt success: if a user runs the agent once with one temperature draw, avg@N avg@N is the expected correctness of that single attempt. It is invariant to which of the K samples we examine, and it is an unbiased estimate of the per-attempt correctness probability. pass@n. The unbiased estimator of Chen et al. (2021) for the probability that at least one of n samples is correct: for n≤Kn≤ K, pass@n=1M∑x∈[1−(K−χxn)(Kn)]. pass@n= 1M _x [1- K- _xn Kn ]. (2) The estimator is unbiased under random subsampling without replacement from the K observed attempts: (K−χxn)/(Kn) K- _xn/ Kn is the exact probability of drawing n all-incorrect attempts, and pass@n pass@n is one minus its expectation. pass@1=avg@N pass@1= avg@N exactly. For n>1n>1, the quantity reflects the user-facing utility of taking multiple samples and accepting the answer if any one is correct. This is an ensemble-with-oracle-selection ceiling. We report pass@4 pass@4 throughout. pass^n. The expected probability that every one of n samples is correct, under the same random-subsampling estimator: passn=1M∑x∈(χxn)(Kn).pass^n= 1M _x _xn Kn. (3) (χxn)/(Kn) _xn/ Kn is the probability that all n randomly drawn attempts are correct. Two checkpoints with the same pass@n pass@n may differ dramatically in passnpass^n: passnpass^n rewards distributional concentration on the right answer: high values arise iff the right answer is the modal answer across samples, low values arise when correctness is sample-dependent. maj@n. The expected probability that majority vote among n samples agrees with the gold answer. Because check correct is binary, majority on correctness is well-defined and gives, under random subsampling without replacement and the conservative tie convention of strict majority, with ties broken against the agent, maj@n=1M∑x∈1(Kn)∑j=⌊n/2⌋+1n(χxj)×(K−χxn−j). split maj@n&= 1M _x 1 Kn _j= n/2 +1^n _xj\\ & × K- _xn-j. split (4) We report maj@4 maj@4 throughout. The gap between maj@n maj@n and avg@N avg@N measures the benefit of self-consistency aggregation, which assumes wrong answers are more diverse than right ones. Stability. The ratio of consistency to coverage, stability=passnpass@n∈[0,1]. stability= pass^n pass@n∈[0,1]. (5) A value of 11 indicates perfect consistency: any problem the model can solve, it solves on every attempt. A value of 00 indicates the right answer is purely sample-dependent. The stability delta summarizes the main post-training effect in one number. AUC@n. A finer-grained “area-under-the-curve” summary of the full (pass@j)j=1n( pass@j)_j=1^n trajectory, used internally by the reporting pipeline: AUC@n=1n∑j=1npass@j. AUC@n= 1n _j=1^n pass@j. (6) AUC@n AUC@n favors checkpoints whose accuracy at small j is already high, i.e., checkpoints that do not depend on the oracle-selection ceiling. Equivalently, it can be read as a discount on later samples and so penalizes sample-greedy ensembles. g-pass@nαn_α. The threshold-pass variant: g-pass@nα g-pass@n_α is the expected indicator that at least a fraction α∈(0,1]α∈(0,1] of n random samples is correct. α=1α=1 recovers passnpass^n, and α=1/nα=1/n recovers pass@n pass@n; we report the standard α∈0.25,0.5,0.75,1.0α∈\0.25,0.5,0.75,1.0\ ladder in the per-dataset reports of nl2smt.analyze, but only the endpoints in the main tables below. B.2 Agent-Reliability Measures These metrics compare the agent’s behavior conditional on internal events. As established in §A.2, κx(r) _x^(r) is the commitment bit, namely the JSONL verified field: it is 11 iff the agent terminated the loop by producing an answer rather than hitting TmaxT_ . χx(r) _x^(r) is the correctness bit. κx(r)=1,χx(r)=0 _x^(r)=1, _x^(r)=0 is the overcommit cell (the agent declared confidence in a wrong answer) and is the operative quantity in the soundness metric. Soundness. soundness=ℙ(χ=1∣κ=1)=∑x,rχx(r)κx(r)∑x,rκx(r). soundness=P(χ=1 κ=1)= _x,r _x^(r) _x^(r) _x,r _x^(r). (7) Among attempts where the agent chose to finish instead of refining further, what fraction were correct? Soundness is a measure of decision quality: it asks whether the agent’s internal stopping criterion is well-aligned with ground truth. Low soundness indicates an agent that “thinks it’s done” while still wrong; a drop in soundness during post-training is diagnostic of training-induced overconfidence, typically introduced by SFT on demonstration traces that all terminate successfully. Completeness. completeness=ℙ(κ=1∣χ=1). completeness=P(κ=1 χ=1). (8) Among correct attempts, what fraction terminated voluntarily? Low completeness is the dual failure to soundness: the agent silently arrives at a correct answer but does not commit, instead burning iterations until it hits TmaxT_ . In practice every reported configuration in this work has completeness≥0.999 completeness≥ 0.999 because Qwen reliably emits a finish terminator when satisfied. We retain completeness in the table for diagnostic value and because failure modes on novel datasets could plausibly violate it. Recovery. recovery=ℙ(χ=1∣first SMT call errored). recovery=P (χ=1 SMT call errored ). (9) The conditioning event is precisely success(zx(r,1))=False\ success(z_x^(r,1))= False\ or the first call’s sat result was missing; i.e., the very first Z3 invocation either failed to parse, ran out of resources, or did not return a verdict. Recovery measures the agent’s robustness to early failure: a high value indicates the agent diagnoses the error from Z3’s stderr text, rewrites the SMT, and eventually arrives at the right answer; a low value indicates the agent commits to a wrong answer after the first bad call. The difference recovery−avg@N recovery- avg@N measures the conditional penalty of a first-call failure, with the unconditional accuracy as baseline. Expected Calibration Error. With only a binary commitment signal κ and binary correctness χ, ECE collapses to the absolute gap between the per-attempt commitment rate and the per-attempt accuracy: ECE=|κ¯−χ¯|. ECE= |\, κ- χ\, |. (10) For a well-calibrated agent, the rate at which it commits matches the rate at which it is right. Lower values are better; the metric becomes a binned ECE if a continuous confidence signal is supplied via att["confidence"], but none of our checkpoints expose one. Tool efficiency and turn efficiency. Let Sx(r)S_x^(r) be the number of SMT calls and Tx(r)T_x^(r) the number of agent iterations in attempt (x,r)(x,r). Then tool eff.=avg@NS¯,turn eff.=avg@NT¯,S¯=1MK∑x,rSx(r),T¯=1MK∑x,rTx(r). gathered tool eff.= avg@N S, turn eff.= avg@N T,\\ S= 1MK _x,rS_x^(r), T= 1MK _x,rT_x^(r). gathered (11) Both ratios are dimensionally correctness/compute-unit: tool efficiency is accuracy per SMT call, the marginal value of querying the solver; turn efficiency is accuracy per agent iteration, the marginal value of calling the model. Because Tx(r)≥Sx(r)+1T_x^(r)≥ S_x^(r)+1, each SMT call consumes an iteration and the final answer takes another, turn efficiency is always the smaller of the two; the gap reflects how much non-solver agent work is being done per problem. Wasted turns. For each correct attempt, let ιx(r) _x^(r) denote the smallest index i such that the i-th SMT call in the trace has ρx(r,i)∈sat,unsat, _x^(r,i)∈\ sat, unsat\, i.e., the earliest call that emitted a real Z3 verdict. Then wasted turns=x,r:χx(r)=1[max0,Sx(r)−ιx(r)−1], split wasted turns&=E_x,r: _x^(r)=1\\ & [ \0,S_x^(r)- _x^(r)-1\ ], split (12) the mean number of additional SMT calls the agent issued after an already-correct call’s verdict was returned. The metric captures retroactive exploration: it is invariant to how hard a problem was, only to whether the agent kept poking after the answer was implicitly already known. Lower is better; a value of zero indicates the agent commits the moment it has a real verdict. Unique skeletons. For each problem we compute the SMT skeleton, the sequence of top-level command tokens of each call, (declare-const,assert,check-sat,…),( declare-const, assert, check-sat,…), and count the number of distinct skeletons across the K attempts. The reported value is the mean of this count over D; we also report the mean pairwise Jaccard distance between the skeleton sets of two attempts on the same problem. Both are diversity measures: large values mean the agent explores qualitatively different solution shapes on resampling; small values mean it produces structurally homogeneous attempts. B.3 SMT-Program Quality Sample-based correctness metrics measure what answer the agent produced; SMT-program quality metrics measure how it got there. Each is a function of the SMT-LIB code and Z3 verdicts in the trace, defined first per-call, then per-attempt via the lift in Table 9, then aggregated over D. The per-attempt lift is materially important: an agent that emits a strong SMT call somewhere in its trace should not be penalized for also issuing weak exploratory calls, so we use disjunctions, e.g., “any non-trivial,” “any grounded,” and “any real verdict,” rather than averages over calls. Attribute Definition any non trivial ⋁i¬is trivial(zx(r,i)) _i \, is trivial(z_x^(r,i)) any grounded ⋁i(grounding(zx(r,i),x)≥λgnd) _i ( grounding(z_x^(r,i),x)≥ _gnd ) any real verdict ⋁i(sat resulti∈sat,unsat,unknown) _i ( sat result_i∈\ sat, unsat, unknown\ ) any unsat ⋁i(sat resulti=unsat) _i ( sat result_i= unsat ) first pass valid sat result1∈sat,unsat,unknown sat result_1∈\ sat, unsat, unknown\ max grounding maxigrounding(zx(r,i),x) _i grounding(z_x^(r,i),x) Table 9: Per-attempt structural attributes computed from the sequence of SMT calls (zx(r,1),…,zx(r,Sx(r)))(z_x^(r,1),…,z_x^(r,S_x^(r))) in trace τx(r) _x^(r). The grounding threshold is λgnd=0.25 _gnd=0.25. is trivial is the predicate defined in §B.3.2. B.3.1 Grounding The grounding score quantifies how much of the problem’s actual content the agent transferred into the formal SMT representation. We extract problem entities E(x)E(x) from the problem text x via the regular expression [A-Za-z][A-Za-z0-9 ]1, after lower-casing, then remove a small fixed list of ∼50 50 English stopwords plus generic task scaffolding tokens, e.g., question, answer, true, false, and option. For an SMT call z, the grounding score is the fraction of problem entities that appear as substrings in the lower-cased SMT body: gnd(z,x)=1|E(x)|∑e∈E(x)[e∈lc(z)], splitgnd(z,x)&= 1|E(x)| _e∈ E(x)1\! [e (z) ], split (13) where lc(z)lc(z) is the lower-cased SMT body. We use the convention gnd=0gnd=0 when |E(x)|=0|E(x)|=0, which is vanishingly rare in our datasets. Because the predicate “e is a substring of z” is permissive (it counts both declare-const e Int and any occurrence of e in a comment or sort name), grounding is a liberal measure of semantic transfer rather than a strict one, intentionally biased toward false positives so that the metric does not reward intentional obfuscation. The reported mean grounding is the per-attempt max grounding averaged over D. A grounding score of 0.050.05 on a problem with twenty named entities indicates the SMT references one of them: this is the decorative-SMT regime in which the agent has constructed a formally valid program that does not actually express the problem. A score of 0.50.5 indicates the SMT references roughly half the entities, sufficient for the program to be non-vacuous. The threshold λgnd=0.25 _gnd=0.25 used in Table 9 is empirically set: it cleanly separates inspection-verified decorative programs from inspection-verified content-loaded ones on a held-out development sample. B.3.2 Triviality An SMT call z is trivial if any of the following hold: 1. z is empty or whitespace. 2. z contains no declare-const, declare-fun, or define-fun, and contains fewer than two (assert ...) forms. 3. Every (assert ...) form in z matches a literal tautology or contradiction: (assert true)( assert true), (assert (= n n))( assert (= n n)) with n a numeric literal, (assert (not true))( assert (not true)), or (assert (not false))( assert (not false)). 4. z has fewer than 4040 non-whitespace characters and at most one assertion. The first three cases catch semantically empty SMT, i.e., programs that contain Z3 syntax but no problem content. The fourth case catches stub programs that initiate an SMT-LIB block but abandon it before encoding anything substantive. The trivial smt rate reported in tables is the fraction of attempts whose entire SMT call sequence is trivial: trivSMT=1NSMT∑(x,r)[⋀itriv(zx(r,i))], splittriv_SMT&= 1N_SMT _(x,r)1\! [ _itriv(z_x^(r,i)) ], split (14) where NSMTN_SMT is the number of attempts with at least one SMT call. A non-zero trivial-SMT rate is diagnostic of performative SMT: the agent emits Z3 calls to satisfy the tool-calling prior of its training distribution without actually using the solver to reason. B.3.3 First-Pass Z3 Validity The fraction of attempts, over those with at least one SMT call, whose very first invocation produced a real Z3 verdict: Z3=sat,unsat,unknown,rv=(x,r):ρx(r,1)∈Z3,SMT=(x,r):Sx(r)≥1,fpvZ3=|rv||SMT|. gatheredV_Z3=\ sat, unsat, unknown\,\\ A_rv=\(x,r): _x^(r,1) _Z3\,\\ A_SMT=\(x,r):S_x^(r)≥ 1\,\\ fpv_Z3= |A_rv||A_SMT|. gathered (15) This isolates whether the agent’s very first SMT-LIB emission is syntactically well-formed under SMT-LIB v2 and well-typed under the declared theory. A delta on this metric during post-training reflects improvements in surface-level SMT syntax (fewer malformed parentheses, undeclared symbols, and theory mismatches), not in reasoning depth. B.3.4 Verified-Correct Rate and its Unsat Restriction We now define the strictest accuracy measure used in this work. An attempt is verified-correct if the conjunction VCx(r):= _x^(r):= χx(r) _x^(r) (16) ∧any real verdictx(r) any real verdict_x^(r) ∧any groundedx(r) any grounded_x^(r) ∧any non trivialx(r) any non trivial_x^(r) holds, and verified-correct under unsat if it further satisfies any unsatx(r) any unsat_x^(r). The aggregate rates are vcr =1MK∑x,rVCx(r), = 1MK _x,rVC_x^(r), (17) vcrunsat _ unsat =1MK∑x,r(VCx(r)∧any unsatx(r)). = 1MK _x,r (VC_x^(r) any unsat_x^(r) ). vcrvcr filters out four distinct failure modes that can all produce a passing χx(r)=1 _x^(r)=1: • No real verdict: the agent answered correctly without ever obtaining a sat/unsat/unknown verdict from Z3, i.e., all calls errored or produced no verdict. • Decorative SMT: the agent obtained a verdict but the program had grounding below λgnd _gnd, i.e., the SMT did not reference the problem. • Trivial SMT: every call was structurally trivial. • The conjunction held but on a vacuous verdict: e.g., a sat verdict on the empty constraint set. Of these the most dangerous is the no-real-verdict case: it indicates a model that answers correctly via natural-language reasoning while only performing SMT use. The post-training vcrvcr delta measures the shift from performative to real solver use. vcrunsatvcr_ unsat goes further by requiring that at least one SMT call in the trace returned unsat. By the discussion in §A.1, this is the refutational-proof restriction: the agent must have attempted to derive a contradiction from the negation of its candidate answer, and the solver must have confirmed it. The pair (vcr,vcrunsat)(vcr,vcr_ unsat) therefore separates correctness into three regimes: (i) correct but performative; (i) verified-correct via sat witness, i.e., model-finding; and (i) verified-correct via unsat, i.e., refutational proof. B.3.5 Z3 Outcome Distribution For diagnostic and downstream analysis purposes, we additionally report the distribution of Z3 outcomes across every SMT call in the sweep: ωZ3=(ωsat,ωunsat,ωunknown,OPENωerror,ωno-verdict), gatheredω^Z3= ( _ sat, _ unsat, _ unknown,\\ _ error, _ no-verdict ), gathered with ωuZ3ω^Z3_u the fraction of all SMT calls whose sat result took value u. We treat no verdict, where the call succeeded but no sat result token appeared in stdout, as distinct from error, where the call raised an exception or returned a non-zero exit. Appendix C Comparison to Open-Weight Baselines We additionally compare the DPO-tuned Sequent-Prover checkpoints against external open-weight baselines evaluated with the same SMT-scratchpad harness. The external baselines are Gemma-4B, GPT-OSS-20B, and GPT-OSS-120B. All deltas are Qwen-DPO minus the external model. Positive values indicate that the Qwen-DPO checkpoint is higher, except for lower-is-better diagnostic rates, such as the trivial-SMT rate, where the raw signed delta is still shown. Aggregate correctness. Table 10 reports macro-averaged deltas over the shared canonical datasets. The 4B comparison shows a large separation from Gemma-4B: Qwen-4B-DPO improves avg@N by +0.647+0.647, pass@4 by +0.524+0.524, and pass^4 by +0.640+0.640. The GPT-OSS-20B comparisons show the same pattern at a larger external baseline: Qwen-27B-DPO improves avg@N by +0.326+0.326 and pass^4 by +0.648+0.648, while Qwen-9B-DPO improves avg@N by +0.287+0.287 and pass^4 by +0.567+0.567. Against GPT-OSS-120B, the comparison is closer and therefore more informative: Qwen-27B-DPO remains positive on all correctness aggregates, including +0.027+0.027 avg@N, +0.021+0.021 pass@4, and +0.036+0.036 pass^4; Qwen-9B-DPO is close on coverage, with +0.006+0.006 pass@4 and +0.002+0.002 AUC@4, while GPT-OSS-120B has the advantage on avg@N and pass^4. 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 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. Verifier-use diagnostics. Table 11 compares solver-facing behavior. The largest gains are in the verified-correct rate, UNSAT-restricted verified-correct rate, and grounding. Qwen-4B-DPO improves verified-correct rate by +0.615+0.615 relative to Gemma-4B. Against GPT-OSS-20B, both Qwen-27B-DPO and Qwen-9B-DPO improve the verified-correct rate by +0.487+0.487. The GPT-OSS-120B comparison is particularly useful because it separates answer-level strength from verifier-use quality: Qwen-27B-DPO improves verified-correct rate by +0.341+0.341 and grounding by +0.274+0.274, while Qwen-9B-DPO improves verified-correct rate by +0.349+0.349 and grounding by +0.299+0.299. Trivial-SMT rate decreases in all five comparisons, indicating that the DPO checkpoints emit fewer structurally empty or decorative SMT programs. Comparison Sound. Recov. VCR VCR-U FP-Z3 Triv. SMT ↓ 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 Table 11: Macro-averaged verifier-use deltas. Sound. is P(correct∣finish)P(correct ); 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. Per-dataset breadth. Table 12 reports polarity-adjusted win/loss/tie counts across shared datasets. The Qwen-DPO checkpoints dominate the 4B and 20B external baselines across the main sample-based metrics: pass^4 and maj@4 win on every shared dataset in the Gemma-4B and GPT-OSS-20B comparisons. The GPT-OSS-120B comparison is more balanced. Qwen-27B-DPO wins avg@N on 28 of 35 datasets and pass^4 on 24 of 35 datasets, with five pass^4 ties. Qwen-9B-DPO remains competitive on coverage, winning pass@4 on 22 of 33 datasets, while GPT-OSS-120B has the stronger all-sample consistency profile. 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 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-level trends. Table 13 groups the avg@N deltas by benchmark category. Qwen-DPO is substantially ahead of Gemma-4B and GPT-OSS-20B in every category. Against GPT-OSS-120B, Qwen-27B-DPO is strongest on AGIEval, NLI/MCQ, and hard-reasoning categories, and remains close on arithmetic and free-form QA. The 9B-DPO comparison to GPT-OSS-120B is near parity for AGIEval, arithmetic, hard reasoning, and NLI/MCQ, with larger gaps on spatial and free-form QA tasks. 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 Spatial +0.341 +0.143 +0.110 −-0.037 −-0.071 Table 13: Mean avg@N delta by dataset category. Values are macro-averages over shared canonical datasets in each category. These external comparisons support two conclusions. First, Sequent-Prover DPO checkpoints are substantially stronger than the same-scale or moderately larger open-weight baselines under the SMT-scratchpad evaluation, with especially large advantages in pass^4 and verifier-grounded correctness. Second, the comparison with GPT-OSS-120B shows that the 27B DPO checkpoint is competitive with a much larger open-weight model on answer-level metrics, while retaining a clear advantage in the use of executable, grounded solvers. Appendix D Additional Analyses This section gives full tables and details behind the main results: pool composition and per-category results, the test-time sampling study, grounding without comments, structural uncertainty of the generated SMT, teacher support, and soundness. D.1 Pool Composition and Per-Category Results Each benchmark contributes 200 problems, except ProofWriter, which contributes 54 because of a data-loader bug. This gives 36×200+54=7,25436× 200+54=7,254 problems per family. Table 14 groups the pool by category. Table 15 reports Base, SFT, and DPO results within each category. Values are micro-averages over the problems in each category, using the same four trajectories per problem as the main results. 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 AGIEval 4 800 11.03 Total 37 7,254 100.00 Table 14: Composition of the 37-benchmark evaluation pool. avg@N ↑ pass^4 ↑ 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 Other 0.950 0.988 0.997 0.815 0.950 0.988 AGIEval 0.900 0.955 0.970 0.729 0.863 0.911 9B Hard reasoning 0.853 0.938 0.951 0.687 0.859 0.871 Arithmetic 0.979 0.988 0.989 0.945 0.970 0.973 Spatial 0.896 0.891 0.916 0.707 0.712 0.777 NLI/MCQ 0.968 0.987 0.987 0.887 0.959 0.960 Free-form QA 0.987 0.993 0.997 0.949 0.978 0.989 Other 0.973 0.992 0.996 0.905 0.968 0.988 AGIEval 0.953 0.976 0.976 0.863 0.911 0.914 27B Hard reasoning 0.967 0.974 0.992 0.924 0.926 0.976 Arithmetic 0.996 0.996 0.998 0.993 0.988 0.994 Spatial 0.962 0.945 0.974 0.912 0.858 0.923 NLI/MCQ 0.998 0.998 0.999 0.993 0.994 0.995 Free-form QA 1.000 0.999 0.999 1.000 0.996 0.995 Other 0.999 0.999 1.000 0.998 0.998 1.000 AGIEval 0.998 0.993 0.997 0.988 0.980 0.990 Table 15: Per-category results for Base, SFT, and DPO checkpoints. Values are micro-averages over the problems in each category. Hard reasoning has the largest within-category gain at 4B (+0.493 pass^4). NLI/MCQ, the largest category, also contributes strongly. At 27B, most categories are near ceiling. The remaining gains are in hard reasoning and spatial reasoning, with small changes on saturated categories. D.2 Post-Training versus Test-Time Sampling We compare post-training with a larger test-time sampling budget. We fix 180 held-out problems, 30 each from ProntoQA, FOLIO, AR-LSAT, GSM8K, StepGame, and ARC-Challenge. We draw 16 trajectories per problem from the 4B base model and from the post-trained 4B model. We also draw four trajectories per problem with decomposed prompting, least-to-most prompting, and self-refinement on the base model. All methods share the solver harness, temperature 0.9, a limit of ten agent iterations, the answer checker, and the problem list. The study contains 7,920 trajectories. Table 16 reports equal-weight macro-averages over the six families. Intervals are stratified 95% bootstrap intervals over problems (10,000 resamples). Method K Accuracy [95% CI] ↑ pass@K ↑ pass^K ↑ Stab. ↑ Tokens/problem ↓ Cost ↓ Base + self-consistency 1 0.657 [0.623, 0.689] 0.657 0.657 1.000 27,729 1.7× Base + self-consistency 2 0.657 [0.623, 0.689] 0.780 0.533 0.683 55,458 3.3× Base + self-consistency 4 0.657 [0.623, 0.689] 0.848 0.395 0.466 110,915 6.6× Base + self-consistency 8 0.657 [0.622, 0.689] 0.887 0.257 0.290 221,831 13.3× Base + self-consistency 16 0.657 [0.623, 0.689] 0.911 0.139 0.152 443,662 26.5× Base + decomposed 4 0.590 [0.550, 0.629] 0.828 0.267 0.322 117,070 7.0× Base + least-to-most 4 0.621 [0.578, 0.661] 0.828 0.317 0.383 121,933 7.3× Base + self-refine 4 0.772 [0.733, 0.811] 0.928 0.572 0.617 219,491 13.1× Post-trained 4B 1 0.869 [0.836, 0.899] 0.869 0.869 1.000 16,718 1.0× Post-trained 4B 2 0.869 [0.835, 0.899] 0.924 0.813 0.880 33,437 2.0× Post-trained 4B 4 0.869 [0.836, 0.900] 0.948 0.743 0.784 66,873 4.0× Post-trained 4B 8 0.869 [0.836, 0.900] 0.960 0.663 0.690 133,747 8.0× Post-trained 4B 16 0.869 [0.835, 0.900] 0.967 0.572 0.592 267,493 16.0× 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=1K=1. Beyond the results in Section 3.4, at matched K=4K=4 the post-trained model also improves accuracy by 21.2 points and majority-vote accuracy by 9.9 points over base self-consistency. Against the base model at K=16K=16, majority-vote accuracies are statistically similar, but the base model needs 6.6× more tokens to get there. Decomposed and least-to-most prompting do not improve over base self-consistency on this mixture. D.3 Grounding without Comments Grounding (Eq. 13) counts entity names anywhere in the SMT body, including comments. Comments often hold the only readable mapping from short SMT symbols to problem entities. For example, an AR-LSAT trace may name people J and K in code and explain them in comments. Still, a model could in principle raise grounding by writing entity names in comments. Grounding is not part of any training reward; it is only a filter for Gold traces. To test this concern, we strip comments and recompute grounding on about 50k trajectories from the runs in the main paper. Table 17 shows that post-trained models still have higher grounding than their base models. Family SFT −- Base DPO −- Base 4B +0.074 +0.081 9B +0.051 +0.051 27B +0.039 +0.036 Table 17: Change in mean grounding after removing SMT comments. D.4 Structural Uncertainty of SMT Programs Full semantic validation of a formalization is not possible in general (see Limitations). As a symbolic proxy, we follow Ganguly et al. (2026), who show that structural variation in sampled SMT-LIB programs predicts autoformalization errors. We ask whether post-training reduces this structural uncertainty. For task x and independent trajectory j, let sx,js_x,j be its final parseable SMT call. We parse sx,js_x,j with the SMT-LIB ANTLR grammar and count each grammar production r, giving counts cx,j(r)c_x,j(r) and the distribution Px,j(r)=cx,j(r)/∑r′cx,j(r′)P_x,j(r)=c_x,j(r)/ _r c_x,j(r ). The lexer drops comments, and all identifiers map to one token class. The measure is unchanged by comments or renaming, but it is sensitive to declarations, quantifiers, operators, and term structure. We compare two distributions with the Jensen–Shannon divergence JSDJSD in base 2, so JSD∈[0,1]JSD∈[0,1]. A value of zero means equal production frequencies. It does not imply identical syntax trees or semantics. Across trajectories. For trajectory j, we pool the counts of its peers into P¯x,−j(r)=∑i≠jcx,i(r)/∑i≠j∑r′cx,i(r′) P_x,-j(r)= _i≠ jc_x,i(r)/ _i≠ j _r c_x,i(r ) and score Dx,j=JSD(Px,j∥P¯x,−j)D_x,j=JSD(P_x,j\,\|\, P_x,-j). The scored program never enters its own reference. We require at least two parsed peers and average Dx,jD_x,j within each task to get DxD_x. Within a trajectory. For a trajectory with L≥2L≥ 2 parseable SMT calls with distributions P(1),…,P(L)P^(1),…,P^(L), we measure first–last drift JSD(P(1)∥P(L))JSD(P^(1)\,\|\,P^(L)) and mean adjacent drift 1L−1∑ℓ=1L−1JSD(P(ℓ)∥P(ℓ+1)) 1L-1 _ =1^L-1JSD(P^( )\,\|\,P^( +1)). For each measure we average over eligible trajectories in a task and report the paired task-level change Δ=x[Dxtuned−Dxbase] =E_x[D_x^tuned-D_x^base]. Negative values mean lower structural variation after post-training. Across traj. Within traj. Comparison Δ [95% CI] ↓ First–last ↓ Adjacent ↓ 4B Base→ −0.023-0.023 [−0.025-0.025, −0.021-0.021] −0.029-0.029 −0.011-0.011 4B Base→ −0.019-0.019 [−0.021-0.021, −0.016-0.016] −0.027-0.027 −0.008-0.008 9B Base→ −0.019-0.019 [−0.021-0.021, −0.017-0.017] −0.024-0.024 −0.010-0.010 9B Base→ −0.016-0.016 [−0.018-0.018, −0.015-0.015] −0.026-0.026 −0.010-0.010 27B Base→ −0.008-0.008 [−0.010-0.010, −0.006-0.006] −0.006-0.006 −0.005-0.005 27B Base→ −0.004-0.004 [−0.006-0.006, −0.002-0.002] −0.011-0.011 −0.006-0.006 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. In Table 18, the drop in peer divergence is largest at 4B and 9B and smaller at 27B, whose base model is already stable. Both within-trajectory drifts also fall in all six comparisons, so tuned models make smaller structural revisions during repair. D.5 Teacher Support and Student Capability SFT imitates the teacher conditioned on success, pT(τ∣x,A(x,y⋆,τ)=1)p_T(τ x,A(x,y ,τ)=1) (Section 2). With KTK_T samples, at least one accepted trace appears with probability 1−(1−ZT(x))KT1-(1-Z_T(x))^K_T. The student is bounded by the teacher’s support over successful strategies. The same idea underlies expert iteration, where an expensive search procedure produces behavior that a policy learns to reproduce (Ren et al., 2025). It explains why the students exceed the teacher’s all-sample reliability on AR-LSAT (Section 3.6, Table 8). The students learn reusable steps, such as datatype encodings and push/pop option testing (Appendix E.4, E.5). The teacher is weak on some SMT fragments, such as fixed-size bit-vector arithmetic. Our benchmarks do not test these fragments, and a stronger teacher there would extend the same recipe. D.6 Soundness after SFT Soundness is the accuracy of attempts on which the agent chooses to finish (Eq. 7). All SFT demonstrations are successful traces that end cleanly. This may teach the model to commit early, which would lower soundness. We do not see a broad drop in reliability that would confirm this effect. After DPO, soundness improves, together with fewer malformed SMT calls and more refutational solver use (Table 5(b)). Appendix E Qualitative Improvements The quantitative improvements we observe in our metrics, such as verified correct rate with unsat (i.e., appropriate proof by contradiction) correlate to formalizations that, on manual inspection, follow the problem statement much more closely. Throughout the harness and metric development, as well as during intermediate checkpoints, we took care to ensure there is no reward hacking and quantitative improvements actually manifest via qualitative improvements in formal artifact quality. In this section, we attempt to elucidate a few learnt capabilities in our trained models. E.1 Capability 1: SMT-LIB language fluency The most basic gap is that the 4B Qwen Base model emits malformed SMT-LIB on the first attempt and rarely recovers, whereas Sequent-Prover-4B recovers in one turn. We illustrate with ProntoQA-95 (gold = B): a chain of universal implications resolves to “Stella is not feisty.” Qwen-4B. The first tool call is itself malformed at the envelope level: the model wraps its payload as "arguments":"\"smt_code\":\"...\"", which the harness’s JSON-strict tool parser cannot decode, so the next tool message is empty. Inside the inner payload the SMT-LIB is also incorrect: ⬇ (set-logic QF_LIA) (declare-const IsFeisty Pred) (declare-const IsVumpus Pred) (declare-const Stella Bool) (assert (= (IsVumpus Stella) True)) (assert (forall ((x Pred)) (=> (= (IsVumpus x) True) (= (IsDumpus x) True)))) Several things are wrong: Pred is not a sort, IsVumpus is declared as a constant but applied as a function, Stella is a Bool but used as an individual, and True appears as a value rather than the SMT-LIB literal true. Over the next eight turns the model loses track of the original problem and cycles through (set-logic QF_LIA), (set-logic QF_BV), (set-logic QF_NIA), and (set-logic QF_ARITH), the last of which is not a recognized logic name. It exhausts its 10-turn budget without emitting finish. Sequent-Prover-4B. The first tool call is a first-order encoding with a sort for animals and one predicate per type: ⬇ (declare-sort Animal) (declare-fun vumpus (Animal) Bool) (declare-fun dumpus (Animal) Bool) (declare-fun rompus (Animal) Bool) ;; ... (one declare-fun per category) ... (declare-const Stella Animal) (assert (forall ((x Animal)) (=> (vumpus x) (dumpus x)))) ;; ... the full implication chain ... (assert (forall ((x Animal)) (=> (zumpus x) (not (feisty x))))) (assert (vumpus Stella)) (assert (feisty Stella)) ; proof by contradiction (check-sat) ; --> unsat The first pass surfaces two ordering errors (yumpus and floral are used before they are declared). The Sequent-Prover-4B model reads the Z3 error, hoists the missing declare-funs to the top, re-runs, and finishes in four turns. The base model, given the same kind of error, could not localize the fix and drifted into unrelated probes. E.2 Capability 2: First-order over propositional encoding When a problem quantifies over individuals, a propositional encoding (one boolean per ground proposition) often forces the model to fill in unstated relations by hand. The base model does this routinely; Sequent-Prover does not. Example: FOLIO-1361 (gold = Uncertain). Premises describe animals near a campus and ask whether “Rockie is a turtle.” The critical step is to notice that the premises constrain Rockie to be a rabbit or a squirrel but say nothing about whether rabbit and turtle are disjoint categories. Qwen-4B. Declares one Bool per (Rockie, property) pair, with no animal sort. Lacking a way to express “the only animals spotted are rabbits and squirrels” as a universal, it instead injects two disjointness axioms that are nowhere in the premises: ⬇ ; Assumption: Rabbits and turtles are mutually exclusive (assert (=> RockieRabbit (not RockieTurtle))) ; Assumption: Squirrels and turtles are mutually exclusive (assert (=> RockieSquirrel (not RockieTurtle))) With those injected axioms, the negation of the conclusion becomes unsat and the base model answers “False”, but the false answer is caused by the hallucinated premise, not by the actual problem. Sequent-Prover-4B. Uses a sort Animal and universally quantified predicates over animals; the conditions in the prompt translate mechanically. We discuss Sequent-Prover’s full reasoning trajectory under Capability 6 below, because it turns on the same diagnostic move used in another problem. E.3 Capability 3: Bidirectional satisfiability for ternary verdicts When the verdict space is ternary (True / False / Uncertain) or four-valued (entailment / contradiction / neutral / self-contradiction), a single satisfiability query is not enough. The textbook idiom is two queries: assert the conclusion, then assert its negation. The base model asks one and stops; Sequent-Prover-4B asks both. Example: FOLIO-476 (gold = False). “Tom will rent at the Olive Garden,” under premises constraining the deposit to be at least the monthly rent ($2000) and renting to require deposit ≤$1500. Qwen-4B. Spends three turns repairing surface syntax (Boolean→ ; -> to implies; (= oliveWillRent False)→(not oliveWillRent)). Its single satisfiability query is on the negation of the conclusion, which is sat, so it concludes “the conclusion does not necessarily follow” and answers Uncertain. It never asks the dual question. Sequent-Prover-4B. Runs both queries: ⬇ ;; First: can the conclusion FAIL under the premises? (assert (not (and allowed_to_move_in_with_fluffy (<= deposit_at_olive 1500.0)))) (check-sat) ; sat ==> not forced True ;; Second: can the conclusion HOLD under the premises? (assert (and allowed_to_move_in_with_fluffy (<= deposit_at_olive 1500.0))) (check-sat) ; unsat ==> forced False (sat, unsat) is the signature of a forced-false conclusion. Sequent-Prover-4B finishes with False and the explanation reproduces the informal argument: “$2000 >> $1500, so the deposit condition cannot be satisfied at the Olive Garden.” Both models know check-sat. Sequent-Prover-4B differs in its choice of which experiment to run next. E.4 Capability 4: Declarative encoding via datatypes For problems with explicit finite enumerations (LSAT analytical reasoning, ZebraLogic), the canonical idiom is declare-datatypes for each finite domain and a function from one to another. Example: AR-LSAT-82 (gold = E). Seven sales reps assigned to three zones, with same-zone pairings and an XOR-style either-but-not-both rule. “If more reps work in Zone 1 than in Zone 3, which one of the following could be true?” Qwen-4B. Encodes zones as unbounded integers and emits a wall of errors over all ten turns. The actual bugs we observe across calls are: bare <= 1 zone_Kim 3 expressions at top level (outside any assert); ad-hoc [zone_Kim] bracket syntax; (select zone_Kim 1) on a Bool as if to extract an indicator; the conjunction (and (= zone_Kim 1) (= zone_Kim 2) (= zone_Kim 3)) used where the intent is disjunction; (if ...) instead of (ite ...); and a multi-variable declare, (declare-const zK zM zP zQ zS zT zU Int), which is not legal SMT-LIB. None of these get repaired; each turn re-issues a near-copy of the previous one. The model never reaches the option-testing stage. Sequent-Prover-4B. First turn uses two algebraic datatypes and an abstract assignment function: ⬇ (declare-datatypes () ((Rep Kim Mahr Parra Quinn Stuckey Tiao Udall))) (declare-datatypes () ((Zone Zone1 Zone2 Zone3))) (declare-fun zone (Rep) Zone) (assert (xor (= (zone Parra) Zone1) (= (zone Tiao) Zone1))) ; rule 1 (assert (xor (= (zone Tiao) Zone2) (= (zone Udall) Zone2))) ; rule 2 (assert (= (zone Parra) (zone Quinn))) ; rule 3 (assert (= (zone Stuckey) (zone Udall))) ; rule 4 (define-fun count1 () Int (+ (ite (= (zone Kim) Zone1) 1 0) (ite (= (zone Mahr) Zone1) 1 0) ;; ... ite per rep ... )) The first pass writes (not = =) (the constraint is “exactly one of X, Y”) and gets a Z3 arity error; the next turn replaces the offending subtree with xor. This is the same local-edit recovery pattern as in Capability 1. E.5 Capability 5: Push/pop for multi-option queries LSAT analytical-reasoning items ask “which of the following could / must be true?” This is a sequence of independent satisfiability tests on a shared base theory, the SMT idiom is push/pop. Example: AR-LSAT-60 (gold = E). Four riders and four bicycles across two days, with same-day distinctness and cross-day pairing. “If Theresa tests G on day 2, which one of the following must be true?” Qwen-4B. Across all ten turns the same family of errors recurs. Seven of the ten calls contain (assert (= T1 H) or (= T2 H)), with or as a top-level token outside the assert, which Z3 reports as “invalid assert command, ) expected.” The base model treats the error as a request to reformat the body (one call collapses the entire program onto a single line; another swaps in unbounded integer ranges), but never rewrites the offending node as the prefix expression (or (= T1 H) (= T2 H)). It never reaches the option-testing stage, and extraction_method = none. Sequent-Prover-4B. A single first-turn body emits five push/pop blocks, one per answer choice. Each block asserts the negation of the choice: the canonical pattern for “must be true” (if the negation is unsat, the choice must hold). (echo ...) labels the output so the five results are self-describing. ⬇ (declare-datatypes () ((Rider R Seamus T Yuki))) (declare-datatypes () ((Bike F G H J))) (declare-fun d1_rider (Bike) Rider) (declare-fun d2_rider (Bike) Rider) (assert (distinct (d1_rider F) (d1_rider G) (d1_rider H) (d1_rider J))) ;; ... base theory ... ;; Yuki’s day-1 bike is Seamus’ day-2 bike: (assert (exists ((b Bike)) (and (= (d1_rider b) Yuki) (= (d2_rider b) Seamus)))) (echo "Testing (A): Reynaldo tests H, day 1") (push) (assert (not (= (d1_rider H) R))) (check-sat) (pop) ;; ... (B), (C), (D) similarly ... (echo "Testing (E): Yuki tests H, day 2") (push) (assert (not (= (d2_rider H) Yuki))) (check-sat) (pop) The single Z3 reply ends with “Testing (E) … unsat,” the unique negation that is unsat, so (E) is the choice that must hold. Sequent-Prover finishes in three iterations, having issued one comprehensive query instead of five separate ones. Three sub-skills are bundled into this first turn: (i) scaffolding with (echo ...) so the Z3 output is self-describing; (i) knowing which direction to negate for “must” vs. “could” questions; (i) knowing that push/pop make the five queries independent. Note also the encoding choice: inverting the natural direction to d1_rider : Bike → Rider lets the day-1 distinctness collapse to a single distinct call instead of six pairwise inequalities, and lets the cross-day pairing be expressed as a one-variable existential. E.6 Capability 6: Diagnosing inconsistent premise sets A further capability is noticing that both directions of a hypothesis are unsatisfiable, and inferring from that signature that the premise set itself is inconsistent. This move appears in two superficially unrelated transcripts. Example A: Self-Contradiction We used an example where there were twelve atomic facts and twelve quantified rules over seven named people. The base model spends ten turns rewriting an 80-line SMT body, hitting the same family of errors each time (missing Harold_brainy declaration, mis-parenthesized rules 4 and 9). At turn 22 the harness sends a follow-up nudge, “Z3 returned a clean UNSAT result, so now emit the finish tool call”, but the base ignores it and issues yet another z3_solve on turn 23. Sequent-Prover-4B arrives at the verdict in three steps. First, it tests both directions of the hypothesis: ⬇ ;; (a) Is the hypothesis decidable? (push) (assert R_huge) (check-sat) (pop) ; unsat (push) (assert (not R_huge)) (check-sat) (pop) ; unsat Both unsat is the diagnostic signature of an inconsistent premise set. Sequent-Prover-4B confirms by querying the premises alone: ⬇ ;; (b) Are the premises consistent? ;; ... (only premises asserted) ... (check-sat) ; unsat and finishes with self_contradiction. The explanation it produces names the diagnostic explicitly: “Z3 returns UNSAT for the premises alone, and both R_huge and (not R_huge) are UNSAT when added to the premises. This means the premises contain an inherent contradiction.” Example B: FOLIO-1361, revisited. Recall that the base model on this problem (§E.2) injected ad-hoc disjointness between rabbits, squirrels, and turtles and got an unsound “False.” Sequent-Prover’s trajectory uses the same diagnostic move as Example A: 1. No injected axioms; both directions of (turtle Rockie) return sat. (Sequent-Prover-4B does not yet realize this is the “Uncertain” answer.) 2. Adds disjointness axioms; the negation goes unsat, suggesting the conclusion is forced True. 3. Runs both push/pop queries on the disjointness-augmented theory: both are unsat. 4. Recognizes both-unsat as a contradiction signature, checks the augmented premises alone, gets unsat. 5. Concludes the disjointness axioms are not licensed; removes them. 6. Re-runs both directions: sat and sat. 7. Finishes with Uncertain and a verbal argument: “The premises do not state that rabbits and turtles are disjoint categories.” The same meta-strategy, both UNSAT ⇒ suspect your own axioms, recovers the correct answer on a problem where the base model is led astray by the axioms it injected. This strategy spans several solver calls, and the model learns it as a policy over them. E.7 Capability 7: Error text as actionable feedback The recovery patterns we observe in Sequent-Prover-4B follow a recurring structure: read the Z3 error string, locate the named node in the previous body, and patch it without disturbing the rest of the program. The base model either re-emits a near-identical body or escalates the change in unhelpful directions (switching logics, collapsing onto one line). Three mini-patterns: ProntoQA-95. Error: “unknown constant yumpus (Animal).” Fix: move (declare-fun yumpus (Animal) Bool) above its first use. Nothing else changes. FOLIO-476. Error: “unknown sort Boolean.” Sequent-Prover-4B patches each occurrence to Bool in one turn. The base model takes two extra turns to also re-discover that -> is not a keyword (use => or implies) and that the constant is lower-case false. AR-LSAT-82. Error: “Wrong number of arguments (2) passed to function not.” Fix: replace the entire (not (= ...) (= ...)) subtree with (xor (= ...) (= ...)), which is both shorter and correct. The base model knows the SMT-LIB tokens. It does not use the parse tree, symbol table, or scopes to locate an error, and it retries the whole program instead.