Stepwise Reasoning Verification: Don't Generate, Classify!

Introduction

LLMs are increasingly used for complex mathematical and scientific problem solving, making reliable verification of their reasoning essential: seemingly coherent solutions can contain invalid intermediate steps, and a correct final answer does not guarantee sound reasoning [5, 26] (Zheng et al. 2025a). This need also extends to core educational applications of LLMs, such as tutoring and automated feedback, where corrective guidance requires locating errors in a student’s reasoning rather than simply judging the solution incorrect [5] (Srivatsa et al. 2025). Stepwise verification addresses these challenges by assessing individual reasoning steps in context to detect and localise errors (Zheng et al., 2025a).

Existing stepwise verifiers rely on large decoder models: discriminative approaches assign step-level scores or labels [28] (Wang et al. 2024b), while generative approaches produce verdicts [21] (Zhang et al. 2025a; Zhao et al. 2026). However, recent work finds no consistent performance advantage for either paradigm [24], leaving open which approach is preferable and whether large decoder models are necessary for strong verification. Resolving these questions is especially important for real-world deployment, where running a large verifier at every reasoning step can impose substantial latency and computational costs.

To address these questions, we formulate stepwise verification as natural language inference (NLI) [4, 2]. We treat the problem statement and solution prefix as the premise and the next reasoning step as the hypothesis, classified as entailed or non-entailed. This formulation extends encoder-based NLI classification, where encoders remain competitive with far larger LLMs on discriminative tasks [9], to stepwise verification and provides a common task definition for comparing encoder classifiers, decoder classifiers, and generative verifiers.

We evaluate our NLI formulation on five datasets covering mathematical, formal, and multi-domain reasoning. To the best of our knowledge, we are the first to demonstrate that encoder classifiers with only hundreds of millions of parameters can outperform generative verifiers with several billion parameters at detecting invalid reasoning steps (Figure 1). On identical decoder backbones, classification outperforms generative verification from 0.5B to 4B and matches it on the strongest 7B backbone. In data-scaling experiments, classification often achieves comparable performance with roughly one tenth as many annotated problems as generative verification. Collectively, our findings suggest that how a model is trained to verify stepwise reasoning matters more than its size, supporting the use of small classifiers in applications where repeated step-level verification must fit within limited time and compute budgets.

Related Work

Verification objectives. Verification requires accurate error detection at a computational cost that permits repeated checks throughout a solution, making small, effective verifiers a practical priority. However, existing approaches typically rely on large decoder backbones, using dedicated scoring heads [28] (Wang et al. 2024b; Zhang et al. 2025b), generating verdicts through next-token prediction (Zhang et al., 2025a), or generating verification rationales before predicting a verdict [21] (Zhao et al. 2026). Whether this scale is necessary depends in part on how the model is trained to verify. Lee et al. [24] find that the performance of classification and generation varies across verification settings, while differences in model size, supervision, and inference computation further complicate comparisons. We therefore compare classification and direct-verdict generation on identical decoder backbones and training instances across model sizes and annotation budgets, testing whether classification can reduce the model size and supervision needed for accurate verification. Appendix § 9 compares these studies by the factors each holds fixed.

Verification as inference. Assessing a reasoning step requires relating it to the problem and preceding steps. NLI provides a formulation of this task by assessing whether a hypothesis follows from a premise [4]: the problem and preceding reasoning form the premise, and the current step is the hypothesis. Prior work uses entailment and deductive judgements to evaluate intermediate reasoning [29, 39] (Zhu et al. 2024; Zhou et al. 2024), including existing NLI models that detect unsupported or contradictory claims within reasoning chains [13, 34]. Related approaches examine mathematical premise selection [10], verify steps through autoformalisation and theorem proving [19, 39], or extract validity signals from attention structure [32]. We build on inference-based evaluation by training classifiers directly on step-level error labels. The premise–hypothesis formulation provides a common input for encoder and decoder verifiers, allowing us to compare architectures and training objectives on identical labelled instances.

Small encoder verifiers. Encoders are a well-motivated alternative to large decoder verifiers given their established use in NLI and their effectiveness and parameter efficiency on discriminative language-understanding and reasoning tasks [36, 38, 33, 9] (Weller et al. 2026). Their potential is also supported by Gu et al. (2023), who show that scoring candidate plans with BERT-base can outperform generative approaches while requiring less supervision. In reasoning verification, DIVERSE [27] fine-tunes a DeBERTa encoder with solution-level supervision and auxiliary step labels, demonstrating that encoders can learn step-level predictions. Its evaluation, however, focuses on improving final-answer selection. Conversely, we examine the effectiveness of encoders as standalone step-level verifiers, comparing them with decoder classifiers and generative verifiers across datasets, model sizes, and annotation budgets. This directly tests whether small classifiers can match larger generative models at detecting reasoning errors, and how much supervision they require.

Methodology

Stepwise Verification as Natural Language Inference

Let a reasoning trajectory consist of a problem statement $Q$ and an ordered sequence of steps $s_1,\ldots,s_n$. To verify each step $s_i$, we construct a premise containing the problem and all preceding steps, with the current step as the hypothesis:

where $\oplus$ denotes concatenation. Each verification instance is $(x_i,y_i)$, with

These labels represent step validity in context: $H_i$ is labelled entailment if it is supported by $P_i$, and non-entailment otherwise. For example, given the problem “Solve $2x+3=7$” and the prefix “$2x=4$,” the next step “$x=2$” is entailed, whereas “$x=4$” is non-entailed. This formulation enables precise localisation of intermediate reasoning errors and provides a common task definition for encoder classification, decoder classification, and generative verification.

