Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning
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 semanti...
| Authors | Debargha Ganguly, Weicong Chen, Mohsen Hariri et al. |
|---|---|
| Primary category | cs.CL |
| Published | 11 October 2026 |
| Last updated at source | 11 October 2026 |
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 14 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.