interwhen: A Generalizable Framework for Steering Reasoning Models with Test-time Verification

Reasoning models produce long traces of intermediate decisions and tool calls, making test-time verification increasingly important for ensuring correctness. Existing approaches either verify only the final answer, which misses early errors, or rely on branch-and-verify strategies that explore multiple trajectories at substantially higher compute cost. We introduce interwhen, a single-trajectory verification framework that steers model behavior by providing feedback on intermediate reasoning traces. It addresses two key challenges. First, given a set of verifiers, obtaining verifiable states from the reasoning trace typically requires prompt engineering or external task decomposition into fixed steps, which can constrain the model's reasoning strategy. Instead, we propose a monitoring system that periodically polls the reasoning trace and forks inference of the reasoning model to recover intermediate states. Verifiers are run asynchronously alongside generation, adding negligible overhead on correct executions and intervening only when violations occur. Second, beyond math and code, a central challenge for process verification is the scarcity of verifiers. interwhen addresses this through automatic verifier synthesis from natural-language policy documents. Given a policy, it can generate code-based verifiers, including provably correct verifiers in Lean and Z3. Together, these contributions yield a plug-and-play system for policy-grounded, formally verified process supervision of any reasoning agent. On reasoning benchmarks where policies encode mathematical or logical constraints, interwhen-based steering achieves near-perfect accuracy for reasoning models using a fraction of the token compute of test-time verification baselines. On agentic benchmarks with policy-based verifier generation, it enables significant improvements in task quality for SLMs without any finetuning; e.g., the task completion rate of Qwen3-30B jumps from 32% to 87% on the telecom domain in tau^2-bench.