Concretely, we use the predicted probability of non-entailment as the step-level error score:

For a trajectory whose first annotated error occurs at step $k$, we retain the $k$ instances $\{(x_i,y_i)\}_{i=1}^{k}$ and assign

We discard subsequent steps because their premises already contain an annotated error. For fully correct trajectories, we retain all $n$ steps and label each as entailment. Each retained instance is scored separately using its full premise $P_i$.

Classification and Generative Verification

To test whether strong verification requires large decoder models, we compare encoder classification, decoder classification, and decoder verdict generation across model scales, using identical premise–hypothesis instances (Figure 2).

1. Encoder classification. An encoder maps the premise–hypothesis pair $x_i$ to a representation $h_i^{\mathrm{enc}}$. A binary classification head then produces the non-entailment score $p_i$.

2. Decoder verdict generation. We fine-tune the decoder to generate a single verdict token: Yes for entailment or No for non-entailment. At inference, we compute the non-entailment score by normalising over the two verdict tokens:

where $z_i^{\mathrm{Yes}}$ and $z_i^{\mathrm{No}}$ are their logits at the last prompt position.

3. Decoder classification. The same decoder processes $x_i$ causally. We take its hidden state $h_i^{\mathrm{dec}}$ at the final non-padding input token and apply a linear head with two outputs:

The non-entailment score uses the same normalisation as Equation (3). We initialise $w_{\mathrm{Yes}} and $w_{\mathrm{N0}}$ from the language-model output embeddings of the two verdict tokens and set both biases to zero.

Both decoder variants use supervised fine-tuning (SFT); we refer to them as decoder generation SFT and decoder classification SFT. They share the pretrained backbone, input prompt, and training instances, but differ in their output heads and training objectives. Although both make the same binary verification decision, generation minimises next-token cross-entropy over the full vocabulary, whereas classification minimises cross-entropy over the two verification labels. Comparisons between encoders and decoders additionally reflect differences in architecture, pretraining, and context capacity.

Experiment Setup

Models and Datasets

Our NLI formulation motivates evaluating encoder models widely used for this task: BERT Devlin et al. [8], RoBERTa Liu et al. [30], DeBERTa He et al. [17], and ModernBERT Warner et al. (2025), each at base and large scales. For decoders, we use pretrained checkpoints from Qwen2.5 Yang et al. (2024a) at 0.5B, 1.5B, 3B, and 7B; Qwen2.5-Math Yang et al. (2024b) at 1.5B and 7B; Llama-3.2-3B Llama Team [31]; and Gemma-3-4B Gemma Team [12]. Each decoder is fine-tuned separately for verdict generation and classification, allowing us to compare the two objectives on the same pretrained backbone.

We use five English datasets common in stepwise verification [21, 24] (Zhang et al. 2025b), spanning mathematical, formal, and multi-domain reasoning: PRM800K Lightman et al. [28], MathShepherd Wang et al. (2024b) (MS), Epic50K Sun et al. (2025), FoVer Kamoi et al. [20], and MMLU-Pro-CoT Zeng et al. (2025) (MMLU). Their step labels come from different sources (Table 1) and measure different things: human judgements (PRM800K) and formal verifiers (FoVer) assess whether a step is valid, whereas rollout labels (MathShepherd) assess whether the prefix can still reach the correct answer, which is closer to the step’s utility than to its validity Lee and Hockenmaier [25].

Dataset	Domain	Labels	Train	Test	Err.
PRM800K	Math	Human	46.0k	70.5k	8.3
MS	Math	Rollout	37.0k	80.9k	17.5
Epic50K	Math	Contrib.	42.7k	37.8k	6.0
FoVer	Formal	Verifier	34.3k	10.8k	24.0
MMLU	Multi	Synthetic	38.0k	49.5k	9.6

We construct all splits at the question level, keeping solutions to the same question together to prevent overlap between training and evaluation. For PRM800K and MathShepherd, we retain the released test partitions and exclude their questions from training. For the remaining datasets, we hold out 10% of questions for testing. After converting solutions into premise–hypothesis instances (§ 3.1), we retain one copy of each duplicate pair with matching labels and discard pairs assigned conflicting labels.

To keep the numbers of training problems comparable across datasets, we cap PRM800K, MathShepherd, and MMLU-Pro-CoT at between 37k and 46k problems per dataset and retain all available training problems from Epic50K and FoVer. These sets define our Full training condition.

Training splits are balanced by undersampling within each step position, so that position does not predict the label; validation and test splits keep their natural label distribution. Inputs beyond a model’s context limit are truncated from the left, keeping the step and its nearest context; this mainly affects Epic50K, where a third of test instances exceed 512 tokens (Appendix § 10).

Training Setup

All models are trained with full-parameter fine-tuning using the 8-bit AdamW optimiser Dettmers et al. [7]. We repeat each SFT experiment with three random seeds and report results aggregated across the three runs. Full implementation details are provided in Appendix § 11.

Metrics

Following prior work [20] (Xia et al. 2025), we report step-level area under the receiver operating characteristic curve (AUC), computed over separately scored premise–hypothesis instances. AUC measures discrimination between the two labels without requiring a decision threshold and does not directly depend on the class proportions of the test splits, which retain their natural label distributions.

Results & Analysis

Main Results

Table 2 shows that the training objective matters more than model size. On identical decoder backbones up to 4B, classification achieves an average AUC of 0.870, compared with 0.803 for generation—a gain of 0.067 without increasing backbone size. Encoder classifiers with 0.11B–0.44B parameters average 0.806 AUC, comparable to these generative decoders despite having roughly one ninth as many parameters on average. Qwen2.5-0.5B trained for classification (0.844 AUC) also outperforms every generative decoder up to 4B except Qwen2.5-3B. At 7B, classification matches generation on Qwen2.5-Math, demonstrating that it remains competitive on larger backbones. We next examine these results in more detail, focusing first on the training objective and then on model scale.

