PaperlayerView exact revision on arXiv

Source-linked AI summary

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

arXiv:2610.15258v1cs.CLcs.AIcs.LGcs.LO

TL;DR

Solver access alone cannot ensure reliable reasoning because a solver may check a misformalized task. Sequent-Prover trains agents from curated, verifier-supported trajectories; post-training improves answer accuracy and reliability across model scales.

  • Problem

    A solver verifies only the formal artifact it receives, so omitted premises or other misformalizations can produce valid results for the wrong problem.

    Source: §1 · p. 1

  • Method

    Sequent-Prover samples teacher trajectories, curates correct and executable traces with grounded, non-trivial evidence, then applies supervised fine-tuning and trajectory-level preference optimization.

    Source: §1 · p. 2, §2.4 · p. 5

  • Results

    Post-training improves accuracy and reliability across model scales; for 4B, DPO raises avg@N from 0.856 to 0.970.

    Source: §3.1 · p. 6, §5 · p. 9

  • Takeaways & Limitations

    Post-training turns sample-dependent solver successes into more stable behavior, with more grounded, non-vacuous programs and more correct traces backed by refutational UNSAT evidence.

    Source: §5 · p. 9

    No automatic check can certify that a formal artifact preserves meaning, and choosing the right level of formal abstraction remains open.

    Source: §6 · pp. 9–10

Abstract

from arXiv · show

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

Fluent multistep reasoning is not executable evidence, and SMT checks can fail when a task is misformalized. Sequent-Prover trains agents to construct grounded, executable formalizations through solver interaction.

1 Introduction

  • Figure 1 shows Sequent-Prover turning an underspecified commonsense claim into a grounded, checkable inconsistency.Source: Figure 1 · p. 1
  • Natural-language tasks can be misformalized, so a solver may correctly check an artifact that omits premises or encodes the wrong problem.Reliable verifier use therefore requires grounded, non-vacuous, executable formalizations built through multi-turn tool use.Source: §1 · p. 1
  • Sequent-Prover uses solver interaction as a training substrate, filtering candidate traces and turning supported ones into supervised and preference data.The resulting agents write more grounded, non-trivial, executable SMT programs.Source: §1 · p. 2
  • Post-training improves multi-sample reliability, SMT-LIB quality, refutational reasoning, and—especially with DPO—stability and efficiency beyond SFT.DPO-tuned agents solve problems earlier, with fewer tokens and solver-interaction rounds per correct answer.Source: §1 · p. 2

2 Methodology

Sequent-Prover bootstraps verifier-mediated reasoning from successful teacher trajectories, formalizes tasks as SMT obligations, and trains agents to use solver feedback, repair artifacts, and finish with answers. Its pipeline combines trace curation, supervised learning, and trajectory-level preference optimization.

2 Methodology

  • Verifier-conditioned trajectory distillation samples teacher traces, retains correct and executable traces with grounded, non-trivial evidence, then trains with SFT and trajectory-level DPO.The successful tail teaches verifier-mediated search behavior that the teacher produces only sporadically.Source: §2 · p. 2

2.1 Problem Formulation

  • Entailment requires a satisfiable formalized context and an unsatisfiable context conjoined with the negated claim.Context consistency and claim compatibility are checked separately through SAT queries.Source: §2.1 · p. 2

2.2 The SMT Scratchpad Interface

  • The SMT-LIB scratchpad exposes z3-solve and finish, letting agents execute scripts, inspect solver observations, revise artifacts, and terminate with an answer.Accepted traces must include an executable, non-trivial, input-grounded program that obtains a real solver verdict.Source: §2.2 · pp. 2–3

2.3 Verifier Feedback and Trace Semantics

  • Verifier feedback distinguishes inconsistent contexts, entailed or contradictory claims, possible claims, and unresolved executions; SAT may provide a witness, while UNSAT supplies refutational evidence.Errors, timeouts, and unknown results remain unresolved rather than receiving a semantic status.Source: §2.3 · p. 3
  • Teacher rollouts are curated into Gold, Silver, or Rejected traces: only correct answers with executable, grounded, non-vacuous evidence become Gold demonstrations.Gold traces define the success-conditioned target, while weaker or failed traces remain contrastive signals.Source: §2.3 · pp. 3–4

