General Reasoning Evaluation and Layered Verification

I. Correct answers can conceal invalid reasoning and reverse model rankings

Checking the final answer is enough only when the answer is the entire deliverable. In the OlympiadBench and Omni-MATH samples analyzed for ProcessBench, 32.2% and 51.8% of solutions with correct final answers still contained process errors (ProcessBench, Section 3.3). Answer accuracy and the validity of a reasoning trace are distinct evaluation targets. For a task that also requires a derivation or a specified execution process, I examine domain assumptions, method applicability, supporting evidence, tool compliance, intermediate results and the conclusion. The model's displayed CoT and visible reasoning traces enter that examination as observable outputs that I cross-check against execution records. They are not direct records of its internal reasoning.

To see what this does to a score, suppose problems and model trajectories are drawn from a target capability distribution. Let $Z = 1$ indicate that the complete solution, including its reasoning steps and tool execution, is valid, and let $V = 1$ indicate that the evaluation protocol accepts it. For model $m$, define its true validity rate as $\theta_m = \Pr_m(Z = 1)$, its false acceptance rate as $\alpha_m = \Pr_m(V = 1 \mid Z = 0)$, and its false rejection rate as $\beta_m = \Pr_m(V = 0 \mid Z = 1)$. False acceptance can let through an unsupported derivation, or a tool call that produces the correct answer while violating a predefined execution requirement; false rejection can exclude a valid alternative derivation. By the law of total probability:

The term $\alpha_m(1 - \theta_m)$ credits invalid trajectories, while $-\beta_m\theta_m$ penalizes valid ones. Adding benchmark problems helps with only part of this: it reduces the sampling variance of $\hat{s}_m$ and leaves the structural gap $s_m - \theta_m$ in place. Models can also differ in how closely they adhere to evidence requirements, verification steps and tool permissions, and the resulting differences in $\alpha_m$ and $\beta_m$ can reverse their ranking. Suppose Models A and B have true validity rates of $\theta_A = 72\%$ and $\theta_B = 64\%$. If invalid trajectories pass the final-answer check with probabilities $\alpha_A = 4\%$ and $\alpha_B = 36\%$, with $\beta_A = \beta_B = 0\%$, their observed scores are $s_A = 73.12\%$ and $s_B = 76.96\%$, and the model with the lower rate of fully valid solutions ranks higher.

