An aggregate can agree for the wrong reason
In an early Countdown training run, the original grader and its corrected replacement both awarded exactly one successful rollout out of 256. If I had compared only the batch accuracy, the repair would have looked irrelevant. The two graders had rewarded different rollouts.
The model was not stopped at its first closing answer tag. It continued writing, often inventing another user question and answering that instead. The original parser selected the last answer block. A later answer could accidentally solve the actual task even when the first answer did not; a later invented task could also obscure a correct first answer.
Re-scoring the retained batch found 166 extraction disagreements, one false positive and one false negative. Nearly 86% of the generated text came after the first answer. The arithmetic checker was evaluating expressions, but the surrounding system had not reliably identified which expression was the submitted answer.
The specification includes the boundary
The repair had two parts: stop generation at the closing answer tag, and grade the first answer after the reasoning section. Regression checks preserve both requirements. Fixing the parser alone would leave unnecessary continuation in the rollout; changing generation alone would leave a fragile scorer for older or malformed outputs.
This example is a grading vulnerability with observed consequences for reward assignment. It is not evidence that reinforcement learning taught the model to exploit the bug. Only one batch remains from the stopped first run, and a convincing claim of learned exploitation would require evidence about how the relevant behavior changed under optimization.
That distinction matters because an explanation can outrun its data. “The grader can reward the wrong answer” and “the agent learned to game the grader” motivate related investigations, but they are different empirical claims.
A repaired score still needs interpretation
After the repair, Countdown per-attempt accuracy rose from 1.3% at the base model to 55.7% at the final checkpoint. The evaluation used the same 256 puzzles and 32 samples per puzzle. Yet pass@32 reached 55.1% by step 50 and ended at 56.2%.
The later training mostly made successful answers more likely on a limited set of puzzles. A single rising accuracy curve would have hidden that structure. Matching the sampling budget and inspecting puzzle-level outcomes makes the interpretation more precise. The puzzles were excluded from training updates, but monitored during development; they were not an untouched final confirmation set.
A checker can tell us whether an answer passes its rule. Understanding what improved requires another layer of measurement: coverage, reliability, sampling, task difficulty and the ways the evaluation itself informed development.
The same problem appears in a learning product
Cognanimus checks numeric and structured answers locally and uses explicit rubrics for written work. That separation limits what a language-model judgment can control, but it does not make the rubric automatically correct.
One grading investigation found a hidden requirement: a response explained what the question asked, while the rubric also demanded additional information. The system was enforcing a criterion that the learner had not been given. The repair changed the public criteria and kept the historical submission and correction record.
Another case exposed an ambiguous partial-credit boundary. The expected score remained fixed, the rubric was clarified, and an opposite-side boundary case was added so the fix would not simply suppress valid partial credit. Passing examples become more informative when the neighboring failure cases are explicit.
Formal verification sharpens the promise
The BusyCoq contributions use a stronger acceptance mechanism: exact machine statements checked by Rocq/Coq. Search can propose an invariant or an accelerated execution batch, while a separate checker decides whether the proof follows from the framework.
Even here, the claim must match the theorem. One accepted submission proves that a machine halts. The approximately 1.77 × 10^44 step count is computed separately; that number is not proved by the halting theorem. The assumption report is also part of the result, not an implementation footnote.
Across these projects, my working rule is to keep four things together: the intended task, the exact accepted object, the evidence for accepting it and the claim the result supports. Mechanical checks are valuable precisely because their scope can be inspected. Their usefulness increases when the surrounding experiment and explanation respect that scope.
References & artifacts
An evidence-based synthesis of the linked project records. Report timestamps and experimental conditions are retained in the source artifacts.