2.4 Training

  • SFT imitates model-generated actions in accepted traces, conditioning on solver observations while masking those observations from the prediction loss.This trains the action patterns for constructing evidence, responding to feedback, and committing to an answer.Source: §2.4 · pp. 4–5
  • DPO contrasts accepted trajectories with Silver or Rejected alternatives, increasing preference for verifier-supported traces over weakly supported or failed behavior.Silver traces can reach the correct answer but provide weaker scratchpad support.Source: §2.4 · p. 5
  • When the teacher has nonzero probability of an accepted trace, sampling more rollouts raises the chance of finding one; inference then uses the same scratchpad protocol and evaluates multiple trajectories.At test time, agents generate tool actions until finish or the interaction budget, and evaluation retains the full trajectory for process analysis.Source: §2.4 · p. 5

3 Results

The evaluation covers nine checkpoints across 37 benchmarks and 7,254 problems per model family, using multi-sample reliability alongside accuracy and solver-process measures. Post-training improves aggregate reliability, training-stage comparisons, test-time efficiency, and results across tasks and scales.

3.1 Aggregate accuracy and reliability

  • 4B DPO raises avg@N from 0.856 to 0.970 and pass^4 from 0.641 to 0.917; 9B pass^4 rises from 0.858 to 0.934, while 27B reaches 0.986.The comparison uses each model family’s base checkpoint as its baseline.Source: Table 1 · p. 6, §3.1 · p. 6
  • 4B DPO reaches 0.970 at pass@1, matching 4B base pass@4; stability rises from 0.661 to 0.919 for 4B and from 0.863 to 0.936 for 9B.pass^4 measures whether all four samples are correct, unlike pass@4, which measures whether at least one succeeds.Source: §3 · p. 5, §3.1 · p. 6

3.2 Problem-level consistency transitions

  • 86.7% of 4B and 78.7% of 9B problems with one to three correct base attempts become correct on all four DPO attempts.DPO retains 96.5%, 96.2%, and 99.3% of already reliable 4B, 9B, and 27B problems, respectively.Source: §3.2 · p. 6

3.3 Training-stage ablation

  • DPO improves every compared family on avg@N, pass^4, stability, and verified-correct rate; at 27B it adds +0.012 macro pass^4 over SFT.The 4B SFT and DPO models each solve 7,213 problems at least once, with 25 DPO-only and 8 SFT-only problems.Source: §3.3 · p. 6, Table 2 · p. 7

3.4 Test-time sampling and data ablations

  • At K = 4, post-training raises pass@4 by 10.1 points and pass^4 by 34.8 points over base self-consistency, while using fewer tokens.On five hard held-out benchmarks, answer-only SFT reduces pass^4 from 0.409 to 0.126; the full recipe leads on avg@N and pass@4.Source: §3.4 · p. 7, Table 3 · p. 7, Table 4 · p. 7

3.5 Solver-agent process quality

  • 4B DPO cuts average SMT calls from 4.10 to 2.52 and tokens per attempt from 18.97k to 12.72k.First verified-correct signals arrive earlier, and SMT errors fall from 41.3% to 19.0% for 4B; UNSAT calls rise from 12.3% to 35.3%.Source: §3.5 · pp. 7–8, Table 5 · p. 8

3.6 Benchmark-level trends

  • DPO’s largest 4B pass^4 gains include 85.2 points on ProofWriter and 59.0 points on RuleTaker; gains are largest on tasks with executable symbolic or relational structure.At 4B and 9B, DPO improves avg@N and pass^4 in every category; 27B DPO has the sweep’s highest aggregate scores and SMT-quality profile.Source: §3.6 · pp. 8–9, Table 7 · p. 9

