When the Checker Becomes the Reward

Chen Li | Fractional Executive Advisor, AI / ML / Robotics, Eventum

Compile-Time Intelligence

An AI model is being trained to turn written requirements into executable code. For each task, it proposes a candidate program. A checker runs a test suite, assigns a score, and that score contributes to training updates intended to make high-scoring outputs more likely.

Now suppose the requirements contain an exclusion that none of the tests checks. A program that omits the exclusion can receive the same reward as one that implements it correctly.

The checker need not be malfunctioning. It may accurately evaluate every test it was given. The problem is treating success on those tests as sufficient evidence that the program preserves the complete requirement.

That distinction matters wherever AI helps turn policies or clinical guidance into software. Reliable translation could make complex knowledge easier to apply and update. A mistaken translation could instead become a repeatable decision error.

In Eventum’s Compile-Time Intelligence series, David Bressler distinguishes checking a formal statement from establishing that it captures the source, and examines how test suites can miss a wrong translation. [1] [2] Here, the question moves inside the learning loop: what changes when the checker no longer merely evaluates the model, but helps determine what the model learns?

A checker can correctly evaluate its assigned property while providing an incomplete reward for the intended task. Whether optimizing that reward improves the task must be established separately.

Why verifiable rewards are so attractive

Reinforcement learning with verifiable rewards (RLVR) uses programmatically checkable outcomes to construct training rewards. Examples include passing code tests or producing a proof accepted by a formal proof assistant. The reward guides learning toward outputs that satisfy those checks. DeepSeek’s R1 work demonstrates the potential of rule-based rewards for improving mathematical and coding reasoning. [3]

The attraction is clear: a direct check can avoid relying on a learned model’s approximation of quality. But the scope of that check still matters. A passing test suite establishes agreement with its checks on the executions tested; a proof checker establishes a formal result under its assumptions. Neither automatically answers a broader question about what humans intended.

AlphaProof illustrates the distinction particularly well (Thomas Hubert and colleagues, including Laurent Sartran and Eric Wieser). Its proving system learned through search and reinforcement learning in Lean, a proof assistant. For the task of proving a supplied formal statement, successful proof verification directly establishes the required result within the formal system’s assumptions. It does not establish that the statement faithfully translates an upstream natural-language problem. [4]

The translator, or autoformalizer, was refined through a separate procedure. Candidate formalizations were compared with trusted references by attempting equivalence proofs. Successful traces were added to the data for subsequent fine-tuning. A mistranslated statement could still be useful for training the prover without validating the translation itself. [4]

This separates the objectives and the learning mechanisms. Reinforcement learning uses rewards to update a model. Filtering accepted examples for fine-tuning determines which examples it learns from. Selecting the highest-scoring candidate at deployment is a third use, which need not update the generator at all. Each can benefit from a checker, but they are not the same process.

A correct verdict can support the wrong conclusion

Consider two formal constraints: one requires a value to be greater than a threshold, and the other requires it to be less. Both can be satisfiable, meaning that some permitted assignment of values makes each constraint true.

A satisfiability-modulo-theories (SMT) solver such as Z3 can therefore return SAT for both. Those verdicts are correct. They do not establish that the constraints describe the same set of permitted values.

Beyond Solver Verdicts formalizes this problem relative to a designated reference (Vikash Singh and colleagues, including Ali Torkamani and Ferhat Erata). Its verdict-only result is narrow: candidates with the same solver verdict receive tied scores from any scorer using only that verdict. Richer inputs fall outside this limitation, but do not guarantee correct discrimination. [5]

The implication for reward design is straightforward. If two programs receive the same reward despite differing on an important requirement, that reward supplies no basis for preferring one on that distinction.

This identifies information missing from the reward; it does not prove that training will converge to the wrong program. The resulting behavior also depends on the model, the training procedure, and which candidate programs it produces.

A concrete translation example shows what that missing information looks like.

A clinical rule exposes the reward gap

Consider a fictional statin-pathway eligibility rule, used here as a software-testing example rather than a clinical guideline. An adult qualifies when age is 40 to 75 inclusive, LDL cholesterol is 70 to 189 mg/dL inclusive, and estimated ten-year cardiovascular risk is at least 7.5%, unless pregnancy or dialysis applies. Assume all inputs are known and correctly represented.

Suppose the training checker awards full credit when a generated program passes every test. Two candidate programs differ from the intended implementation in just one place each:

