A: Mathematical reasoning

Case A evaluates mathematical reasoning: whether a model reliably solves a target population of math problems. One construct meets four mechanisms — an answer checker, a proof assistant, a process reward model, and mathematicians — in three regimes: benchmark reporting, best-of-N selection, and RLVR training.

Claim and decision#

The case uses an illustrative deployment, the one the Studio preset loads: a competition-math model behind a math tutor.

• Construct: reliably solving competition and proof-style problems from the target population.
• Population: problems from AMC to olympiad level, plus short proofs, stratified by topic and difficulty and released after the model's training cutoff.
• Environment and harness: single-turn generation with a scratchpad and no tools except an optional calculator; a fixed prompt template, temperature, and answer-extraction rules.
• Validity domain: English problems with numeric or short symbolic answers, and formalizable proofs.
• Decision: which checkpoint to release, and which of 16 sampled solutions the user sees.

The claim excludes general mathematical research ability and the pedagogical quality of explanations.

Report, select, train#

Two migrations are foreseeable: the held-out set leaking into training data, and selection drifting toward its scorer's quirks. A third risk is built in: the checker that grades the report is also the RLVR reward.

Criteria and mechanisms#

The specification asks for a correct final result, no forbidden tool leakage, and optionally valid intermediate steps, each routed to its own mechanism:

A PRM is not "above" the checker: it is usually epistemically weaker but diagnostically denser. A step score locates where a failing solution went wrong, which no final-answer verdict can, but its errors are learned. Process evaluation earns its place because lucky outcomes can hide bad procedures: filtering by final-answer correctness admits right answers reached by faulty reasoning (Chen, Wang & Qu, 2026, §4.1), and process supervision can outperform outcome-only supervision for training (Lightman et al., 2023).

Faithful reasoning is therefore advisory: a solver may use any valid derivation, and rollout-labeled step scores estimate something closer to a policy-conditioned value than to the step's quality, so step scores never enter the release number. No forbidden tool use is fatal, with zero forbidden calls allowed. The final answer and the proof are tradeable: their verdicts average into the accuracy, reported per stratum.

Checker normalization and the trusted base#

The final-answer checker's normalization code decides what counts as correct. The outcome-validity checks for answer matching ask whether the checker accepts expressions semantically equivalent to the reference (O.a.1) and resists an answer that lists every possibility (O.b.2), and whether the problem states the required answer format (O.h.1) and makes guessing unlikely (O.h.2) (Zhu et al., 2025, via Song, 2025, slides 42 and 45). False rejects understate capability; false accepts overstate it. See the MATH card for a public example.

Measure those errors on the solver policy's own outputs. RLVR moves the policy toward whatever the checker accepts, so a false-accept rate estimated on reference solutions or an earlier checkpoint need not transport; re-estimate it at every checkpoint (see Case E).

The proof assistant is the one sound mechanism here: if the configured checker accepts, the formal statement holds. The guarantee belongs to a configured trusted base — theorem statements, permitted axioms, checker version, kernel configuration, and whether the optimizer can modify them — and under search the Goodhart boundary moves to those surfaces. A proof of a mis-formalized statement proves the wrong theorem, so mathematicians review each formalization, and statements stay outside the modification surface.

Selection: pass@k is a ceiling#

pass@k is the probability that at least one of k attempts succeeds; pass^k, that all k succeed. If each sampled solution to a hard problem is correct 25% of the time (illustrative), sixteen independent samples contain a correct one 99.0% of the time; all sixteen are almost never correct. pass@16 is what best-of-16 would deliver with a selector that never errs: a ceiling, not an accuracy. Set k to 1 for what one sample delivers.

At inference there is no reference answer, so the selector must be reference-free: a learned judge such as a reward model, or the proof assistant for formally stated problems. The benign best-of-N selection model, a model and not a theorem, assumes independent candidates, true- and false-positive rates $t$ and $f$ that hold on every candidate, and a uniform choice among flagged ones; under it, a flagged candidate is correct with probability $pt / (pt + (1-p)f)$ at every N.