Process supervision extends evaluation to intermediate steps (Let's Verify Step by Step, Sections 2 and 3). When I apply it to general post-training evaluation, I account for omissions in reference solutions, accept valid alternative methods, and enforce evidence and execution requirements defined before responses are generated. Structural simplification can explain a method or reveal redundant work. Being slower or taking more attempts, however, does not by itself make a solution incorrect, so a resource-related rejection requires a hard limit specified in advance.

II. Proof obligations organize layered review and allow alternative solutions

A task specification defines the domain assumptions and execution constraints $\Gamma_q$, the target conclusion $C_q$, and the proof obligations needed to establish it. A model trajectory $\tau$, which here means its visible reasoning and observable execution records, may get there through different intermediate lemmas, representations or orders of deduction. That is allowed, because review concerns the submitted material and whether it fulfills the task's obligations. A directed acyclic dependency graph (DAG) $G$ organizes the local soundness check for each node $v_j$, together with a global tool-compliance predicate $\mathcal{T}_{\text{comp}}(\tau) \in \{0, 1\}$:

The symbol $\vdash$ denotes valid derivability within a sound domain inference system, and the condition $\mathcal{T}_{\text{comp}}(\tau) = 1$ certifies that each external tool invocation $t \in \tau$ belongs to the task's permitted execution environment $\mathcal{A}_q$. If root nodes follow from verified assumptions $\Gamma_q$, every dependency is sound, with its local derivation verified in that system, and $\mathcal{T}_{\text{comp}}(\tau) = 1$, structural induction over a topological ordering of $G$ establishes the full conclusion.

In production, I divided verification into three layers:

1. Code and rule checks cover the directly verifiable parts of an answer, required deliverables, and predefined restrictions on tools, execution environments and resources. Tool compliance requires $\mathcal{T}_{\text{comp}}(\tau) = 1$, and a call that violates an explicit hard requirement causes rejection ($V = 0$) even when the final answer is correct.

2. LLM-as-a-Judge assists with semantic screening. It flags insufficient evidence, misapplied rules, conclusions that exceed their premises and gaps in reasoning, and it links each concern to the relevant trace, tool response or intermediate output. These flags help direct further review.

3. Scholars with relevant expertise take the questions that require domain judgment, admit several reasonable interpretations, or remain disputed after the first two checks. They examine the evidence, the applicability of the method and the conclusion, and a question that cannot be resolved from the available evidence stays open.

All three layers work from the same observable material. I cross-check the model's displayed CoT and visible reasoning against actual tool calls, intermediate outputs, elapsed time and attempt counts. For each attempt I look for new evidence, revised premises or a change in the state of the solution. That is how I identify repeated calls, continued use of failed assumptions and loops that make no progress. Where the necessary execution records are missing, conclusions remain unverified. I record efficiency separately from correctness and compliance. Long runtimes, repeated attempts or exhaustive methods can warrant efficiency analysis, but they affect acceptance only when they violate a predefined hard limit.

Method applicability also needs its own check, because pointwise convergence at a fixed parameter value does not establish that an approximation remains valid within an optimization, an integral or an exchange of limits. A claim about the order of accuracy requires an approximation parameter, its domain of validity and a uniform error bound. When such issues cannot be decided programmatically, an LLM can help locate a concern and a specialist scholar can review the assumptions and derivation. That review carries a different evidentiary status from a checkable formal certificate.

For feedback, I record the first failed obligation at node $v_j$ and mark its descendant subgraph $\operatorname{desc}(v_j)$ as unverified, since locally correct calculations under a false premise do not repair the full derivation. This treatment addresses the ambiguity after an error discussed in ProcessBench, Section 3.1. A suspected error awaiting specialist review remains unresolved until that review is complete.

III. Error certificates for a programmatically verifiable subfamily

To test the programmatic layer, I use an optimization subfamily whose constraints and certificates can be checked explicitly. It shows whether certificate checks reject invalid submissions while retaining valid alternative proofs. Consider the equality-constrained strongly convex quadratic problem:

Here $H$ is symmetric, $Ax = b$ is feasible, and $\mu > 0$ is a verified lower bound on curvature. For any feasible candidate $x$ satisfying $Ax = b$, choose any dual multiplier vector $\nu$ and define the stationarity residual $r = Hx + c + A^\top \nu$. Strong convexity gives the first inequality below for every feasible displacement $d \in \ker A$, and completing the square in $d$ gives an exact optimality error certificate:

The operator $P_{\ker A}$ is the orthogonal projection onto the space of feasible directions $\ker A$. It removes residual components normal to the constraints, which do not affect optimality along the feasible manifold (Boyd and Vandenberghe, Convex Optimization, Sections 5.5 and 9.1). A zero projected residual, $P_{\ker A} r = 0$, certifies exact optimality, and otherwise the certificate bounds the suboptimality gap in objective units. Two kinds of submission fare differently under this check:

• Solutions derived through Lagrange multipliers or by eliminating the equality constraints can satisfy the same semantic obligations and pass verification.

• Reporting the correct optimal value $v^*$ alone does not fulfill these obligations. Feasibility and the claimed objective value have to be checked separately. A submission that claims a KKT multiplier witness must also have its full stationarity equation $Hx+c+A^\top\nu=0$ verified, because the projected-residual bound cannot validate that multiplier, given that $P_{\ker A}A^\top\nu=0$ for every $\nu$. A valid equality-elimination proof need not supply a multiplier witness.

I carry the lessons from this subfamily over to the structure of general review: check the inputs and assumptions, compliance with the execution specification, support for the derivation, and whether the conclusion exceeds the evidence. Obligations that admit programmatic checks go to rules or certificate verifiers, and other semantic questions go through LLM-assisted screening and specialist review. Structural simplification may explain why a method needs less repeated work, but efficiency gains and validity certificates are evaluated separately.

IV. Task transformations must propagate error bounds

Symbolic templates parameterize variable domains and answer formulas (GSM-Symbolic, Section 3.1). Tasks with formalizable transformations also need verifiable rules for how those transformations affect feasible sets, objective values and acceptance tolerances. I derived the exact tolerance-propagation rule below for bijective task transformations.

Let an original problem and its transformed variant have feasible sets $F$ and $F'$, objectives $J$ and $J'$, and finite infima $v$ and $v'$. Suppose the task designer verifies a bijection $\Phi : F \to F'$ such that every feasible $u \in F$ satisfies the uniform bound:

Taking infima in the first line gives the second, and subtracting the lower bound on $v'$ from the upper bound on $J'(\Phi(u))$ gives the third. So after a unit conversion, parameter rescaling or numerical transformation with error bounded by $\varepsilon$, the result determines the acceptance tolerance for a previously $\delta$-optimal solution. Keeping the original tolerance $\delta$ can misclassify a valid transformed solution as a model failure, while relaxing it arbitrarily can conceal a real capability gap. When $\varepsilon = 0$, the bijection and positive scaling $a > 0$ also preserve whether an optimum is attained. Changes to boundary compactness or admissible control classes require a new attainment proof.

V. Grading errors change the post-training objective

Step-level labels can improve post-training only if they measure logical validity and compliance, because systematic grading errors pass into the targets used by process reward models (PRMs) and RLHF policies. Let $h$ denote the task input and the model's visible reasoning prefix through the current step. Let $Z = 1$ indicate that the step is valid under the problem's assumptions, and let $V \in \{0, 1\}$ be the grader's noisy acceptance label, with conditional false acceptance $\alpha(h)$ and false rejection $\beta(h)$. Writing $p(h) = \Pr(Z = 1 \mid h)$, a process evaluator with logit $s$ trained by binary cross-entropy is optimized toward the corrupted conditional target:

The expected gradient difference shows which way grading bias moves the training target:

• If false rejection dominates, $\beta(h)p(h) > \alpha(h)[1-p(h)]$, then $\tilde{p}(h) < p(h)$. The learned validity target shifts downward, which penalizes valid alternative proofs.

• If false acceptance dominates, $\alpha(h)[1-p(h)] > \beta(h)p(h)$, then $\tilde{p}(h) > p(h)$. The target shifts upward, rewarding flawed proofs or noncompliant tool calls. When the weighted contributions are equal, the effects cancel in the conditional mean.

When $\alpha, \beta$ are known constants with $\alpha + \beta < 1$, class-conditional noise correction can remove bias from the mean estimate (Learning with Noisy Labels, Sections 2 and 3), at the cost of increasing variance by the following squared factor:

For task families whose validity is exactly decidable by a sound and complete certificate verifier, $\alpha=\beta=0$ removes this variance penalty. The stress test below evaluates the certificate method within such a programmatically decidable subfamily. Error rates for LLM-assisted labels and specialist review require separate calibration samples.

VI. Reproducible tests of false acceptance and false rejection

I constructed 600 strongly convex quadratic task families to test the certificate verifier within this subfamily. Using exact rational arithmetic, I generated 6 algebraic submissions per family, for 3,600 submissions in total:

• 1,200 valid certificates, 2 per family: one derived using Lagrange multipliers and one using equality elimination.

• 2,400 submissions with controlled defects, 4 per family: (1) an infeasible construction, $Ax \neq b$, that yields the exact optimal value $v^*$; (2) failure of stationarity along a feasible direction in $\ker A$ while reporting $v^*$; (3) a claimed multiplier that fails the stationarity equation while reporting $v^*$; and (4) an incorrect final objective value. The first three classes, comprising 1,800 submissions or 75% of all invalid submissions, report the correct final answer $v^*$.

I compared three deterministic acceptance protocols on all 3,600 submissions:

Within this exact-arithmetic benchmark, semantic certificate verification accepted 1,800 fewer invalid proofs than final-answer matching and retained 600 more valid alternative solutions than strict reference-path matching. It also passed all 600 feasible-perturbation checks on the projected-residual bound in Equation (4). Semantic certificate verification here means checking the constraints, objective value and certificate conditions explicitly. The reported error rates are those of the certificate verifier on this constructed benchmark, and LLM-assisted screening and review by specialist scholars are evaluated separately.

VII. Dependence within task families and the cost of expert review

Surface variations of one problem template do not provide independent observations of general reasoning ability. Suppose there are $F$ independent task families, each with $K$ variants, common marginal variance $\sigma^2$, and common pairwise within-family correlation $\rho$. The variance of the sample mean and the effective sample size $n_{\text{eff}}$ are:

For $F = 50$ families with $K = 8$ variants each, there are 400$400$ responses, and if $\rho = 0.6$, those 400$400$ responses provide the same precision as $n_{\text{eff}} \approx 77$ independent observations. Training and test sets therefore need to be split by task family, and new tasks should vary assumptions, evidentiary relationships or the structure of a derivation, beyond simply substituting numbers.

Within the programmatically verifiable subfamily, I account for the cost of certificate verification and human review separately. The following model compares automated certificate checking with the original workflow of reviewing every submission; the full three-layer process also incurs costs for model calls, calibration and review of disputed cases. Let $C_0$ be the upfront engineering cost of the proof-obligation certificates and verifier, $c_e$ the original expert review cost per submission, $c_v$ the automated verifier's unit execution cost, and $u$ the fraction of submissions escalated to human adjudication. Once false acceptance and false rejection standards are met, assume unit costs are stable and the same expert unit cost applies to escalated cases. The certificate workflow then reduces total cost when submission volume $N$ exceeds:

The evaluation workflow I developed combines task specifications, visible reasoning, execution evidence and layered review, with exact certificates where the problem class permits them. I report correctness, compliance and efficiency separately, which preserves the scope and evidentiary status of each assessment.