Model	Paradigm	PRM	MS	Epic	FoVer	MMLU	Avg.	$\Delta$
Decoders
Qwen2.5-0.5B	Gen.	.680$\pm$.011	.665$\pm$.010	.968$\pm$.001	.764$\pm$.016	.826$\pm$.004	.780$\pm$.008	+.064
	Cls.	.745$\pm$.097	.769$\pm$.010	.974$\pm$.002	.894$\pm$.046	.838$\pm$.004	.844$\pm$.032
Qwen2.5-1.5B	Gen.	.707$\pm$.040	.589$\pm$.012	.969$\pm$.001	.701$\pm$.026	.858$\pm$.008	.765$\pm$.017	+.097
	Cls.	.780$\pm$.070	.824$\pm$.003	.978$\pm$.002	.860$\pm$.158	.867$\pm$.004	.862$\pm$.047
Qwen2.5-Math-1.5B	Gen.	.767$\pm$.013	.617$\pm$.012	.973$\pm$.001	.792$\pm$.001	.864$\pm$.005	.803$\pm$.007	+.113
	Cls.	.838$\pm$.068	.890$\pm$.002	.985$\pm$.000	.974$\pm$.001	.891$\pm$.001	.916$\pm$.014
Qwen2.5-3B	Gen.	.843$\pm$.004	.790$\pm$.010	.976$\pm$.000	.868$\pm$.071	.886$\pm$.003	.873$\pm$.018	+.021
	Cls.	.858$\pm$.004	.808$\pm$.097	.977$\pm$.008	.977$\pm$.001	.849$\pm$.085	.894$\pm$.039
Llama-3.2-3B	Gen.	.782$\pm$.010	.613$\pm$.009	.970$\pm$.001	.894$\pm$.011	.855$\pm$.004	.823$\pm$.007	+.062
	Cls.	.811$\pm$.001	.795$\pm$.003	.977$\pm$.000	.965$\pm$.004	.875$\pm$.002	.885$\pm$.002
Gemma-3-4B	Gen.	.689$\pm$.093	.598$\pm$.014	.967$\pm$.003	.771$\pm$.036	.850$\pm$.002	.775$\pm$.030	+.046
	Cls.	.761$\pm$.041	.763$\pm$.056	.972$\pm$.004	.766$\pm$.097	.843$\pm$.008	.821$\pm$.041
Qwen2.5-7B	Gen.	.876$\pm$.006	.887$\pm$.002	.986$\pm$.001	.985$\pm$.001	.914$\pm$.001	.929$\pm$.002	-.073
	Cls.	.856$\pm$.003	.882$\pm$.002	.922$\pm$.095	.811$\pm$.150	.811$\pm$.089	.856$\pm$.068
Qwen2.5-Math-7B	Gen.	.907$\pm$.001	.905$\pm$.002	.989$\pm$.001	.990$\pm$.001	.917$\pm$.002	.941$\pm$.001	.000
	Cls.	.899$\pm$.001	.910$\pm$.001	.988$\pm$.000	.989$\pm$.001	.917$\pm$.001	.941$\pm$.001
Encoders
BERT-B (0.11B)	Cls.	.743$\pm$.004	.731$\pm$.003	.765$\pm$.001	.800$\pm$.004	.770$\pm$.005	.762$\pm$.003
BERT-L (0.34B)	Cls.	.698$\pm$.060	.705$\pm$.015	.683$\pm$.130	.720$\pm$.088	.774$\pm$.008	.716$\pm$.060
RoBERTa-B (0.13B)	Cls.	.777$\pm$.007	.720$\pm$.008	.972$\pm$.001	.916$\pm$.001	.812$\pm$.002	.839$\pm$.004
RoBERTa-L (0.36B)	Cls.	.755$\pm$.042	.639$\pm$.121	.972$\pm$.001	.939$\pm$.003	.822$\pm$.010	.825$\pm$.035
DeBERTa-B (0.18B)	Cls.	.778$\pm$.004	.617$\pm$.073	.809$\pm$.007	.907$\pm$.005	.806$\pm$.018	.784$\pm$.021
DeBERTa-L (0.44B)	Cls.	.793$\pm$.004	.700$\pm$.004	.813$\pm$.012	.941$\pm$.008	.850$\pm$.004	.820$\pm$.007
ModernBERT-B (0.15B)	Cls.	.780$\pm$.011	.730$\pm$.003	.973$\pm$.001	.946$\pm$.007	.804$\pm$.005	.847$\pm$.005
ModernBERT-L (0.4B)	Cls.	.783$\pm$.011	.697$\pm$.024	.976$\pm$.001	.960$\pm$.003	.839$\pm$.004	.851$\pm$.009

Classification vs. generation. Figure 3 compares classification and generation on identical backbones. Classification outperforms generation on every dataset for all 0.5B and 1.5B backbones, with average gains of 0.06–0.11 AUC. This advantage persists at 3B and 4B, with average gains of 0.02–0.06 AUC on Qwen2.5-3B, Llama-3.2-3B, and Gemma-3-4B. At 7B, classification matches generation on Qwen2.5-Math, with both achieving 0.941 average AUC. The general Qwen2.5-7B results suggest that more stable optimisation could further improve classification, as instability in some runs contributes to the 0.073 average AUC gap relative to generation. Across datasets, classification delivers its largest gains on MathShepherd and FoVer: averaged over the six backbones up to 4B, it improves AUC by 0.16 and 0.11, respectively, compared with gains below 0.01 on Epic50K and MMLU-Pro-CoT.

