Error Localization and Steering of Language Model Quantitative Reasoning

A single reasoning error in a large language model (LLM) can propagate through subsequent steps and lead to consequential failures in quantitative tasks. Existing correction methods rely largely on textual feedback, while formal verification can provide precise diagnostics without directly translating them into effective model interventions. We introduce our approach, a neuro-symbolic framework that turns formal diagnosis into targeted inference-time correction. A typed factor-graph intermediate representation grounds variables, relations, and dependencies in the source text, enabling a Satisfiability Modulo Theories (SMT) solver to localize the first conflicting reasoning step and identify the constraints responsible for the error. Our approach then converts this diagnosis into steering signals applied through the model's Key-Value (KV) cache, preserving the valid reasoning prefix while regenerating only the erroneous step with the same frozen model. Across four LLM backbones and four quantitative reasoning datasets, our approach improves both first-error localization and correction accuracy over three state-of-the-art baselines. Crucially, it provides effective guidance even for smaller models that struggle to act on textual critiques, showing that verifier-grounded steering can enhance corrections where language-only feedback falls short.