4 Related Works

The related work situates Sequent-Prover between formal theorem-proving systems and symbolic solver methods, shifting the generation target to SMT-LIB artifacts. It also connects the approach to execution-feedback repair and verifiable-output optimization.

Verifier-Integrated Formal Reasoning

  • Formal theorem-proving systems use machine-checkable artifacts and iterative refinement; this work shifts the target from Lean to SMT-LIB for compact models across multiple SMT logics [Lin et al., 2025b; Ren et al., 2025; Wang et al., 2025].The cited systems include Goedel Prover, DeepSeek-Prover, and Kimina-Prover.Source: §4 · p. 9

Solver-Based Symbolic Reasoning and Synthesis

  • Unlike classical symbolic systems with hand-written encodings or formal-object search, Sequent-Prover trains a language model to emit executable artifacts validated by a symbolic backend.SymPy serves as a controllable symbolic front-end for scaling supervision across logic fragments.Source: §4 · p. 9

Self-Repair and Tool Feedback

Reinforcement Learning for Verifiable Outputs

5 Conclusion

Sequent-Prover turns solver use into a learned formal-reasoning policy, with post-training associated with more grounded, stable, and refutational solver behavior.

5 Conclusion

  • Solver use can be learned as a formal-reasoning policy that formulates proof obligations, encodes SMT-LIB, interprets Z3 responses, repairs artifacts, and commits with evidence.The method filters trajectories using executable SMT feedback and contrasts successful traces with failed ones.Source: §5 · p. 9
  • Post-training produces more grounded and non-vacuous SMT programs and shifts correct traces toward refutational UNSAT evidence.The conclusion describes sample-dependent solver successes becoming stable behavior.Source: §5 · p. 9
  • Training helps most when a base model has latent solver-use competence but lacks consistency.Source: §5 · p. 9

6 Limitations

The paper identifies intended abstraction as a limit of formal verification, then describes Z3's proof modes, the agent loop, and the breadth of evaluation datasets.

6 Limitations

  • A solver checks a formal artifact but cannot determine whether its abstraction captures the intended task; learning the right abstraction remains open.Most tasks lack a reference formalization, and the paper uses grounding, non-triviality, and structural-uncertainty measures as proxies for meaning preservation.Source: §6 · pp. 9–10

A Background: Agent, Solver & Training

  • Z3 returns SAT, UNSAT, UNKNOWN, or an error for formulas over combinations of background theories.The described theories include integer or real arithmetic, bit-vectors, uninterpreted functions, strings, arrays, and datatypes.Source: §A.1 · p. 13

A.1 The Z3 SMT Solver and the Two Proof Modes

  • For entailment, asserting premises with the negated conclusion makes UNSAT evidence establish entailment, whereas SAT for premises plus conclusion only shows consistency.The paper distinguishes this refutational use from SAT-based model-finding and describes vcr and vcrUNSAT as quantifying the distinction.Source: §A.1 · p. 13

A.2 The Tool-Calling Agent Loop

  • Across turns, the agent receives prior conversation and tool outputs, calls Z3 with SMT code or replies with a final answer, and is subject to execution and iteration limits.The harness applies a 30-second and 256-MB cap to solver calls, with Tmax = 10; answers are checked using dataset-specific extractors.Source: §A.2 · pp. 13–14

A.3 Datasets.

  • Training uses AR-LSAT, FOLIO, and ZebraLogic for distinct symbolic reasoning forms, with other datasets added for diversity.Evaluation separates held-out examples from those core dataset families from other benchmark sources, testing transfer across dataset families.Source: §A.3 · pp. 14–15
  • The evaluation suite spans logical, arithmetic, spatial, commonsense, science, broad-coverage multiple-choice, and multi-hop question-answering tasks.Source: §A.3 · p. 14

A.4 Reproducibility.

The appendix documents released artifacts, trajectory curation and training, scope decisions, and the evaluation metrics used to characterize correctness, reliability, and SMT-program quality.

