Verification and supervision in scientific reasoning tasks

Project 3: Scientific Reasoning Evaluation and Task Design
Author: Theodore Ouyang

Controlling evaluation errors and supervision bias through proof obligations, error certificates, and task families

I designed a series of scientific reasoning tasks for a frontier AI research laboratory, specifying the target capabilities, original problems, reference arguments, and failure feedback as part of the deliverable. The research question was how to determine whether a model that produces a seemingly complete scientific solution has mastered the required principles, and how expert-produced data can provide reliable signals for model comparison and post-training research. This article develops a formal account of that approach to task design and acceptance, then tests its mechanisms through reproducible certificate stress tests.

1 Correct final answers can conceal invalid reasoning and reverse model rankings

Checking only the final answer is appropriate when that answer constitutes the complete deliverable. Scientific reasoning research often requires the model formulation, theorem assumptions, derivation, and conclusion to hold together. In the specifically selected OlympiadBench and Omni-MATH samples used to construct ProcessBench, 32.2% and 51.8% of solutions with correct final answers, respectively, still contained process errors. These rates do not generalize to arbitrary models, but they establish that answer checking and process validity measure different things. ProcessBench, Section 3.3

Suppose problems and responses come from a predefined target distribution. Let $Z=1$ mean that the complete solution is valid, and $V=1$ mean that the acceptance protocol passes it. For model $m$, let $\theta_m=\Pr_m(Z=1)$ be its true validity rate, $\alpha_m=\Pr_m(V=1\mid Z=0)$ its false acceptance rate on invalid solutions, and $\beta_m=\Pr_m(V=0\mid Z=1)$ its false rejection rate on valid solutions. The law of total probability gives:

The first term credits invalid solutions; the second penalizes valid ones. Adding more problems can reduce sampling error in the estimate of $s_m$, but it does not automatically remove the gap between that quantity and $\theta_m$. Models make different kinds of errors, so their $\alpha_m$ and $\beta_m$ can differ enough to reverse their ranking. In a specified arithmetic scenario, for example, two models have validity rates of 72% and 64%. Their invalid solutions happen to pass an answer check with probabilities of 4% and 36%, respectively, while all valid solutions pass. Their observed scores become 73.12% and 76.96%. This example illustrates a ranking risk; it is not a measurement of the project's models.

Process supervision extends evaluation to intermediate steps, as Lightman and colleagues demonstrated. Producing scientific tasks also requires attention to omissions in reference solutions, valid methods that differ from the reference path, and superficially similar variants that change a theorem's assumptions. I incorporated these issues into the task specifications so that the basis for acceptance was developed alongside each problem, before model responses were available. Let's Verify Step by Step, Sections 2 and 3

2 Define acceptance through proof obligations and allow valid alternative solutions

A task deliverable includes its assumptions $\Gamma_q$, the conclusion $C_q$ that must hold, and the proof obligations needed to establish it. A response may choose its own lemmas and order of proof. Acceptance depends on whether it fulfills the obligations. Organizing the response as an acyclic dependency graph gives the following local check for node $v_j$:

Here, $\vdash$ denotes derivability in the sound inference system being used. If the roots follow from verified assumptions and each inference represented by a dependency is sound, induction over a topological ordering establishes the complete conclusion from the local checks. The reusable specification therefore identifies what must be proved while allowing the author to choose a valid proof. The graph organizes dependencies; filling its nodes or asking a language model whether they look plausible does not establish soundness.

In implementation, I organized the central obligations around a valid model formulation, the applicability of the chosen method, sound derivations, and a conclusion with sufficient logical strength. Each had a corresponding verification procedure. Algebraic identities could be checked symbolically. Numerical constructions required feasibility checks and error bounds. Existence claims and exchanges of limits required explicit assumptions and justification. Unresolved obligations went to expert review instead of being forced into an incorrect label. Reference solutions underwent the same obligation checks, so the reference text itself was not treated as an unquestionable authority.

Physics tasks require particular care in distinguishing pointwise approximation from uniform error control over the task's parameter domain. Convergence at a fixed parameter value does not establish that the approximation remains valid inside an optimization, an integral, or an exchange of limits. If the optimizer approaches a boundary as the approximation parameter changes, the original error control may fail. The acceptance specification should require authors to state the approximation parameter, its domain of validity, and the required type of error bound before deciding the order of accuracy that the reference solution can support. In risk engineering tasks, the corresponding obligations concern the distributional and dependence assumptions behind a tail probability bound, and whether the guarantee survives a change in those assumptions. These conditions determine whether a problem is valid research material and which part of its argument needs expert review.

