Learning Formal-Informal routing for stepwise COT verification

Large language models (LLMs) often solve complex reasoning tasks by generating chain of thought (CoT), making step-level verification critical. Existing approaches rely on either _formal verification_, whose effectiveness depends on whether a CoT can be faithfully formalized and whether the resulting formal representation preserves its meaning, or _informal LLM-based verification_, which is prone to inconsistent judgements. We propose an adaptive routing policy framework that learns to select the appropriate verification tool (_formal_ or _informal_) for each CoT verification instance. The policy is initialized through supervised finetuning (SFT) and subsequently optimized with reinforcement learning (RL) using two latent faithfulness scores, which encourage it to choose formal verifier only when symbolic formal translation is sufficiently faithful and semantically consistent. We evaluate the framework on six reasoning benchmarks, including _Sieve_, a new step-level verification dataset introduced in this work to assess generalization. Across all benchmarks, our RL routing policy outperforms 1) neuro-symbolic pipelines (_Vanessa_, _Parc-Graph_) and the formal-only verifier, is competitive with the 2) informal-only verifier, and rivals or exceeds substantially larger 3) proprietary verifiers such as GPT-4.1 and GPT-5.4. The improvement reaches ∼36 Macro-F1 points over the formal-only verifier and up to ∼11 points over the informal-only verifier. Its edge over the larger proprietary verifiers is clearest on the challenging _Sieve_ and _PRM_ benchmarks, where the RL routing policy attains the best results among comparable systems and surpasses even GPT-4.1 and GPT-5.4 on _Sieve_ (e.g., $59.51$ vs. $53.12$/$34.18$ Macro-F1 on _Sieve-MCQ_) and exceeds GPT-4.1 on _PRM_ ($58.00$ vs. $55.73$). These results demonstrate that adaptive verification tool selection is an effective strategy for improving step-level reasoning verification.