A.4 Reproducibility.

  • The authors release the SMT harness and post-trained 4B, 9B, and 27B models, and plan to release 14,307 curated trajectories and prompts.The full sweep used approximately 1,000 GPU-hours on A100-80GB/H200 hardware.Source: §A.4 · pp. 15–16
  • Teacher rollouts are accepted as Gold only when answers are correct, traces finish, SMT is grounded and non-trivial, and Z3 returns a real verdict.The dataset contains 10,785 gold, 2,995 reject, 464 silver, and 63 discarded infrastructure-error trajectories.Source: §A.4 · p. 15
  • SFT trains on rendered traces that preserve interleaved reasoning, tool calls, and solver outputs; DPO then contrasts chosen and rejected trajectories.The SFT and DPO recipes use different sequence cutoffs and training settings.Source: §A.4 · p. 15
  • The authors report scope choices including limited component ablations, aggregate reporting over 7,254 problems per family, and no comparison with methods requiring hundreds of test-time samples.They state that a fair comparison with those methods would require a similar test-time budget.Source: §A.4 · p. 16

B Evaluation Metrics

  • Evaluation metrics cover sample-based correctness, agent reliability, and SMT-program quality, with K = 4 samples unless otherwise stated.The groups respectively assess correctness indicators, commitment relative to correctness, and properties of emitted SMT-LIB code.Source: B Evaluation Metrics · p. 16

B.1 Sample-Based Correctness

The appendix defines complementary measures for sample-based answer correctness, agent reliability, and SMT-program quality. These measures distinguish answer success from consistency, solver use, and the quality of the formal artifacts in an agent’s trace.

B.1 Sample-Based Correctness

  • avg@N estimates single-attempt correctness, while pass@4 measures four-sample coverage and pass^4 measures the probability that all four attempts are correct.maj@4 measures majority-vote correctness; the gap between it and avg@N reflects the benefit of self-consistency aggregation, which assumes wrong answers are more diverse than right ones.Source: §B.1 · p. 17

B.2 Agent-Reliability Measures

  • Agent-reliability measures assess commitment quality, recovery after an initial solver failure, tool and turn efficiency, and variation in generated SMT skeletons.Soundness is correctness among attempts that finish; completeness is voluntary termination among correct attempts, and recovery measures correctness after a first-call failure.Source: §B.2 · p. 18

B.3 SMT-Program Quality

  • SMT-program quality measures evaluate how an answer was obtained, using per-attempt disjunctions so one strong call can count despite weaker exploratory calls.The metrics include grounding, triviality, first-pass Z3 validity, and verified-correct rates.Source: §B.3 · p. 19, §B.3.1 · p. 19, §B.3.2 · p. 20

B.3.1 Grounding

  • Grounding measures the fraction of extracted problem entities appearing in the SMT body, but permissive substring matching makes it a liberal measure of semantic transfer.The λgnd = 0.25 threshold was empirically set to separate inspection-verified decorative programs from content-loaded ones on a held-out development sample.Source: §B.3.1 · p. 19

B.3.2 Triviality

  • Triviality rules flag empty, structurally empty, tautological, or stub-like SMT calls; a nonzero trivial-SMT rate diagnoses performative solver use.The rate is the fraction of attempts whose entire SMT-call sequence is trivial.Source: §B.3.2 · p. 20

B.3.3 First-Pass Z3 Validity

  • First-pass Z3 validity tests whether the first SMT-LIB emission parses and type-checks; changes measure surface syntax, not reasoning depth.Source: §B.3.3 · p. 20

B.3.4 Verified-Correct Rate and its Unsat Restriction

  • Verified-correct rates exclude correct answers lacking real, grounded, non-trivial solver evidence; the UNSAT-restricted rate additionally requires refutational evidence.The pair distinguishes performative correctness, correctness supported by a SAT witness, and correctness supported by UNSAT.Source: §B.3.4 · p. 20