Model scale. Strong verification does not require large decoders. ModernBERT-Base (ModernBERT-B), with only 0.15B parameters, achieves 0.847 average AUC, outperforming every generative decoder up to 4B except Qwen2.5-3B, which has twenty times as many parameters. Increasing encoder size does not consistently improve performance (Table 2). Domain specialisation, however, can improve verification without increasing model size: Qwen2.5-Math-1.5B outperforms its general-purpose counterpart on every dataset under both objectives.

Head Initialisation Ablation

Decoder classification introduces a task-specific head whose initialisation can affect performance and training stability. We compare two strategies: zero initialisation sets $w_{\mathrm{Yes}}$, $w_{\mathrm{No}}$, and both biases to zero, initially assigning equal logits to both classes; verbalizer initialisation sets the class weight vectors to the language-model output embeddings of Yes and No, reusing the pretrained weights for scoring these verdict tokens. We train Qwen2.5-3B under both initialisations using the same data and random seeds.

Table 3 shows that verbalizer initialisation improves both performance and training stability, raising average AUC from 0.833 to 0.894 and reducing the standard deviation across seeds from 0.098 to 0.039. With zero initialisation, some runs substantially underperform the others. Verbalizer initialisation produces consistent results on PRM800K, Epic50K, and FoVer, with standard deviations of at most 0.008. Overall, verbalizer initialisation improves average AUC by 0.061 and reduces the standard deviation across seeds by approximately 60%, even with one underperforming run among the three seeds on MathShepherd and MMLU-Pro-CoT.

Dataset	Zero	Verbalizer
PRM800K	.722$\pm$.109	.858$\pm$.004
MathShepherd	.789$\pm$.118	.808$\pm$.097
Epic50K	.909$\pm$.125	.977$\pm$.008
FoVer	.857$\pm$.130	.977$\pm$.001
MMLU-Pro-CoT	.887$\pm$.010	.849$\pm$.085
Avg.	.833$\pm$.098	.894$\pm$.039

Annotated Data Scaling Ablation

To compare the data efficiency of classification and generation for step-level verification, we vary the number of annotated training problems over doubling budgets and include the full training set:

We use deterministic nested subsets, sampled at the problem level before conversion into step-level examples, while keeping the validation set, test set, and number of training epochs fixed. We compare classification and generation SFT on Qwen2.5-0.5B and Qwen2.5-3B, holding the backbone fixed within each comparison, and include ModernBERT-B as an encoder reference. Each configuration below the full-data budget is evaluated with a single run.

Figure 4 reports step-level AUC averaged over the five datasets, with the dashed line marking the corresponding full-data generation baseline. At both model sizes, classification outperforms generation on average at every budget dataset from 1,024 problems onwards. With just 4,096 training problems, classification matches the corresponding full-data generation baseline on average, using only 9–12% as many training problems. Generation makes its largest gains at the highest budgets and remains below the 0.15B ModernBERT-B at smaller budgets. These results demonstrate that classification achieves strong verification with substantially fewer annotated problems, an advantage that full-data comparisons alone do not capture.

Representation Analysis

We test whether classification SFT makes valid and invalid reasoning steps easier to distinguish from the model’s intermediate hidden states. This examines whether its advantage extends beyond the final prediction head to the representations learned within the backbone. We compare pretrained Qwen2.5-3B with its generation-SFT and classification-SFT variants. With each model frozen, we fit a separate logistic-regression probe at each layer to predict $y_i$ from the hidden state at the final non-padding input token [1]. Probe AUC measures how readily a linear classifier can recover verification labels from each layer’s representations.

Figure 5 suggests that classification’s advantage is reflected in intermediate backbone representations, with step-validity labels becoming more linearly recoverable well before the final prediction head.

caption:

:::

tbl:4: In-context verification improves with scale but stays below a fine-tuned 0.15B encoder on average. Step-level AUC of in-context verification with three demonstrations per query, retrieved from the training set, and deterministic scoring. Bold marks the best result per column. Avg. denotes the macro average AUC over five datasets. †The Gemini API does not expose token probabilities, so its AUC is computed from binary Yes/No verdicts rather than a continuous score.

In-Context Learning Baselines

We test whether LLMs can perform stepwise verification from labelled in-context examples, assessing whether prompting can substitute for task-specific training (Table 4). We evaluate Qwen2.5-Instruct from 0.5B to 7B and two API models, DeepSeek-V4.1-Flash [6] and Gemini-3.8-Flash [14]. Each prompt contains the premise, the hypothesis, and three labelled demonstrations retrieved by embedding similarity [37] (Wang et al. 2024a) from the same training pool used for fine-tuning. This keeps the source of supervision fixed, while providing it through in-context examples without parameter updates. We score each step using the Yes/No verdict probabilities. Including the demonstrations’ reasoning contexts makes these prompts three to four times as long as the corresponding fine-tuning inputs, requiring a substantial input token budget even in this three-shot setting.

Under this protocol, no prompted model matches the fine-tuned 0.15B ModernBERT-B classifier on average. Qwen2.5 benefits from scale but reaches only 0.663 average AUC at 7B. The API models perform better, achieving 0.733 for DeepSeek-V4.1-Flash and 0.815 for Gemini-3.8-Flash. However, ModernBERT-B achieves 0.847, exceeding even the strongest prompting baseline by 0.032 AUC with only 150 million parameters. These results extend the practical case for small classifiers beyond comparisons with generative fine-tuning: task-specific training enables a small verifier to outperform every evaluated prompting baseline on average, despite their access to labelled demonstrations at inference time. Together with the matched-backbone comparisons, they support our central finding that how a model is trained to verify reasoning can matter more than its size.

