The authors propose a post-training framework for language models that use SMT solvers (Z3) as a reasoning tool.
Training with solver feedback boosts reliability of language model reasoning
Sequent-Prover agents, post-trained using verifier-conditioned trajectory distillation, achieve 97% accuracy on SMT-based reasoning benchmarks.
Big Tech
Debargha Ganguly · Weicong Chen · Mohsen Hariri · Vikash Singh · Sreehari Sankar · Shouren Wang · +10 more
Case Western Reserve University · UT Austin · Microsoft Research
Research Digest··2 min read
The authors introduce Sequent-Prover, a family of language model agents that reason by writing and executing SMT-LIB programs with the Z3 solver.
Why this paper
From Microsoft Research and 2 others
In one line
Post-training language model agents with solver feedback improves SMT reasoning accuracy and reliability.
What we could check
- ·No code link found
- ·No weights link found
- ·No dataset link found
- ·No compute details found
- ·No stated limitations found
- ✓Reports numbers on named benchmarks
Observed from the paper text and links we have. Absence here means we did not find it, not that it does not exist.
§