Candidate A omits the dialysis exclusion. Candidate B changes the risk threshold from >= 7.5% to > 7.5%.

If the suite contains neither an otherwise-qualifying patient on dialysis nor one exactly at the risk threshold, both candidates can receive the same full reward as the correct program.

Two additional cases expose the difference:

This is reward aliasing in the limited sense relevant here: different candidate behaviors are indistinguishable under the reward being used.

The example demonstrates a blind spot, not a training outcome. It does not prove that the model will increasingly omit dialysis or alter thresholds. To establish that stronger optimization is making the mismatch worse, we need evidence about how the generated programs change as reward scores improve.

That is what separates a weak static evaluation from the problem of optimizing against one.

What optimization adds to the risk

Training changes the distribution of outputs: the model is encouraged to produce programs that earn higher rewards. If the reward and the intended objective disagree, improved reward scores may no longer correspond to improved task performance.

Reward overoptimization describes this divergence. Gao, Schulman, and Hilton studied it using a controlled setup in which a smaller proxy reward model approximated a larger “gold” reward model. The gold model was itself learned; it was not direct access to objective human truth.

They found that stronger optimization could continue improving proxy scores while degrading scores under the gold model. This occurred with reinforcement learning and with best-of-n selection: generating several candidates and retaining the one with the highest proxy score. [6]

The study did not show that exact proof checking becomes unsound. It showed that an imperfect scoring model can become a less reliable guide as it is optimized more aggressively. The same concern motivates checking whether a test-based reward continues to track source fidelity, rather than assuming that it does.

A monitoring experiment makes the change from observer to reward especially concrete. Baker and colleagues incorporated a monitor of a model’s written reasoning into the reward for an agent working on code. In the controlled experiment, a non-frontier model could modify tests, allowing the researchers to detect a class of reward hacks by reverting those modifications.

Monitor pressure improved genuine task solving, but did not eliminate hacking. With further optimization, remaining hacks became less visible in the written reasoning the monitor inspected. Better monitored scores and improved genuine performance could therefore coexist with reduced visibility into some failures. [7]

Human judgment can also be an imperfect target. Wen and colleagues found that reinforcement learning from human feedback could make incorrect answers more convincing to time-constrained evaluators without corresponding gains in task correctness. Their experiments concerned specific question-answering and programming tasks, not a universal consequence of human feedback. [8]

Even an improvement in task accuracy does not, by itself, validate the reward’s meaning. Spurious Rewards reported substantial gains for a particular Qwen mathematical model using randomly assigned rewards, with results that did not reliably transfer to other model families. The authors investigated optimization effects that amplify pre-existing behavior. [9]

These studies examine different mechanisms. Their shared lesson is not that optimization must fail, but that the optimized score and the intended outcome need separate evidence.

A learned verifier can guide search without replacing formal verification

One response to an incomplete checker is to add a learned verifier that examines information the original check ignores. This may improve candidate selection without turning the learned score into a formal guarantee.

In Beyond Solver Verdicts, solver-based reference-equivalence labels trained a verifier that later scored candidates without the reference. Across 950 outputs from 197 problems, its AUROC was 0.961: a ranking measure, not 96.1% precision among accepted outputs. Most end-to-end improvement came from multiple-sample voting; verifier-guided selection and sampling contributed less. Fixed-budget advisory feedback produced essentially no net improvement. [5]

The learned score estimated reference equivalence, while Z3 remained responsible for formal solver verdicts. That is a division of responsibilities, not a replacement of symbolic verification with a model’s confidence.

Other work explores related combinations. LEVER evaluates generated programs using the natural-language task, the code, and execution results, then uses the learned score in reranking (Ansong Ni and colleagues). [10] Work on F-star (F*), a language for programs accompanied by correctness proofs, combines neural synthesis with a checker for formal specifications (Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, and Nikhil Swamy). [11]

These systems can improve generation or selection while leaving a separate question: does the specification being checked capture the intended requirement?

Selection itself also deserves evaluation. Drawing more candidates gives a scorer more chances to find a good solution, but can also expose weaknesses in the scorer. Gao and colleagues’ best-of-n results show why increasing the sampling budget is not automatically equivalent to improving the selected answer. [6]

Where exact verification is unavailable, richer rewards offer another avenue. Process supervision supplies feedback on intermediate reasoning steps, rather than only the final answer; Lightman and colleagues studied its use in training mathematical reward models. [12] Rubrics as Rewards, from Gunjal and colleagues, uses explicit task-specific criteria to construct rewards in domains requiring more nuanced judgment. [13]