Discussion and Conclusion

Why classification helps. Classification has its largest advantage with smaller backbones and less training data. This advantage persists under verbalizer initialisation, where both objectives start from the same pretrained verdict logits. Generation normalises these logits over the full vocabulary and must suppress non-verdict tokens, whereas classification normalises only over the verdict labels. We conjecture that this additional requirement contributes to generation’s poorer performance when capacity or supervision is limited. This interpretation is consistent with prior findings on the sample efficiency of discriminative training (Gu et al., 2023) and the greater gains from scaling generative verifiers (Zhang et al., 2025a), as well as the disappearance of the gap on Qwen2.5-Math-7B. Our probing results also suggest that classification changes the information recoverable from backbone representations, although probing establishes that information is accessible, not that the model uses it in prediction [1].

Why initialisation matters. Classification head initialisation can change which objective performs better. A zero-initialised head transmits no gradient to the backbone on the first backward pass; in our experiments, some seeds also stall well below the performance of other runs (§ 5.2). Initialising from the verdict tokens reduces this variability and, at 3B, reverses the ranking against generation (Table 2 and Table 3). An unsuitable head initialisation can therefore lead comparisons to understate the effectiveness of classification. We recommend verdict-token initialisation and reporting results across random seeds.

Implications for verifier design. Our results support a small classifier trained on step labels as the default for direct stepwise verification, particularly when limited resources must support repeated checks throughout a solution. Domain-specific pretraining also matters: Qwen2.5-Math-1.5B with classification achieves 0.916 average AUC, outperforming the general-purpose 3B model under either objective. Our comparisons hold the backbone, training instances, prompt, and number of epochs fixed, while using each objective’s standard training recipe. They concern direct-verdict prediction; generative verifiers trained on verification rationales can also be data-efficient [21, 24]. Whether rationale supervision, test-time sampling, or scaling beyond 7B changes the relative advantage of classification remains an open question. Comparing these settings under the same controls would help distinguish the benefits of the generative objective from those of additional supervision and computation.

By formulating stepwise verification as NLI, we show that small classifiers can outperform generative verifiers with substantially more parameters and learn effectively from fewer annotated problems. Their advantage extends to the evaluated in-context baselines, where providing labelled demonstrations does not match task-specific training. These findings challenge the assumption that effective verification requires large generative models: how a verifier is trained can matter more than its size. Small classifiers therefore offer a practical approach to checking reasoning when repeated verification must fit within limited data and compute budgets.

Limitations

Annotation requirement. Classification makes more efficient use of step-level labels than generation, but does not eliminate the need for supervision. With only a few hundred annotated problems, all models in our data-scaling experiments remain substantially below their full-data AUC (§ 5.3). The benefit is therefore a reduction in annotation requirements, rather than independence from labelled data. For domains without existing step-level annotations, obtaining suitable training data remains a prerequisite for task-specific fine-tuning.

First-error identification. Our evaluation stops at the first annotated error, focusing on the earliest point at which a reasoning trajectory becomes invalid. This targets a practical use of verification: identifying a mistake before subsequent reasoning builds on it. Once an error has occurred, a later step may follow from an incorrect premise without being correct relative to the original problem, requiring a distinction between local entailment and overall correctness. Our protocol isolates first-error identification; it does not assess the detection of subsequent errors or recovery from earlier mistakes.

Task complexity. Our results demonstrate the effectiveness of small classifiers across mathematical, formal, and multi-domain reasoning tasks of varying difficulty. However, all five datasets contain solutions to self-contained problems, and performance on long formal proofs or research-level mathematics remains untested. Such tasks may involve dependencies beyond the evaluated models’ input windows, restricting access to premises needed for verification. This leaves open whether classification retains its advantages as reasoning depth and context requirements increase.

Ethical Considerations

Data and licences. We use five publicly released datasets and publicly released or API-served models under their respective licences and terms of use (Appendix § 13), and release no new dataset. Our use of the datasets follows their intended purpose of training and evaluating step-level verifiers of model-generated reasoning. All five are in English and contain model-generated solutions to mathematical, formal-logic, and subject-knowledge problems, with human or automatically assigned step labels. We did not conduct additional screening for personal or offensive content.

Potential benefits and risks. Small classifiers can reduce the computational cost of repeated verification relative to larger generative verifiers, making these checks more feasible in settings with limited resources. However, a verifier may accept an invalid step or reject a valid one. In educational applications, either error could mislead learners if predictions were presented as authoritative feedback. Verifier outputs should therefore support rather than replace human judgement. Errors and inconsistencies in the training annotations, including automatically assigned labels, may also affect the reliability of these predictions.

Use of AI assistants. We used AI assistants to support code development and language editing. The authors designed and verified the experiments and analyses and take responsibility for all reported results and claims.

Acknowledgments

We gratefully acknowledge the computational resources provided by the Alan Turing Institute and the University of Cambridge High Performance Computing (HPC) Service / CSD3. This material is based on research that is in part supported by DARPA for the SciFy program under agreement number HR00112520301. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either express or implied, of the DARPA or the U.S. Government.

Literature Review

