Steering Tree-of-Thought Reasoning via Deductive Verification

Large language models (LLMs) have demonstrated great potential in code reasoning tasks, but their reasoning processes lack reliable verification mechanisms, making it difficult to ensure logical correctness. The Tree of Thoughts (ToT) framework improves reasoning by exploring multiple paths and employing backtracking, yet its path selection relies entirely on LLM-based self-evaluation—a heuristic and error-prone mechanism—leading to frequent erroneous pruning and unproductive exploration. We identify a key insight: LLMs’ encoding capability is stronger than their reasoning capability—translating code semantics into formal constraints is a pattern-matching task that LLMs can perform reliably, while verification should be delegated to SMT(Satisfiability Modulo Theories) solvers. Based on this insight, we propose Deductive Steering, a mechanism that integrates SMT solver verification into Tree of Thoughts exploration. It consists of four core components: (1) Candidate Generator produces candidate reasoning steps, each comprising a natural language thought t and its SMT constraint encoding ϕ; (2) Deductive Evaluator verifies whether a candidate constraint ϕ is a logical consequence of the accumulated constraint Φ by checking the unsatisfiability of Φ ∧ ¬ ϕ; (3) Counterexample Refinement uses counterexample to guide the LLM in correcting its reasoning when verification fails; (4) Exploration and Backtracking Strategy manages path exploration and backtracks to alternative candidates when verification fails. Experiments on five benchmarks covering fault localization, program synthesis, and loop invariant generation show that, compared with ToT, Deductive Steering improves task-level effectiveness by 9.2–32.6 percentage points while reducing token consumption by 35.7–52.4%. The method generalizes across different LLMs and extends to mathematical reasoning, demonstrating broad applicability to domains where reasoning can be encoded as formal constraints.