The calculator, which calls the selector a verifier, starts at an illustrative $t = 0.90$ and $f = 0.10$: at N = 16 the selected solution is correct 74.8% of the time, and no N lifts it past the 75% ceiling. Set t to 100% and f to 0%, the proof assistant's case relative to its trusted base, and selection reaches 99.0%. Then switch to continuous scores: if 2% of wrong answers score like exploits (illustrative), the top-scored pick peaks near N = 13 at 72% and falls to 0.3% by N = 1,024. Only the real optimizer shows which curve applies.

Validation plan#

Each row is a planned, not yet measured, entry in the validation profile Π.

Channels and tripwires#

Keep three measurement channels apart: the optimized RLVR reward; the anchor channel, the post-cutoff report set graded by the checker plus an independent algebra check and a mathematician sample, queried once per release and tracked in an anchor burn ledger; and production, the answers best-of-16 serves, audited on a sample. Training reward rising while the anchor channel stays flat signals proxy corruption, such as checker exploitation; both rising while audited production answers do not signals a construct or deployment mismatch; a stratum near its ceiling signals saturation.

Validity statement#

Following the validity-statement template, and stated as a plan until the profile is measured:

The math release evaluator — answer extraction with normalization and a symbolic equivalence check, a proof assistant for the formal subset, a PRM for step diagnosis only, and two mathematicians who adjudicate — is designed to support the claim that the model reliably solves competition problems from AMC to olympiad level and short proofs, for the research leads' checkpoint-release decision and the serving stack's choice among 16 samples, over English problems with numeric or short symbolic answers released after the training cutoff and formalizable proofs, under RLVR training against the same answer checker with reward-only access and best-of-16 selection by a learned judge at inference, up to tested exposures $b^{*}$, in training steps and in N, that have not yet been measured, with a validation profile that is planned rather than measured, relative to the proof assistant's configured trusted base for the formal subset and to two mathematicians, whose agreement is still to be measured, for notation and proof quality. Ambiguous notation, proof quality beyond formal validity, and revisions to the specification remain human judgment.

Common failure modes#

• pass@k reported as accuracy — a table shows pass@16 for a system that serves one answer → report the checker's verdict on the selected answer, with n and an interval. See one-number reporting.
• Checker exploitation under RLVR — the training reward climbs while an independent check of held-out answers stays flat → re-estimate checker error on-policy; certify with a different mechanism. See reward hacking.

Check yourself#

Analyze. Why can RLVR still reward a flawed reasoning trace that reaches a correct final answer? Which criterion in this case would catch it, and at which resolution?

Hint

The reward reads only the final answer. The PRM can localize a lucky guess at step resolution, as an advisory signal; the proof assistant and the mathematicians decide.

Evaluate. A colleague proposes making PRM scores the release metric because the PRM inspects every step. Argue for or against.

Hint

Separate diagnostic density from epistemic strength: which mechanism's acceptance rests on a reference answer or a formal semantics, and which has learned errors?

Create. Write the final-answer checker's normalization test suite: equivalent forms it must accept, hedges and guesses it must reject, and how you will estimate its false-accept rate on each checkpoint's outputs.

Hint

Start from O.a.1, O.b.2, and O.h.1–O.h.2; stratify by answer type; send every disagreement with an independent algebra check to the mathematicians.

Further reading#

• Adaptive validity — the best-of-N selection model, the scalar tail case, and exploitability curves.
• Signals and resolution — why PRM scores, value estimates, and robustness margins are different objects.
• Case E: Reasoning-model training — dense rewards for development, an untouched certification channel.
• Lightman et al. (2023), "Let's verify step by step" — step-level supervision for mathematical reasoning.

Open this case in the Studio to start an evaluator dossier with its claim and regimes pre-filled.