Verification objectives differ in the form of the judgement. Discriminative reward models and PRMs ([3, 28] (Wang et al. 2024b; Zhang et al. 2025b; Xia et al. 2025); Gao et al. [11]) produce a classification score, while generative verifiers ([21] (Zhang et al. 2025a; Zhao et al. 2026; Zhong et al. 2025; She et al. 2025; Xiong et al. 2025; Zhu et al. 2026)) emit a token-level verdict, often after generating verification reasoning. DPO-trained verifiers ([18]) derive a score implicitly from the divergence between a policy and a reference model, and prompted general-purpose judges ([23] (Zheng et al. 2023)) use no task-specific training.

Table 5 lists the prior studies that compare classification with generation or use encoder verifiers, and marks which factors each holds fixed. GenRM (Zhang et al., 2025a) is the most controlled, comparing a discriminative reward model with direct and rationale-generating verifiers on the same Gemma backbones, but it verifies whole solutions rather than steps. At the step level, ThinkPRM ([21]) and Lee et al. [24] train their generative verifiers on verification rationales, and ThinkPRM uses about a hundredth of the labels of its discriminative baseline; GenPRM (Zhao et al., 2026) compares against classification PRMs released with other backbones and data. StepWiser (Xiong et al., 2025) treats direct-verdict generation as a discriminative judge and contrasts it only with judges that reason first, so classification and direct generation are never separated. Encoders appear as off-the-shelf NLI scorers ([34]) or as answer-level verifiers ([27]), not as step classifiers compared with decoders. Our comparison holds the backbone, labelled instances, and prompt fixed, trains the generative verifier to predict the verdict directly, adds encoder classifiers, and varies the annotation budget, so differences between the two objectives cannot be attributed to these factors.