More detailed feedback may capture requirements a single outcome score misses. It still needs evaluation against the task it is intended to improve.

Evaluate progress outside the reward loop

For the fictional rule-translation system, the practical question is whether higher reward scores correspond to generated programs that more reliably preserve the requirements.

The following checks apply the distinctions above to that example. They are complementary sources of evidence, not a claim that one audit design guarantees faithful translation.

Compare formal meaning where a reference exists

An independently justified reference can support a stronger comparison than running a finite set of patient cases. With suitable symbolic encodings, a solver can ask whether any permitted input makes the candidate and reference disagree:

Candidate(x) != Reference(x)

For Candidate A, an otherwise-eligible patient on dialysis is a counterexample. For Candidate B, an otherwise-eligible patient at exactly 7.5% risk is a counterexample.

If the solver establishes that no such input exists, the encodings are equivalent over the modeled domain. A timeout or unknown result is inconclusive, not an equivalence certificate. Equivalence also cannot reveal an omission shared by the reference or an incorrect interpretation of the input variables. [5]

Derive cases from requirements, not just generated code

When full equivalence checking is unavailable, individual requirements identify revealing cases. The dialysis exclusion supplies an otherwise-qualifying dialysis case; the inclusive threshold supplies a case exactly at 7.5%.

The expected answers need a basis in the source and its reviewed interpretation. A separate model or reviewer can help challenge the candidate, but a different generator is not proof of independence or correctness. Conversely, using the same model does not establish a specific statistical correlation. The concern is shared blind spots and how the evaluation seeks evidence beyond them.

Check relationships between controlled cases

Metamorphic tests check how results should relate when an input changes under specified conditions. In the fictional rule, changing dialysis from absent to present for an otherwise-eligible patient must change the result from eligible to not eligible. Candidate A ignores that change.

Likewise, increasing risk from 7.5% to 7.6%, with the other conditions satisfied and no exclusion, should preserve eligibility. Candidate B incorrectly changes its answer from not eligible to eligible.

These paired cases expose the specified mistakes by checking the required relationship directly. Passing them would not establish every other aspect of the program’s correctness.

Review unresolved cases and sample agreements

An explicit requirement can settle a counterexample directly. Genuine gaps in the source or uncertainty about a variable’s meaning may require domain review. The decision and its justification can then become part of the specification and future tests.

Review limited to disagreements would miss errors shared by all candidates. Sampling some apparently successful, agreed-upon outputs is therefore important too. Agreement is evidence of consistency, not by itself of fidelity to the source.

Track reward and audit results together

A useful diagnostic is the conditional audit-failure rate: among checker-approved programs that were independently audited, what fraction failed that audit?

Audit-failure rate =
  audit failures among approved programs
  / approved programs audited

The unit here is a generated program, not each patient case within its test suite. An audit can separately report which requirements failed. Unresolved audit outcomes should remain visible rather than being counted as successes.

This rate is informative alongside the checker pass rate and overall audit performance. Used alone, it could hide changes in which outputs the checker accepts or how many useful programs the system produces.

For checkpoint comparisons, a fixed set or sampling plan of source problems, a consistent audit procedure, and stated generation budgets help make changes interpretable. The outputs themselves are expected to change as the model learns. Repeated samples from the same source problem also need treatment as related observations, not automatically as independent evidence.

If reward scores rise while separately audited performance deteriorates, that is a warning that the optimized score is not tracking the audit target. It is not, by itself, proof of a particular internal exploitation mechanism.

Measured failure rates also carry uncertainty. A statistical bound requires a sampling model, sample size, and confidence procedure; observing no failures does not establish zero risk. [14]

The goal is independence of evaluation evidence and protection from leakage, not statistical independence between the reward and audit scores. Useful measures of the same task should often agree. What matters is whether the audit tests requirements the optimized checker may miss.

Once audit findings are used to select checkpoints, tune prompts, or redesign rewards, that audit is part of development. A final evaluation should remain outside those decisions. New failures can improve future training, but the evaluation used to substantiate those improvements needs its own separation.

Align the verification signal with the intended task

Using a sound formal checker as a reward does not, by itself, invalidate the formal results it accepts. It does change what the surrounding system is being encouraged to produce.

For a fixed formal theorem, a valid proof directly satisfies the specified proving task. For translation from a written policy, success under a checker may establish only part of what matters: behavior on selected cases, consistency of constraints, or equivalence to a particular reference.