The same interface governs feedback after the first error. Algebra that is locally correct under a false premise does not restore the validity of the whole proof. Recording the first failed obligation and its affected successors preserves the distinction between a locally valid inference and an inference that supports the original problem's conclusion. ProcessBench also observes that the correctness of steps after the first error can become ambiguous. The dependency structure makes that ambiguity an explicit object of review. ProcessBench, Section 3.1

3 Produce an error certificate as part of acceptance

An executable optimization subfamily illustrates this interface. Consider the strongly convex quadratic problem:

Here, $H$ is symmetric, the constraints are feasible, and $\mu$ is a verified lower bound on curvature. For a feasible candidate $x$, choose any multiplier $\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$. Completing the square in $d$ then yields an optimality error certificate:

The operator $P_{\ker A}$ is the orthogonal projection onto the space of feasible directions. It removes residual components normal to the constraints, which do not affect optimality along feasible directions. A zero projected residual certifies that the feasible point is optimal. Otherwise, the certificate bounds the optimality gap in the units of the objective, making it directly comparable with the task's required accuracy. The derivation uses standard strong convexity and constrained optimization theory. Its engineering purpose is to base acceptance on a proved error bound, rather than on numerical proximity to a reference value. Boyd and Vandenberghe, Convex Optimization, Sections 5.5 and 9.1

Solutions obtained through Lagrange multipliers or by first eliminating the equality constraints can thus map to the same obligations. Conversely, reproducing the correct optimal value does not make a complete solution valid if its construction is infeasible or its argument fails to support the claimed accuracy. The task specification must state the allowed error and whether verification uses exact arithmetic or certified numerical bounds. A small floating-point residual alone is not a proof.

Optimization certificates are one instance within the task families. In an original kinematics problem from the project, I used the path invariance of vertical travel time to reduce the problem to horizontal scheduling. The analysis separately established an attained minimum completion time, an unattained supremum, and harmonic-number asymptotics for a staircase construction approaching the supremum. The example illustrates why feasibility, optimal bounds, and attainment require separate proof obligations, even when the final value is correct.

4 Task expansion must propagate mathematical error

GSM-Symbolic parameterizes variable domains, validity conditions, and answer calculations together. Scientific tasks also need verifiable relations specifying how an expansion changes the feasible set, objective values, and error tolerances. GSM-Symbolic, Section 3.1

Let the original problem and its variant have feasible sets $\mathcal F$ and $\mathcal F'$, with objectives $J$ and $J'$. Suppose the task designer has verified a bijection $\Phi:\mathcal F\to\mathcal F'$ and the following relation for every feasible $u$:

Here, $v,v'$ are finite infima. Taking infima on both sides of the first line gives the second. Subtracting the lower bound on the new optimum from the upper bound on the transformed candidate gives the third. This answers a practical question: after a unit conversion, parameter rescaling, or numerical transformation with bounded error, what acceptance standard should apply to a previously $\delta$-optimal answer? Retaining the original tolerance can misclassify transformation error as model failure. Relaxing it without a bound can conceal a genuine capability gap.

When $\varepsilon=0$, the bijection and positive scaling also preserve whether an optimum is attained. With only a nonzero error bound, equation (5) controls values and approximate optimality; it does not establish attainment. Variants that change endpoints, compactness, or the admissible class of controls require the relevant obligations to be proved again. This gives task families two research uses. Structure-preserving variants test stability under changes in surface form. Variants that alter a decisive assumption test whether the model understands that condition. Their reference conclusions and scoring rules must remain distinct.

5 Label quality determines what post-training research optimizes

More granular process labels are useful only if they measure the intended property. Systematic errors in those labels can be learned by a downstream model. In this section, $Z=1$ means that the current step is valid under the problem's assumptions and valid premises, and $V$ is the acceptance label for that step. Correspondingly, $\alpha(h),\beta(h)$ are its conditional false acceptance and false rejection rates. Let the input $h$ consist of the problem and the reasoning prefix through the step being evaluated, and define $p(h)=\Pr(Z=1\mid h)$. For a process evaluator trained with binary cross-entropy, noisy labels imply the following conditional target:

Here, $s$ is the evaluator's logit. The final line shows directly how false acceptance and false rejection shift the gradient away from the true validity target. If a class of valid alternative proofs is frequently rejected, the evaluator will systematically discount it. If solutions that omit boundary conditions often produce the correct final answer, those errors may be learned as acceptable. This explains mathematically why improving acceptance procedures for scientific data can benefit post-training research; it does not promise a gain from any particular training run.

Research on class-conditional label noise provides loss-correction methods, but these require the relevant noise structure and identifiable error rates. Even the simple case of fixed error rates exposes a cost. For the acceptance mean $\bar V$ of independent samples, if $\alpha,\beta$ are known and $\alpha+\beta<1$, then