Other work is adjacent: training objectives for discriminative scores (contrastive step scoring [22], pairwise preference [16], step-progress estimation [40], architectural changes to a discriminative PRM (Zhang et al., 2026), and the reliability of generated verification under repeated sampling (Ye et al., 2025). These address the reward-modelling objective or how a verifier is deployed at decoding time rather than the form of the judgement, so we discuss them here but omit them from the table.

Dataset Construction and Details

Dataset Sources and Annotation Semantics

Selection rationale. We select datasets with multi-step reasoning traces, step-level annotations, and minority-class supervision at a scale suitable for full-parameter classification fine-tuning. All five datasets are in English. Process-supervision corpora are a natural starting point because they attach feedback to intermediate reasoning states rather than outcomes alone [25] (Zheng et al. 2025b). Our mathematical core (PRM800K, MathShepherd, and Epic50K) holds the task domain approximately fixed while varying supervision among human correctness judgements, rollout-based answer reachability, and contribution-based automatic annotations. § 4.1 discusses how these sources differ in what a label measures. FoVer and MMLU-Pro-CoT extend the evaluation to formally grounded and multi-domain reasoning, respectively, testing whether findings persist across annotation regimes and beyond mathematics.

• PRM800K. PRM800K contains model-generated solutions to competition-level MATH problems with human judgements of whether each intermediate step is correct and reasonable [28]. It is the closest of the five datasets to direct local-validity supervision; we normalise its released labels to entailment and non-entailment.

• MathShepherd. MathShepherd provides automatic process supervision for GSM8K and MATH solutions by sampling continuations from intermediate states and checking their final answers (Wang et al., 2024b).

• Epic50K. Epic50K provides contribution-based automatic annotations for mathematical reasoning steps (Sun et al., 2025). From each released record, we reconstruct prefix–candidate trajectories, treating the accepted prefix as valid and using the candidate rating as the next-step label.

• FoVer. FoVer contains LLM-generated formal-logic and formal-proof traces labelled using formal verification tools, including Z3 and Isabelle [20]. We use the balanced Qwen2.5-7B subset combining both sources.

• MMLU-Pro-CoT. MMLU-Pro-CoT is the multi-domain synthetic reasoning corpus released with VersaPRM (Zeng et al., 2025). We use its step annotations across mathematical, scientific, engineering, social-science, and other knowledge-intensive tasks.

Preprocessing and Experimental Formatting

Verification instance construction. We first normalise each dataset into a shared schema containing a problem, ordered reasoning steps, and aligned labels. After constructing the data splits, we expand each trajectory into the local NLI instances defined in § 3.1, stopping after the first annotated error so that every hypothesis is evaluated against a prefix not already invalidated (Figure 6).

A trajectory whose first error occurs at position $k$ contributes $k-1$ entailment instances but only one non-entailment instance, while a correct trajectory contributes only entailment instances. This imbalance is why the training split is undersampled within each step position (§ 4.1), which preserves the position distribution.

In-context demonstration construction. The in-context models receive three demonstrations drawn only from the training partition. The retrieval pool is the full training set used for fine-tuning. When a prompt exceeds the 4,096-token context of the Qwen2.5-Instruct runs, demonstrations are dropped, oldest first, so the query step is never truncated. Demonstrations are retrieved by cosine similarity over all-MiniLM-L6-v2 embeddings of the candidate step and final 120 premise words [35, 37] (Wang et al. 2024a); each prompt includes both labels and prepends the demonstrations to the base prompt below. The prompt requests a direct verdict without a rationale.

Supervised training formats. All supervised conditions use the same verification instances

caption: tbl:5: Our comparison isolates the training objective for step-level verification. Each row is a prior study that compares classification with generation or uses encoder verifiers. Step level: verifies the validity of individual steps; Cls. vs. Gen.: compares a classifier with a generative verifier; Same backbone and Same labels: both are trained from the same pretrained model on the same labelled instances; Gen. without rationale: the generative verifier predicts its verdict directly; Label budget varied: the amount of annotated data is varied for both. ✓: yes; (✓): partly; –: no. $^{a}$Groups direct-verdict generation with classification as discriminative and contrasts both only with rationale-generating judges. $^{b}$Single-domain versus multi-domain training. $^{c}$Off-the-shelf NLI models, not trained on step labels.

:::

and binary supervision. Encoders receive paired premise–hypothesis inputs; generation SFT renders the same content with the template below and learns a complete Yes/No response; decoder classifiers predict the label from the final non-padding representation. We provide neither demonstrations nor verification rationales, preventing retrieval, additional supervision, and iterative generation from confounding the comparison. Thus, all conditions share input semantics and supervision, while the two decoder paradigms additionally share the backbone and differ primarily in whether the verdict is learned through next-token generation or sequence classification.

Base Verification Prompt

You are a strict mathematics tutor. Verify the logic of the following step.
### Context:
{problem_description}
Step 1: {step_1}
Step 2: {step_2}
...
### Step to Verify:
{current_step_to_verify}
### Verification:
Is this step correct? Answer with ‘Yes’ or ‘No’.

Dataset Statistics and Splits

We construct deterministic train, validation, and test partitions using the dataset seed before expanding trajectories into NLI instances. Partitions are split by question, so all trajectories for one question, and all candidate paths reconstructed from one source record, fall in the same partition. For PRM800K and MathShepherd, after removing test questions from training (§ 4.1), we hold out 1% of the remaining training questions for validation. Epic50K, FoVer, and MMLU-Pro-CoT each provide a single source partition: we reserve 10% of questions for testing and, of the remainder, 5% for validation on Epic50K and FoVer and 2% on MMLU-Pro-CoT.

To train on comparable amounts of data across datasets, we cap the number of training problems, each a labelled solution trajectory, at 46,000 of 468,066 for PRM800K, 37,000 of 190,607 for MathShepherd, and 38,000 of 74,079 for MMLU-Pro-CoT, sampled with the dataset seed. Epic50K (42,697) and FoVer (34,302) are used in full. Validation and test partitions are never subsampled.

Table 6 reports the number of premise–hypothesis instances after dataset normalisation, first-error truncation, and NLI conversion; these counts therefore differ from the number of original reasoning trajectories. Training counts are after merging duplicates and undersampling; the natural error ratio is the proportion of non-entailment instances in the unbalanced test split. We additionally report token-length statistics for the complete test-set NLI inputs before model-specific truncation. Lengths are measured using the BERT tokenizer, and the overflow columns show the proportion exceeding 512 and 2,048 tokens.

Dataset	Train	Val	Test	Ratio (%)	Mean ± Std	Med.	P90	Max	> 512	> 2048
PRM800K	39,742	19,575	70,548	8.3%	$231.8 \pm152.5$	191	438	1,262	6.1%	0.0%
MathShepherd	43,667	8,570	80,883	17.5%	$185.3 \pm131.9$	146	341	1,580	3.0%	0.0%
Epic50K	58,151	15,982	37,763	6.0%	$651.5 \pm861.4$	315	1,643	5,399	33.0%	7.8%
FoVer	44,399	5,464	10,806	24.0%	$304.9 \pm148.5$	266	529	936	11.6%	0.0%
MMLU-Pro-CoT	42,612	8,727	49,494	9.6%	$343.9 \pm228.3$	286	602	2,351	15.6%	0.1%

Implementation Details

Models

Table 7 summarises the evaluated backbones, parameter counts and context limits. The encoder suite covers four architectural families at base and large scales, allowing comparisons across both architecture and capacity. The decoder suite centres on Qwen2.5 to support scaling comparisons and matched generation–classification experiments within a common model family; Qwen2.5-Math tests domain-specialised pre-training, while Llama3.2-3B and Gemma-3-4B provide a cross-family comparison.

Model	Params.	Native	Used
Encoders
BERT-B	0.110B	512	512
RoBERTa-B	0.125B	512	512
ModernBERT-B	0.149B	8,192	2,048
DeBERTa-B	0.184B	512	512
BERT-L	0.340B	512	512
RoBERTa-L	0.355B	512	512
ModernBERT-L	0.395B	8,192	2,048
DeBERTa-L	0.435B	512	512
Decoders
Qwen2.5-0.5B	0.49B	32,768	2,048
Qwen2.5-1.5B	1.54B	32,768	2,048
Qwen2.5-Math-1.5B	1.54B	4,096	2,048
Qwen2.5-3B	3.09B	32,768	2,048
Llama-3.2-3B	3.21B	131,072	2,048
Gemma-3-4B	3.88B	131,072	2,048
Qwen2.5-7B	7.61B	131,072	2,048
Qwen2.5-Math-7B	7.61B	4,096	2,048

Context-length control. We use 512 tokens for BERT, RoBERTa, and DeBERTa, and 2,048 tokens for ModernBERT and every decoder condition, including decoder classification. Model inputs exceeding these limits are truncated from the left under the same policy during training and evaluation, preferentially removing the earliest premise tokens while retaining the candidate step and recent reasoning context. Table 6 reports overflow before this truncation.

Training precision. Every trained model keeps FP32 master parameters and uses BF16 autocast, except DeBERTa, which trains in full FP32. Distributed sharding changes memory placement but not the model objective or input construction.

Training Configuration

We use full-parameter fine-tuning with 8-bit AdamW ([7]), cosine learning-rate decay, a weight decay of 0.01, and gradient clipping at 1.0. All supervised experiments are run with seeds 1, 42, and 3407 on fixed data partitions. Each seed is launched in a fresh process, and the global random state is set before model construction so that parameter initialisation, data ordering, and training stochasticity vary without changing the underlying split. Encoder learning rates lie between $1 \times10^{-5}$ and $3 \times10^{-5}$; we use commonly adopted fine-tuning defaults for each encoder. Decoder generation SFT uses $2 \times10^{-5}$ and decoder classification uses $1 \times10^{-5}$. We train encoders for at most 5 epochs and decoders for 1 epoch. We use a global batch size of 32.

Encoder configurations follow standard full-parameter fine-tuning ranges rather than a single setting imposed across architectures. Encoders use a warmup ratio of 0.1, reduced to 0.02 on MathShepherd, and are evaluated periodically on the validation partition; the checkpoint with the highest validation AUC is retained, with early stopping based on the same metric. Decoders are trained for one epoch and keep the final checkpoint.

Generation and classification models are trained on the same verification instances and data partitions. Matched decoder conditions additionally share the backbone, context limit, cosine schedule, prescribed number of epochs, and final-checkpoint rule, isolating the principal experimental difference to whether the verdict is learned through next-token generation or a classification head. Generation SFT uses sequence packing, whereas classification processes verification instances independently; optimiser-step counts are therefore not directly comparable across the two objectives. We instead control data exposure by prescribing the number of epochs consistently within each paradigm. No test-set results are used for hyperparameter or checkpoint selection.

Evaluation Protocol

All supervised models produce a continuous non-entailment score for each verification instance. Encoder and decoder classifiers obtain this score by applying a two-class softmax to their classification logits. For generation SFT, we teacher-force the exact single-token Yes and No verbalizers, retrieve their conditional log-probabilities with vLLM, and normalise over the two alternatives. Both verbalizer-extended sequences are evaluated in one batched call with prefix caching, which reuses their shared prompt and avoids top-$k$ approximation or free-form output parsing. We verify that each verbalizer contributes exactly one token under the model-specific chat template and tokenizer.

The same test instances are scored independently by every supervised condition. Step-level AUC uses the continuous scores directly and is therefore threshold-free. Test labels are never used for checkpoint selection or hyperparameter choice.

We evaluate each seed separately and report the arithmetic mean and sample standard deviation across seeds. Because generation SFT and decoder classification use different readout mechanisms, their raw optimiser-step counts and inference calls are not treated as matched units; comparisons instead use identical test instances and the common non-entailment scoring interface described above.

Software and Hardware

All experiments use Python 3.12, PyTorch 2.11 with CUDA 12.8, Transformers 5.5.3, Datasets 4.0.0, and Accelerate 1.11.0. Generation SFT is run with LlamaFactory 0.9.5 (Zheng et al., 2024); fine-tuned generation and in-context models are scored with vLLM 0.25.1, and decoders use FlashAttention 2.8.3. Retrieval embeddings are computed with Sentence-Transformers 5.6.1 and AUC with scikit-learn 1.9.0.

All models are trained and evaluated on NVIDIA A100-PCIE-40GB GPUs. Table 8 gives the number of GPUs and the GPU-hours needed to train one model on one dataset with one seed; each entry of Table 2 is three such runs per dataset. Training all models in Table 2 takes about 950 GPU-hours in total.

Model	GPUs	GPU-hours
Encoders, base	1	0.2–0.5
Encoders, large	1	0.3–1.1
Decoders 0.5B	1	0.3–0.4
Decoders 1.5B	1	0.5–0.8
Decoders 3B–4B, Gen.	2	1.7–2.6
Decoders 3B–4B, Cls.	2	2.5–3.3
Decoders 7B, Gen.	4	7.8
Decoders 7B, Cls.	4	13.0

Layer-wise Probing Protocol

We analyse pretrained, generation-fine-tuned, and classification-fine-tuned Qwen2.5-3B checkpoints across all five evaluation datasets, using the seed-1 checkpoint of each fine-tuned model. For each dataset, the backbone is frozen and the three model states use the same deterministically sampled probe instances.

We extract the hidden state at the final non-padding token from the embedding output and every transformer block, holding the readout position fixed across model states. All three model states read the same rendered prompt as the fine-tuned decoders (Appendix § 10). We use at most 5,000 training instances and 5,000 validation instances. At each layer, we fit an independent standardised logistic-regression probe with L-BFGS, balanced class weights, tolerance $10^{-3}$, and at most 1,000 iterations. The inverse regularisation strength $C \in\{10^{-4}, 10^{-3}, 10^{-2}, 10^{-1}, 1\}$ is selected by AUC on a stratified 20% hold-out of the probe training instances, and the probe is then refit on all of them. The backbone remains frozen, and the same procedure is applied to every layer and model state.

Artifact Licences

Artifact	Licence
Datasets
PRM800K ([28])	MIT
MathShepherd ((Wang et al., 2024b))	None stated
Epic50K ((Sun et al., 2025))	Apache-2.0
FoVer ([20])	CC BY 4.0
MMLU-Pro-CoT ((Zeng et al., 2025))	MIT
Models
BERT ([8])	Apache-2.0
RoBERTa ([30])	MIT
DeBERTa ([17])	MIT
ModernBERT ((Warner et al., 2025))	Apache-2.0
Qwen2.5 (0.5B, 1.5B, 7B)	Apache-2.0
Qwen2.5 (3B) ((Yang et al., 2024a))	Qwen Research
Qwen2.5-Math ((Yang et al., 2024b))	Apache-2.0
Llama-3.2-3B ([31])	Llama 3.2
Gemma-3-4B ([12])	Gemma Terms
Gemini-3.8-Flash ([14])	API Terms
DeepSeek-V4.1-Flash ([6])	API Terms
all-MiniLM-L6-v2 ([35])	Apache-2.0

Table 9 lists the datasets and models we use with the licence under which each is distributed. We use every artifact for research only and release no new dataset.