B.3.5 Z3 Outcome Distribution

  • The Z3 outcome distribution tracks the fraction of solver calls returning each status and distinguishes NO VERDICT from ERROR.NO VERDICT means no sat-result token appeared in stdout despite a successful call; ERROR denotes an exception or non-zero exit.Source: §B.3.5 · pp. 20–21

C Comparison to Open-Weight Baselines

The section compares DPO-tuned Sequent-Prover checkpoints with open-weight baselines under the same SMT-scratchpad evaluation. DPO models are stronger on several correctness and verifier-use measures, while the comparison with GPT-OSS-120B is closer.

C Comparison to Open-Weight Baselines

  • Table 10 reports macro-averaged deltas over shared canonical datasets: versus Gemma-4B, Qwen-4B-DPO improves avg@N by +0.647, pass@4 by +0.524, and pass^4 by +0.640.Source: C Comparison to Open-Weight Baselines · p. 21
  • +0.027 avg@N, +0.021 pass@4, and +0.036 pass^4 for Qwen-27B-DPO versus GPT-OSS-120B; the 27B checkpoint remains positive on all reported correctness aggregates.Source: C Comparison to Open-Weight Baselines · p. 21
  • +0.341 verified-correct rate and +0.274 grounding for Qwen-27B-DPO versus GPT-OSS-120B; trivial-SMT rate decreases in all five reported comparisons.The reported verifier-use gains also include higher verified-correct rates for Qwen-4B-DPO versus Gemma-4B and Qwen-27B-DPO and Qwen-9B-DPO versus GPT-OSS-20B.Source: C Comparison to Open-Weight Baselines · p. 21
  • Qwen-DPO models outperform Gemma-4B and GPT-OSS-20B across categories, while Qwen-27B-DPO is strongest against GPT-OSS-120B on AGIEval, NLI/MCQ, and hard reasoning.Against GPT-OSS-120B, the 9B comparison is near parity on AGIEval, arithmetic, hard reasoning, and NLI/MCQ, with larger gaps on spatial and free-form QA.Source: C Comparison to Open-Weight Baselines · p. 21

D Additional Analyses

  • Additional analyses cover pool composition, per-category results, test-time sampling, grounding without comments, structural uncertainty, teacher support, and soundness.Source: D Additional Analyses · p. 21

D.1 Pool Composition and Per-Category Results

The per-category analysis reports results for a benchmark pool of 7,254 problems per model family. Hard reasoning shows the largest within-category gain at 4B, while most 27B categories are near ceiling.

D.1 Pool Composition and Per-Category Results

  • The pool contains 7,254 problems per model family: 200 per benchmark except ProofWriter, which contributes 54 because of a data-loader bug.Source: §D.1 · p. 21
  • Category results are micro-averages over category problems and use the same four trajectories per problem as the main results.Source: §D.1 · pp. 21–22
  • At 4B, hard reasoning has the largest within-category gain, +0.493 pass^4; at 27B, remaining gains are concentrated in hard and spatial reasoning.Most 27B categories are near ceiling, with small changes on saturated categories.Source: §D.1 · p. 22

D.2 Post-Training versus Test-Time Sampling

Across sampling comparisons and qualitative analyses, post-training improves reliability and SMT-program behavior, with gains in grounding, structural consistency, and solver-guided reasoning. The examples show how agents repair formalizations and choose queries that better preserve the problem’s meaning.

D.2 Post-Training versus Test-Time Sampling

  • At matched K = 4, post-trained accuracy improves by 21.2 points and majority-vote accuracy by 9.9 points over base self-consistency; at K = 16, majority-vote accuracy is statistically similar while the base uses 6.6× more tokens.The comparison uses 180 held-out problems across six benchmark families, with 16 trajectories for base and post-trained models and four for prompting baselines.Source: §D.2 · p. 22

D.3 Grounding without Comments

  • Post-trained models retain higher grounding than base models after comments are stripped, despite grounding not being part of the training reward.The comment-stripping analysis recomputes grounding on about 50k trajectories.Source: §D.3 · p. 22, Table 17 · p. 25

