Sequent-Prover improves accuracy and efficiency in formal reasoning agents
Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning
Computation and LanguageArtificial IntelligenceMachine LearningLogic in Computer Science
Summary
Formal reasoning with computers means writing very precise logical statements that a solver like Z3 can check. The paper presents Sequent-Prover, a system that trains language models to write these precise statements step-by-step and correct them by consulting the solver repeatedly. This training method greatly improves the model’s accuracy and reliability in producing correct formal proofs. As a result, Sequent-Prover agents provide answers backed by formal, executable code, making their reasoning more trustworthy.
What this means in practice
- •For software verification teams: Automatically generate and refine formal proofs for software correctness using a trained language model that interacts with an SMT solver.
- •For automated reasoning tool developers: Enhance reasoning agents with improved training techniques to reduce solver calls and token usage while increasing confidence in generated proofs.
Authors
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
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.