2026.10.16

The limitation and the change

Code agents can pass tests while failing on inputs the tests do not cover. A formal verifier offers a stronger oracle relative to a specification, but a binary accept/reject signal provides no learning gradient when every candidate fails. The earlier SWE-Proof work supplied real issue tasks with formal specifications and verified reference implementations; this paper’s methodological increment is the training environment and reward, not the benchmark construction.

Before each episode, the environment fixes the set and denominator of proof obligations for the instance. The agent can submit candidates to a live verifier over multiple turns and receive diagnostics. Its reward is a weighted fraction of obligations discharged, with hidden isolated assertions derived from reference-proof annotations for annotation repair. Because the denominator is fixed, adding trivial annotations or weakening the candidate’s own proof burden does not directly increase the score. An integrity audit overrides the verifier: candidates that alter the specification or introduce constructs that let verification escape the intended proof are rejected.

What the controlled evidence says

The cleanest comparison is the matched binary-reward ablation on DafnyBench. For the 35B-A3B model, verifier-grounded reward reaches 76.7% rather than 75.2% on annotation repair, and 93.5% rather than 71.0% on code generation. The environment, hyperparameters, training steps, and verifier-graded episode batches are otherwise held constant, so this comparison isolates the candidate-reward change more closely than a comparison across unrelated systems.

The held-out SWE-Proof result is larger but answers a different question. For the same 35B-A3B model, annotation-repair verification rises from 3.1% to 68.8%, while code-generation verification rises from 56.3% to 100.0%. In a separate repository-patch task, the specialist-assisted setting raises held-out issue resolution from 59.6% to 72.5%; resolution is determined by each project’s withheld tests, not verification alone. These results support inspecting the reward design and specialist condition separately rather than treating them as one end-to-end effect.

What to carry into a new experiment

Treat the audit as a second instrument, not as evidence that the specification is correct: verification establishes fidelity to the supplied contract, while whether that contract expresses intended behavior remains a human responsibility. Audit coverage also depends on correctly enumerating verification-escaping constructs for the language in use.

A useful replication operation is to keep the environment, training schedule, and verifier batches fixed while replacing only the reward, then report the obligation denominator, hidden-probe policy, and artifact-audit failures. Finally, interpret the rates cautiously: the paper reports one greedy episode per instance, selects the checkpoint by held-out verified rate, and notes that held-out splits contain only 58–129 instances. The result is a concrete recipe for testing dense verifier feedback—not a general guarantee of correct software.

The paper starts from a specific evaluator failure: existing evaluators can mistake refusals or topically related responses for successful attacks, and changing only the judge LLM altered reported ASR by up to 82 percentage points. This is a narrower contribution than a first substantive-fulfillment evaluator: FJAR had already used query-specific anchored references and staged judgments to assess fulfillment. The distinct change here is to make response-only reconstruction rather than a query-specific anchored reference the central test.

Given only a response, the first LLM reconstructs a concise request represented by substantive content, excluding repeated, named, or refused material. A second LLM generates five semantically close decoys that differ in requested action, information, outcome, or direction. The judge receives the original request and randomized reconstruction–decoy pairs, selects a matching candidate or abstains when neither matches; abstentions count against the reconstruction, and a majority of reconstruction wins yields a jailbreak label. Thus the operational signal is semantic recoverability, not a direct harmfulness judgment. The paper’s analysis makes its central assumption explicit: fulfilling responses should usually make the request recoverable, while non-fulfillment should usually leave it unrecoverable.

On both human-labeled benchmarks, the game has the lowest mean MAE among evaluated methods. With three off-the-shelf judges and the stated benchmark conditions, mean MAE is 0.147 versus 0.181 for vanilla judging on StrongREJECT and 0.224 versus 0.389 on HarmBench. Across five tested attacks against Qwen2-7B-Instruct, the game has the smallest ASR spread among LLM-based classifiers, but the spread remains 12–28 percentage points; for I-GCG, vanilla-judge ASR ranges from 6% to 88% while game ASR ranges from 36% to 48%. This comparison is qualified because each attack run used its evaluator as the in-loop judge, so the judge also influenced attack generation.

The conservative tradeoff is visible in SorryBENCH: the game’s mean MAE is 0.000, 0.012, and 0.011 for refusal, specific-refusal, and refusal-with-safe-alternative categories, but 0.519 and 0.425 for incomplete and substantive successful responses. That pattern is consistent with the paper’s estimated fulfillment–recoverability gap: incomplete responses can fulfill a request without exposing enough content for reconstruction. For a replication, the concrete question is whether changing the number of decoys shifts recall and false positives; the paper uses five decoys but does not ablate their number. Transfer remains uncertain: the experiments use small 8–12B judge models and small attack targets, do not cover chain-of-thought traces, multi-turn jailbreaks, or multi-agent interactions, and do not establish robustness against attacks optimized for the evaluator’s verdicts. The practical takeaway is to report recoverability and fulfillment as separate quantities rather than treating the game’s label as ground truth.

Best-of-N is not only a question of whether sampling has produced a correct candidate. This paper treats selection as a race between the largest reward among correct candidates and the largest reward among incorrect candidates: success requires the former to win. Its extreme-value analysis separates correct-tail-dominant, incorrect-tail-dominant, and critical regimes, providing an account of both improving and degrading scaling.

Earlier work in the supplied comparison already studies inference-time proxy-reward hacking and proposes HedgeTune, whose principled calibration requires true-reward feedback. The practical change here is to diagnose selection risk from unlabeled, per-query reward scores rather than from true-reward feedback. Specifically, the authors fit a two-component Gaussian mixture, use the high-mean component as a proxy for correct responses and the low-mean component as a proxy for incorrect responses, estimate a leading-order crossover budget, and stop after that point when the lower-mean component has higher variance.