D.4 Structural Uncertainty of SMT Programs

  • Structural variation falls after post-training: peer divergence drops most at 4B and 9B, while both within-trajectory drift measures fall in all six comparisons.The structural measure is based on SMT-LIB grammar-production distributions and does not establish identical syntax trees or semantics.Source: §D.4 · p. 23, Table 18 · p. 25

D.5 Teacher Support and Student Capability

  • SFT students are bounded by the teacher’s support over successful strategies, and the benchmarks do not test fragments such as fixed-size bit-vector arithmetic.The passage notes that stronger teacher performance on such fragments could extend the recipe.Source: §D.5 · p. 23, Table 15 · p. 24

D.6 Soundness after SFT

  • After DPO, soundness improves alongside fewer malformed SMT calls and more refutational solver use; the authors report no broad reliability drop after SFT.Soundness is accuracy on attempts where the agent chooses to finish.Source: §D.6 · p. 24

E.1 Capability 1: SMT-LIB language fluency

  • Manual inspection links metric gains to formalizations that follow problem statements more closely; in the language-fluency example, Sequent-Prover-4B recovers in one turn while the base model rarely does.The base model’s example emits malformed SMT-LIB and exhausts its 10-turn budget without finishing.Source: E Qualitative Improvements · p. 24, §E.1 · p. 24

E.2 Capability 2: First-order over propositional encoding

  • On FOLIO-1361, the base model’s propositional encoding injects unsupported disjointness axioms and returns a false answer, while first-order encoding expresses the quantified conditions directly.The premises constrain Rockie to be a rabbit or squirrel but do not state that those categories are disjoint from turtles.Source: §E.2 · pp. 25–26

E.3 Capability 3: Bidirectional satisfiability for ternary verdicts

  • For ternary verdicts, Sequent-Prover-4B tests both the conclusion and its negation; on FOLIO-476, the sat/unsat signature supports the correct False answer.The base model asks only one query and concludes Uncertain.Source: §E.3 · p. 26

E.4 Capability 4: Declarative encoding via datatypes

The examples show Sequent-Prover-4B using declarative finite-domain encodings, independent push/pop tests for answer choices, and solver outcomes to diagnose inconsistent premises. These strategies contrast with base-model errors that prevent reaching the relevant tests or lead to unsupported conclusions.

E.4 Capability 4: Declarative encoding via datatypes

  • For finite-enumeration problems, Sequent-Prover uses datatypes and an assignment function; after a Z3 arity error, it replaces the invalid expression with xor.The example is an AR-LSAT problem about assigning seven sales representatives to three zones.Source: §E.4 · p. 26

E.5 Capability 5: Push/pop for multi-option queries

  • For a “must be true” question, Sequent-Prover tests each choice’s negation in independent push/pop blocks; the unique unsat result identifies the answer.It finishes in three iterations with one comprehensive query rather than five separate queries.Source: §E.5 · p. 27

E.6 Capability 6: Diagnosing inconsistent premise sets

  • Both directions returning unsat prompts Sequent-Prover to test the premises alone, diagnose inconsistency, remove unsupported disjointness axioms, and finish with Uncertain.On the revisited FOLIO-1361 example, the added disjointness axioms make both directions unsat; removing them restores sat results in both directions.Source: §E.6 · pp. 27–28

E.7 Capability 7: Error text as actionable feedback

Sequent-Prover’s error recovery is characterized by using solver feedback to locate and patch a specific faulty expression, while the base model tends to retry the full program or make unhelpful broad changes.

E.7 Capability 7: Error text as actionable feedback

  • Sequent-Prover patches the named SMT-LIB error locally—moving a declaration, replacing Boolean with Bool, or rewriting an invalid not subtree as xor—while the base retries whole programs.The observed recovery pattern is to read the Z3 error, locate the named node, and patch it without disturbing the rest of the program.Source: §E.7 · p. 28

Related papers

Loading 2610.15258v1…