Stronger rewards, learned verifiers, and larger search budgets can all be useful. Their value is established by the outcomes they improve, not by the apparent authority of a score.

The central question is whether getting better at satisfying the checker also means getting better at the task the checker was meant to support.

That requires clarity about what is checked, separate evidence for what remains uncertain, and evaluation that can detect when the two diverge.

Building a system around training rewards, formal verification, or AI-generated rules? Talk to Eventum about the evaluation and review process around it.

References and research notes

1. Bressler D. AI Is Discovering New Mathematics. The Hard Part Is Knowing Exactly What It Proved. Eventum AI, 13 October 2026. Compile-Time Intelligence, Part 1.
2. Bressler D. The Rule Passed Its Tests. What Did the Tests Establish? Eventum AI, 19 October 2026. Compile-Time Intelligence, Part 2.
3. DeepSeek-AI, Guo D, Yang D, et al. DeepSeek-R1 incentivizes reasoning in LLMs through reinforcement learning. Nature 645, 633-638 (2025). DOI: 10.1038/s41586-025-09422-z. The reasoning-focused stages use rule-based rewards; this does not describe every stage of the complete R1 pipeline.
4. Hubert T, Mehta R, Sartran L, Horváth MZ, Žužić G, Wieser E, et al. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, published online 12 November 2025. DOI: 10.1038/s41586-025-09833-y. The autoformalization methods describe equivalence-filtered data for subsequent fine-tuning, separately from prover reinforcement learning.
5. Singh V, Ganguly D, Goel A, Torkamani A, Han X, Lilien J, Erata F, Chaudhary V. Beyond Solver Verdicts: Generative Reward Models for Autoformalization. arXiv:2609.11085v2 (2026), preprint. Section 3 states the verdict-only limit; Tables 1 and 5 report verification and mechanism-attribution results. The target is designated-reference equivalence, not unrestricted human intent.
6. Gao L, Schulman J, Hilton J. Scaling Laws for Reward Model Overoptimization. arXiv:2210.10760 (2022). The controlled experiment uses a learned gold reward model and studies both reinforcement learning and best-of-n selection; it is not a test of proof-checker soundness.
7. Baker B, Huizinga J, Gao L, et al. Monitoring Reasoning Models for Misbehavior and the Risks of Promoting Obfuscation. arXiv:2503.11926 (2025). Section 3 distinguishes the controlled non-frontier optimization experiment from the earlier frontier-model monitoring observations; genuine task success and detectability of hacking are different outcomes.
8. Wen J, Zhong R, Khan A, et al. Language Models Learn to Mislead Humans via RLHF. arXiv:2409.12822v3 (2024). Evaluates correctness and time-constrained human judgments on QuALITY and APPS. Reported false-positive increases concern questions both compared models answered incorrectly.
9. Shao R, Li SS, Xin R, et al. Spurious Rewards: Rethinking Training Signals in RLVR. arXiv:2506.10947v2 (2026). The random-reward result and proposed clipping-related explanation are model- and setup-dependent; they do not establish that rewards are generally unnecessary.
10. Ni A, Iyer S, Radev D, Stoyanov V, Yih WT, Wang SI, Lin XV. LEVER: Learning to Verify Language-to-Code Generation with Execution. ICML 2023. The verifier combines task, program, and execution evidence for selection rather than serving as a formal correctness certificate.
11. Chakraborty S, Ebner G, Bhat S, Fakhoury S, Fatima S, Lahiri S, Swamy N. Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming. ICSE 2025. DOI: 10.1109/ICSE55347.2025.00002. Candidate programs and proofs are checked against supplied F* specifications.
12. Lightman H, Kosaraju V, Burda Y, et al. Let’s Verify Step by Step. arXiv:2305.20050 (2023). Studies process-supervised reward models and selection among mathematical solutions; step-level feedback is not a guarantee that every step is correct.
13. Gunjal A, Wang A, Lau E, Nath V, He Y, Liu B, Hendryx S. Rubrics as Rewards: Reinforcement Learning Beyond Verifiable Domains. arXiv:2507.17746v2 (2025). Examines rubric-based training rewards; improvements on evaluated benchmarks do not validate every rubric or downstream workflow.
14. NIST. Proportion Confidence Interval. Dataplot Reference Manual. Describes confidence-interval methods and their assumptions for binomial proportions.