The correction removes mean bias in this setting but inflates variance. Estimation becomes less stable as the error rates approach the non-identifiable regime. If error rates vary with task family, difficulty, or proof style, a single global correction can leave residual bias. I therefore placed reference verification, support for alternative solutions, and documentation of error causes within data production. This improves the supervision being supplied and leaves subsequent research to determine whether further correction is warranted. Learning with Noisy Labels, Sections 2 and 3

6 Reproducible stress tests for false acceptance and false rejection

To test these acceptance mechanisms, I constructed 600 strongly convex quadratic task families and generated six algebraic submissions per family, for 3,600 submissions in total, using exact rational arithmetic. Each family contained two valid certificates, one in Lagrangian form and one in elimination form. Four further submissions introduced controlled errors: an infeasible construction, failed stationarity along a feasible direction, a submitted multiplier that did not support the claimed stationarity equation, and an incorrect final value. The first three error types retained the correct final value to test the blind spots of answer checking.

The test compared three deterministic protocols: final-answer matching alone; a strict-path ablation requiring exact agreement with the reference route and certificate; and a certificate protocol that accepted different representations while checking each semantic obligation. The strict-path protocol is an ablation designed to isolate a mechanism, not a description of all existing process-supervision methods.

Within this explicitly enumerated test, the certificate protocol admitted 1,800 fewer invalid certificates than the final-answer baseline and retained 600 more valid submissions than the strict-path baseline. The residual bound in equation (4) also passed all 600 feasible-perturbation checks. These differences follow from what each protocol examines: one checks a numerical value, another also requires an identical representation, and the certificate protocol verifies mathematical conditions that support the conclusion.

These are results from the constructed verifier experiments in this article; the error types and their frequencies are set by the experimental design. The experiment validates an implementation for a finite algebraic subfamily. It does not estimate error rates on open-ended scientific problems or measure customer-model performance or training gains. Production trials should test the same two error types on unseen task families, naturally generated model responses, and independent expert references.

The next experiment should separate the source of the answers, the acceptance protocol, and final adjudication. First fix a collection of naturally generated responses from several models. Then randomly assign review protocols to reviewers while concealing model identity. An independent adjudication group should establish the references, and its review should extend beyond responses flagged as wrong by the new protocol. Random audit coverage is needed to estimate both false acceptance and false rejection. Reviewing only difficult cases selected for escalation estimates the error rate of that queue, not of the full production distribution.

The comparison should also cover omissions injected into reference solutions, valid but uncommon proof paths, responses to changed assumptions, and passages that cannot be adjudicated immediately. Reporting these strata separately reveals whether a protocol raises apparent precision by rejecting more responses or increases output by accepting more. The unresolved rate and additional expert time must both remain visible. In research production, reducing one kind of grading error while substantially increasing another can redirect subsequent model research. Both error types and adjudication coverage therefore belong in the acceptance criteria.

7 Account for dependence within task families and the full cost of expert review

Generating many variants of one problem does not provide the same number of independent observations of capability. Suppose there are $F$ independent task families, each with $K$ variants. In a balanced setting with common variance $\sigma^2$ and within-family correlation $\rho$:

This follows directly from the within-family covariance terms in the variance of the mean. If 50 task families each have 8 variants and $\rho=0.6$, the 400 responses provide approximately the same precision for estimating a mean as 77 independent observations. An empirical analysis should estimate the dependence structure, split training and evaluation data by task family, resample at the family level, and group closely related generation templates together. Broader capability coverage requires additional independent combinations of principles, not simply more numerical variants of the same template.

Production adoption also requires full cost accounting. Let $C_0$ be the initial cost of building the certificates and verifier, $c_e$ the existing workflow's expert acceptance cost per submission, $c_v$ the new workflow's basic verification cost per submission, and $u$ the fraction requiring escalation to human review. Once the predefined false acceptance and false rejection standards are met, the new workflow costs less when:

The accounting includes task specifications, reference proofs, certification of transformations, and tool maintenance in the setup cost, with rework and escalated adjudication included in operating costs. Equation (9) gives a scale threshold that can be evaluated using pilot data. A verifier that works for very few tasks and frequently needs human intervention may be unsuitable for sustained production even if its accuracy is high on those tasks.

The final comparison should hold model versions, response sets, expert budgets, and independent references fixed. It should report complete-solution validity, false acceptance of invalid solutions, false rejection of valid alternatives, the unresolved rate, and the total cost per accepted task family. Subsequent post-training experiments should also fix the training budget and data volume, then test transfer to unseen task families. The research contribution connects these decisions: task specifications define the capability to be measured, proof obligations determine what constitutes evidence, acceptance errors determine bias in the supervision signal, and analysis of task families and costs determines whether the approach can support continued expansion.