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 explici...
Debargha Ganguly, Wei-Cong Chen, Mohsen Hariri et al.
· 3 citations