The decisive condition appears in the Gaussian analysis. Even when correct responses have a higher mean score, sufficiently larger variance for incorrect responses makes their upper tail eventually dominate as the sampling budget grows; the paper interprets this non-monotonic case as reward hacking. This gives a sharper diagnostic than average score separation: measure which class is more competitive at the maximum, not merely which class has the better mean.

The reported evidence is consistent with that mechanism but remains conditional. In the real-score statistics, correct responses generally have higher means while incorrect responses often have higher variance, with exceptions. For early stopping, Appendix B.2 reports one concrete setting in which, at planned n=8192, Skywork Qwen3-1.7B reduces computation by 27.6% and raises hack-subset accuracy from 0.0366 without stopping to 0.0792 with stopping. The paper also notes that stopping can be suboptimal when accuracy improves monotonically.

Do not treat the rule as a universal verifier controller. The framework targets verifiable problems, and the heuristic is not established for non-bimodal or far-from-Gaussian scores, cases where incorrect answers have higher average rewards, or reliable finite-budget regime identification. A useful research operation is to fit the mixture on a new verifier, estimate its crossover, and then test accuracy and cost on both sides of that budget while checking whether the mixture components actually align with correctness.

One-step prediction loss is an attractive checkpoint metric, but its target is the model’s own embedding rather than an interpretable physical quantity. It can therefore mix errors already present in the encoder’s representation with errors added by the dynamics predictor. This paper turns that limitation into a measurement experiment: does deliberately improving one-step fidelity also improve goal-conditioned planning?

The proposed protocol fits a decoder from encoder embeddings of real observations to simulator state, freezes it, and evaluates both the decoded real next state and the decoded predicted latent on separate test episodes. Errors are normalized in physical units. The report separates representation error, prediction error, and excess error—the latter intended to identify the predictor’s added error when the encoder/decoder contribution dominates. The authors also repeat the analysis with latent drift, a decoder-free measure. They move fidelity through warm-started fine-tuning checkpoints and evaluate planning with three training seeds and paired planning seeds.

The clearest evidence comes from the PushT checkpoint ladder. The first epoch improved fidelity by 32.0% and planning by 4.44 percentage points. After that, fidelity continued improving monotonically across the 15 later checkpoints, but the correlation between one-step error and planning success was approximately zero (r = -0.010). This was not explained by a task ceiling: planning in the lowest-support data stratum began at 80%, leaving headroom, yet remained flat from epoch 1 onward as fidelity improved. Across environments, the numerical exchange was also unstable: a 93% prediction-error reduction in TwoRoom corresponded to -0.7 percentage points of planning, while a 40% reduction in PushT corresponded to +4.9 points. These percentages are illustrative rather than directly comparable across tasks.

A matched continued-training control also absorbed the fidelity improvement attributed to an auxiliary state-grounding objective; the measured arm effects were not distinguishable. The practical operation is therefore to treat one-step loss as a diagnostic, not a deployment proxy: freeze a task-relevant decoder, separate representation from predictor error, and evaluate matched checkpoints on the actual planning objective.

The boundary is substantial. The study evaluates one 15M-parameter architecture, three low-dimensional simulated environments, one planner, and warm-started fine-tunes from one checkpoint family. Its central within-task result covers a limited post-epoch-1 fidelity range, and the authors note that three training seeds make small effects difficult to resolve. The result is a checkpoint-selection caution for this tested setting, not a general claim about all world models.

The limitation

The paper targets a concrete validation limitation: repair agents often validate a patch against the same evidence used to construct it—such as a static alert, sanitizer trace, published exploit, or test suite. Blocking that evidence can therefore leave a variation of the same vulnerability exploitable.

The method change

P2Patch changes the loop from one-shot validation to adaptive attack-and-repair. Starting from a normalized vulnerability finding, an exploitation agent constructs a reproducing proof of vulnerability (PoV), a patching agent repairs the program, and the exploiter attacks the patched program for a distinct same-vulnerability exploit. Every execution-confirmed bypass becomes a permanent repair requirement, while construction-time PoVs remain separate from held-out evaluation oracles.

The accompanying VulnRepairBench contains 101 CVEs across 60 Java and 41 C/C++ subjects, 61 repositories, and 20 weakness classes. Its held-out design separates attack paths blocked by the official fix from candidate paths that remain reproducible after that fix.

Decisive evidence

In the main configuration, the adversarial stage found at least one confirmed bypass in 41% of runs after the patch had already blocked its bootstrap PoV. Against single-pass repair from the same finding using Claude Code, P2Patch raised fix-closed coverage from 78.1% to 84.7% and beyond-upstream coverage from 42.1% to 62.5% under the benchmark’s scoring policy. The reported ablation attributes detectable coverage gains to adversarial hardening rather than the bootstrap PoV alone. This improvement came with a mean per-subject cost of $2.09, compared with $0.45 for single-pass repair.

What to reuse—and what not to conclude

A transferable research operation is to treat each execution-confirmed counterexample as a new acceptance requirement, accumulate those requirements during repair, and reserve an independent suite for final scoring. This makes the evaluation question operational: does the system improve on attack paths it did not use while repairing?

The result remains bounded testing evidence, not proof of patch completeness. The held-out suites are curated and incomplete; the paper reports that later upstream fixes corroborated 14 residual cases, while closure on later trees was verified for only 8. Semantic distinctness beyond rejecting duplicate commands was not machine-checked, so the authors qualify the 41% bypass rate as an upper bound on genuinely distinct paths.