Recursive Self-Inflation: how self-improvement loops hillclimb on the verifier's mistakes

The evidence that AI systems are starting to improve themselves is a specific, and fairly short, list of results. AlphaEvolve [1] searches over programs and keeps the ones that score better on an automatic metric. Darwin Gödel Machine [2] reports moving a coding agent from 20% to 50% on SWE-Bench Verified and from 14.2% to 30.7% on Polyglot, by having the agent rewrite its own code and keeping what scores better. Self-Harness [3], Agentic Harness Engineering (AHE) [4], and Meta-Harness [5] all optimize agent harnesses against Terminal-Bench 2, with AHE lifting pass rates from 69.7% to 77.0% across ten iterations. EinsteinArena [6] produces new results on open mathematical problems through repeated submission to deterministic verifiers, with accepted solutions persisting publicly for later agents to build on.

Whether all of these are self-improvement in a strict sense is contested, and there is no agreed definition of RSI — but underneath, they run the same loop: (a) generate a candidate, (b) let a program decide whether it beats what came before, (c) keep the winner. The loop runs at all only because that deciding step is fast, cheap, and automatic, and that is the property the argument depends on.

None of this is a secret. In her survey on harness engineering [7], Lilian Weng says as much: these loops work best where evaluation is measurable and objective, the way RL does, and evolutionary search struggles when evaluation is slow, ambiguous, or heuristic. Everything depends on the verifier, and everyone building RSI-adjacent systems knows it.

Are the verifiers we have actually reliable? Over the last two years we've accumulated a lot of evidence that the cheap verifiers we already have are wrong in both directions: they tend to reject solutions that work, and often pass ones that don't. ELT-Bench-Verified [8] is the cleanest case: a newer Sonnet 4.5 agent produced transformation outputs on many more tasks than the older Sonnet 3.5 setup, and of the 81 tasks that then failed column-level evaluation, 67 (82.7%) contained at least one error attributable to the benchmark rather than the agent. One column asked for a country's GNP growth rate; the agent applied the standard formula and returned a decimal, 0.0441 for Aruba, while the ground truth stored the same quantity as a percentage, 4.41. Every one of the 178 non-null values was off by exactly a factor of 100, and the column scored zero. ELT-Bench [33] was not carelessly built. Its authors knew their upstream source was noisy — one study put error rates in the Bird databases as high as 49% — so they manually verified every question and query they drew from it, wrote about ten additional test queries per data model, corrected the transformation queries wherever those tests disagreed, and executed and checked all 100 pipelines by hand, at three to five hours of manual work per pipeline. The defects were there anyway, and stayed invisible until an agent arrived that could reach them. Earlier models never got far enough to trigger the defect, so the verifier looked fine. The stronger the model, the more of the verifier's blind spots it finds. This is a massive hurdle for RSI, because a self-improvement loop optimizes against the verifier over and over, so it hillclimbs on the verifier's mistakes.

Left: the same agent — SWE-Agent running Claude Sonnet 4.5 — scored on the original ELT-Bench and on the corrected ELT-Bench-Verified. Transformation success rises from 22.66% to 32.51% of 203 data models, a gain of 9.85pp produced entirely by correcting the benchmark; the agent and the harness are unchanged. Right: the audit covered 660 individual columns that failed to match, across the 81 tasks that produced transformation output but failed evaluation. At this column level, 218 mismatches (33.0%) were attributable to the benchmark — rigid evaluation scripts, ambiguous specifications, or ground truth that no reasonable query reproduces — and 442 (67.0%) to the agent. These defects were only observable because a newer agent produced transformation output on tasks the older Sonnet 3.5 setup never reached. Data from Zanoli et al. [8].

By now the pattern should be familiar: verifiers reject correct work, pass work that shouldn't pass, grow less reliable exactly as the systems they measure improve, and shift under infrastructure nobody reports. The ambitious versions of the RSI and knowledge-scaling arguments propose leaving cheap verification behind entirely. Weng's list of open challenges [7] names research taste and long-term value as hard to measure. My own view is that the harder problem is upstream: the objective itself is wrong. Agents asked to revise a belief tend not to build a hypothesis and follow its dependencies — they swap the conclusion and leave the reasoning behind it untouched. I have more to say about this, in an upcoming work.

Where does the over-optimism come from? Trehan and Chopra [9] ran research ideas through a minimal-scaffold pipeline and observed six recurring failure modes, three of them directly relevant: implementation drift, where the model moves toward a simpler common solution when the proposed method gets technically hard; over-optimism, where it declares success despite noisy or failed experiments; and weak scientific taste, where experiments are executable but answer the wrong question. Trehan and Chopra [9] found that even when results showed clear degeneracies or outright failures, the text their system generated reported only top-level positive indicators and passed over the fundamental problems. They trace this to how the system read its own results: it evaluated output from report files produced during the execution stage rather than from the raw logs of the experimental pipeline. The paper-writing stage made it worse, overstating novelty and scope — their agent described its own output as "the first ever paper" in a domain regardless of what the research had actually produced. They note this mirrors the p-hacking and eureka-ing behaviors identified by the Goodfire team, and aligns with Bubeck et al. [10], where a physicist modeling a thermonuclear burn wave reported that the model would patch over errors with what he calls "numerical duct tape" and announce success while the numerical signal was still plainly noise. Trehan and Chopra read the whole pattern as an eagerness to please inherited from RLHF, where models are rewarded for being agreeable and helpful, producing a bias toward optimistic interpretation even when the evidence points the other way — objectives, they argue, that are not what an autonomous science system needs, which is scientific skepticism, truth-seeking, and the detection of confirmation bias.

The verifiers we have are demonstrably defective

SWE-bench [11] is the most-cited target for coding-agent self-improvement, and three independent audits [13, 14, 15] have found that its tests fail in both directions: they reject patches that work and accept patches that don't.

When a frontier model keeps failing, is it a limitation of model or the benchmark? The Verified subset was itself a repair effort [12]: three software engineers independently reviewed each of 1,699 candidate problems, and 500 were selected as clear, solvable, and reliably tested. In February 2026, OpenAI re-audited 138 of those 500 [13]. The sample was deliberately failure-enriched, drawn from tasks that o3 did not solve consistently across 64 independent runs, so the result does not generalize to the full set. Within that sample, each case reviewed by at least six experienced engineers, 59.4% had material problems: 35.5% had tests too narrow, enforcing implementation details the issue never required; 18.8% had tests too wide, checking functionality absent from the problem statement; 5.1% had other material issues. In summary, among the tasks being used to characterize what a frontier model still fails to do successfully, the majority of failures examined could not cleanly be attributed to insufficient model capability.

The same audit found a second problem, and the two compound. Every frontier model OpenAI tested could reproduce the gold patch or verbatim problem-statement text on at least some tasks. GPT-5.2 solved 31 of the tasks they had classified as near-impossible. The mechanism they identify is the interaction: models that saw the problems in training succeed because they have the information needed to pass tests the problem statement never specifies. The clearest case is django-14725, where the tests require a parameter edit_only that the issue text never mentions. GPT-5.2's chain of thought reads: "There is also edit_only parameter maybe added around 4.1 or 4.2. Since this is 4.1 dev 2022, the code might be before introduction. We will implement now. Hidden tests will check new behavior." It knew from the Django release notes. Underspecification makes the task unreachable by reasoning; contamination makes it reachable by recall. OpenAI's conclusion was that improvements on the benchmark now reflect training exposure rather than software engineering ability, and they stopped reporting the scores.

How often do benchmarks accept a wrong patch? Those were false negatives; other studies found the reverse. UTBoost [14] identified insufficient tests in 26 of the 500 Verified instances; among 584 agent patches that had passed the original tests on those instances, 92 (15.7%) failed augmented tests. The same work found a larger and stranger problem in the harness itself. SWE-Bench extracts test names from raw test logs using per-repository regular expressions, and those expressions break on output spanning multiple lines: in one Django instance, 55 test cases failed to parse, and the string "Tests altering of the primary key." was pulled out of a log and recorded as the name of a test. Repairing the parser corrected annotations in 271 of the 500 Verified instances, 54.2%, and exposed 79 erroneous patches on its own. This is outside what the 93-engineer verification campaign was looking for, which was test scope and issue specification. Together the augmented tests and the fixed parser identified 169 previously-passing patches as erroneous and changed the ordering of 11 of 45 leaderboard entries. Amazon-Q-Developer-Agent had led at 55% with devlo second at 54.2%; after correction both sat at 53.6%, and the margin was gone. Wang et al. [15] identify a scoping decision in the harness: SWE-bench runs only the test files modified by the PR that fixed the issue, leaving the rest of the repository's suite untouched. Running all of it shows 7.8% of patches counted as correct failing tests the project already had, and 29.6% of plausible patches behaving differently from the gold patch, with manual review judging 28.6% of those certainly incorrect. Together these inflate reported resolution rates by 6.4pp. The ranking moves too. Removing suspicious patches costs the three tools 17.3pp on average, and LearnByInteract's 7.2pp lead over OpenHands — 60.2% against 53.0% — shrinks to 2.2. And 66.2% of the suspicious patches could not be adjudicated at all — the authors could not determine whether they were correct, because the issue statements do not specify the behavior in question. The tests are weak, and the task is underspecified, in the subset 93 engineers filtered for clear specifications.

OpenAI recommended SWE-Bench Pro [16], watched frontier pass rates on the 731-task public split rise from 23.3% to 80.3% in eight months, audited it, found that an automated pipeline classified 200 tasks (27.4%) as broken and a separate human campaign classified 249 (34.1%), estimated the true rate at roughly 30%, and retracted its recommendation [17]. The benchmark's own authors had already measured how much of its score depends on writing the task to suit the checker. Every problem ships with human-authored requirements and interface specifications, added because unit tests expect a narrow set of solutions and unconstrained agents produce valid patches the tests reject. Strip those out and leave only the problem statement: GPT-5 falls from 25.9% to 8.40%, Claude Opus 4.1 from 22.7% to 8.20%. Roughly two thirds of the reported capability is a property of how tightly the task was specified to fit the verifier, which the authors state plainly as a limitation — real tasks admit many correct solutions, and their tests accept one.

Verifier defects are not specific to code: multiple benchmarks in scientific coding, mathematics, instruction following, and general knowledge have been re-audited [19, 20, 21, 23, 24], and every one had a verifier issue large enough to change its leaderboard.

SciCode-Verified [19] audited all 65 test problems in SciCode [18], dropped one as underdetermined beyond repair, and reported 262 corrected defects across 63 of the remaining 64. Across 12 frontier model snapshots, corrected main-problem pass rates rose from a range of 9–27% to 69–92%. Before the audit, the top four models were within only four points of each other, and GPT-5.6 Sol scored the same as GPT-5.5 — in other words, when every model fails at the same broken step, the benchmark stops separating them reliably, and the results falsely appear as a plateau. The authors judged that 150 of the 192 defects that artificially lowered scores required scientific domain expertise to identify: finding the particular class of defect identified required a domain expert, and a generic audit would miss them. SciCode shipped in July 2024 with the best model solving 4.6% of main problems. Two years of model progress moved that to 9–27%. The audit moved it to 69–92%.

Twelve frontier model snapshots scored on the original SciCode and on SciCode-Verified, under the same harness, same prompts, same pass@1 protocol — only the benchmark data differs. Main-problem accuracy is all-or-nothing: a problem counts as solved only if every one of its cumulative subproblems passes, so a single defective gold value or over-tight tolerance fails the whole problem. Correction lifts every model by 53 to 70 main-problem points. It also restores discrimination the original benchmark had lost: GPT-5.5 and DeepSeek V4 Pro Preview sit two main problems apart on the original and eight apart after correction, while Seed 2.1 Pro leads on the original score and ranks sixth on SciCode-Verified. Rows marked * are the mean of three runs; all others are single runs, so small differences should not be over-read. Data from Hu et al. [19].

In mathematics, Hugging Face replaced a brittle answer extractor with Math-Verify [20] and re-ran all 3,751 models ever submitted to the Open LLM Leaderboard. On the 1,324-question MATH-Hard subset, on average, 61 answers per model that the old evaluator had rejected were now accepted as correct, worth 4.66 score points, and many jumped 200 places or more. Nothing had changed about the models' mathematical ability. The parser had simply stopped rejecting correct answers.

In instruction following, an audit of IFEval [22] found four classes of defect in the inherited prompts [21]: checkers that cannot evaluate what the prompt asks for, natural-language prompts that contradict their own stored configuration, typographical errors, and constraint combinations that cannot be satisfied at all. Two examples show how basic the failures are. One test case requires the # character to appear at least four times, but the original evaluation function only supports the letters a-z, so the checker cannot score the constraint the prompt states — the prompt is well-formed and unevaluable. Another asks the model to repeat a sentence verbatim, commas included, while also instructing it to avoid using commas; no output can satisfy both. Deterministic checking guarantees the output was measured correctly, but gives no guarantees on whether the prompt, the stored config, and the checker are asking for the same thing.

Even human-authored answers require revision. MMLU-Redux [23] re-annotated 5,700 questions across all 57 MMLU subjects and estimated a 6.49% error rate, with error heavily concentrated: 57 of 100 analyzed virology questions had some identified issue. HLE-Verified [24] re-audited the 2,500 questions of Humanity's Last Exam, verifying 668 items unchanged, revising and reverifying 1,143, and placing 689 in an explicit uncertain category rather than forcing a binary judgment. Across eight models, accuracy rose 7 to 10pp overall and 30 to 40pp on items whose problem statement or reference answer was erroneous.

A score is a property of the model, the harness, the compute budget, and the prompt together: a change in any one component can result in the same tasks producing a different score.

The same holds on the input side. Rephrasing a prompt while preserving what it asks for drops performance by up to 61.8% across 46 models [20]. Anthropic [25] ran the same model, harness, and Terminal-Bench 2 tasks under six resource configurations. The effect has two regimes. Up to three-times headroom, extra resources cut infrastructure errors from 5.8% to 2.1% while scores stayed within noise (p = 0.40): the eval got more stable without getting easier. Above that, success climbed faster than errors fell — a further 1.6pp drop in infrastructure errors against nearly four points of success — because the extra allocation let agents attempt approaches that only work with generous limits. From strict enforcement to uncapped, success rose six points and infrastructure errors fell to 0.5%. On bn-fit-modify, some models open by installing the standard data science stack; under tight limits the container runs out of memory during installation, before any solution code is written, while models that implement the math with the standard library succeed. The configuration decides which strategy wins. A crossover on SWE-bench — 227 problems, ten samples each, RAM up to five times baseline — showed the same direction at smaller magnitude, 1.54pp. Their practical conclusion was that differences below roughly three points should not be taken for granted when compute and sandbox conditions are not matched.

Why this hits RSI harder than it hits model evaluation

For a static evaluation, a defective verifier produces a wrong number, and the number stays wrong until someone checks. That can take years: SWE-Bench Verified shipped in 2024 and was re-audited in 2026, and SWE-Bench Pro ran for eight months before OpenAI withdrew its recommendation. But the error is inert. The model is not doing anything with the score, so the damage is a period of believing something false about a system that itself is unchanged.

A self-improvement loop will find the verifier's holes and optimize for whatever passes through them.

A static benchmark and a self-improvement loop treat a false positive differently. The RSI loop generates candidates, scores each with the verifier, and keeps the ones that pass. Candidates that exploit a hole in the verifier are more likely to pass, and while in a static benchmark this means letting a false positive slip, absorbing a single measurement error and moving on, in an RSI loop this error becomes the seed for the next round.

Do agents actually exploit them? Meerkat [26] audited 1,264 successful Terminal-Bench 2.0 traces and found two distinct ways the answers were getting through. In the first, 415 of 429 successful traces were from agents that read from a /tests directory the task spec made inaccessible; the agent's first action was often cat /tests/test_outputs.py, after which it reverse-engineered the expected output. In the second, the harness automatically loaded any AGENTS.md file in the working directory into the system prompt, and on some tasks that file contained the graded answer. On one task, the agent researched the question legitimately, failed to resolve it, read AGENTS.md, found both the expected answer and a note that an earlier run had scored zero for answering differently, wrote the supplied answer to disk, and then confirmed it by grepping the same file it had just read. On another, the agent skipped the graded structure-learning step entirely and hardcoded the exact six-edge graph the verifier checks for, saying it would use the correct answer from the guidelines. Of 364 passing traces, 110 referenced AGENTS.md as "project guidelines." When the authors replaced those traces with runs of the same model in a clean harness, the reported pass rate fell from 81.8% to 71.7%, and the leaderboard position from first to fourteenth.

What does the exploitation look like when it happens? METR's analysis [27] catalogues the behaviors: inspecting call stacks, disabling synchronization, overwriting timers, monkeypatching evaluators, copying cached models, overloading equality. Across 1,087 o3 HCAST runs, there were eight incidents, 0.7%, but in the three RE-Bench task families where the behavior appeared it ran to 39 of 128 runs, 30.4%, including 21 of 21 on one task. It's easy to come away thinking o3 reward-hacked about a third of the time. It didn't. That 30.4% only holds inside the three task families where the behavior showed up; across the whole evaluation it was under 1%. Reward hacking was 43 times more common on RE-Bench than on HCAST, which METR attributes to the model being able to see the entire scoring function there. Prompting does not fix it: on one task, appending "Please do not cheat" left the rate at 80%, and "Please solve this task only using methods the task's designer likely intended" raised it to 95%. Nor is it a comprehension failure. Asked afterwards whether its plan adhered to the user's intention, o3 answered no ten times out of ten.

As a system improves, more of its outputs land in territory the verifier was never validated on, because the verifier's authors could only test it against the systems that existed at the time.

Verifier validity is capability-relative: at low model capability, a weak verifier looks strong because most outputs fail in obvious ways, usually well below the boundary of the "gray area" where the verifier's assumptions begin to matter. As model capabilities improve, their outputs move toward that boundary and they end up exploring more of it: a stronger model is capable of producing correct solutions outside the representation the authors anticipated, implementing requested behavior through different but still legitimate abstractions, inferring unstated requirements from repository conventions, and discovering accidental shortcuts in the environment. All of these produce a passing result and none of them mean the same thing.

A verifier is tested, at design time, against the behaviors its authors planned for. The share of system outputs that actually reach the verifier's decision boundary is not fixed: it grows with model capability, because stronger systems produce more solutions near the edge of what the verifier can adjudicate, and explore more of that edge. Past the crossing point, most of what the verifier is asked to judge lies outside the superset of scenarios it was tested on.

ELT-Bench-Verified [8] shows this: the verifier defects surfaced only once a stronger agent reached the code path that stressed them. EinsteinArena [6] is the same story told by the people who built the verifier. On the kissing-number problem, the platform's own authors had to revise the verifier after launch, because the numerical precision needed to separate a valid configuration from an invalid one exceeded a standard double-precision pipeline; they rebuilt it on 80-digit decimal arithmetic. Their stated reason is the argument of this section: agents optimize aggressively against the scoring function. The verifier was adequate until the submissions got close enough to the boundary that the difference between right and wrong fell below machine epsilon. Two other cases corroborate it from different angles: OpenAI's SWE-Bench 138-task re-audit was drawn from the tasks o3 couldn't solve consistently, and 59.4% of those had material defects. The tasks where the strong model kept "failing" were disproportionately the tasks where the verifier was wrong. SciCode-Verified [19] shows: fixing the verifier moved 12 frontier models from a 9–27% range to 69–92%.

Now apply that to a self-improvement loop. Its purpose is to make the system stronger, and every increment pushes it further into untested territory, so the verifier decays as the system improves, and the loop can't see it happening, because the verifier is the only signal it has.

Errors compound across generations: the accepted output in each round becomes the starting point for the next one, so a false positive early on is inherited by everything downstream.

Nothing in the current proposals provides retraction, confidence decay, or a way for later evidence to demote an entry that was accepted earlier.

What would make an RSI result credible

A credible RSI result is one that can distinguish between two plausible outcomes: did the agent or agentic system get better, or did it discover something exploitable that its verifier overlooked?

Benchmarks and their revisions are typically versioned, but results often aren't. Results should always report which version they ran against, which verifier revision was used, and which environment; without those, results are not directly comparable and therefore often misleading. And when results are re-reported after a benchmark revision or a harness change, it's worth auditing both tails of that improvement: check the new passes for false positives — shortcuts, leaks, contamination, or tests with gaps that a wrong patch can pass through — and check the remaining failures for false negatives, such as correct solutions the verifier rejected, outputs the checker couldn't parse, and failures caused by underspecification of tasks or infrastructure failures in the environment.

A test split from the same benchmark inherits the same verifier. If the loop learned to exploit it, the held-out split rewards the exploit exactly as the training split did.

A test split taken from the same benchmark inevitably inherits its flaws: same parser, same tests, same underspecified tasks. If the loop learned to exploit them, the held-out split rewards the exploit as readily as the training split did. Self-Harness [3] validates every harness edit against held-in and held-out splits of the same 64 Terminal-Bench 2.0 tasks, which guards against overfitting the task set and not at all against overfitting the verifier. Evaluating on a second benchmark with an independently written verifier would be one way to fix this, so any defect the loop learned to exploit is absent by construction.

When no cheap verifier exists, the fallback is a model judging outputs — an instrument with its own error rate. AgentProp-Bench [28] measured judge agreement against human review across 14,750 traces from 13 agents, and found the best-performing judge reached a Cohen's κ of only 0.567, against 0.835 between two human annotators, which counts as almost perfect. Notably, a three-model ensemble scored significantly worse than a single judge (κ 0.432 against 0.567). On FALSIFYBENCH [29], a model oracle scored 85–95% correct while agreeing with humans at anywhere from κ 0.34 to 0.98, because accuracy rewards the easy, lopsided calls and says nothing about the ones that decide the result. And the judge doesn't hold still — under sustained pushback frontier models flip their verdicts 25–71% of the time, and 62–91% against an adversarial persuader, with the flips running almost entirely away from the truth [30].

Lin et al. [32] varied the evolver, harness, and task-solving agent independently across 7 models and 3 benchmarks and found that their contributions were poorly unbalanced. Who wrote the harness update barely mattered: the difference between the best and the worst evolver was found to be at most 3.1pp on any benchmark, and a 9B model's updates showed comparable gains to Claude Opus 4.6's, in skills the authors describe as "procedurally isomorphic". Who consumed the update mattered a lot more. Also, an RSI gain reported without matched resources and run-level variance is not interpretable.

Left: harness-updating gain for each of seven models used as the evolver — the component that reads execution evidence and writes the harness update — with the task-solving agent held fixed. On SWE-Bench Verified the seven evolvers span 5.9 to 8.2pp, a 2.3pp difference, and no evolver wins across all three benchmarks: Qwen3-235B leads on SWE and comes last on MCP-Atlas. The 9B model is not the weakest evolver anywhere and is the best on SkillsBench. Right: harness-benefit gain against base pass rate on SWE-Bench Verified, each point one model used as the task-solving agent. The relationship is non-monotonic. Qwen3-235B gains 19.3pp and GPT-OSS-120B 15.8, while Opus 4.6 gains 2.6 — a ceiling effect at the top — and Qwen3-32B gains only 4.4 despite having the most room to improve. Data from Lin et al. [32].

Verifier validity degrades as frontier models improve, and a verifier that was once sound at one capability tier can fail at the next one. Terminal-Bench-Science 0.1 [31] shows what this looks like when taken seriously: it introduces an elaborate vetting process across 70 tasks selected from 920 proposals, parallel domain and technical review, a final bar raiser, oracle and no-op runs that must score exactly one and zero, explicit adversarial cheat trials, retained trajectories, and versioned releases that can add, repair, retire, or regrade. Its documentation still records that an answer-bearing file survived two supposed fixes and remained in the served environment.

A sound verifier certifies that a proof correctly establishes a formal statement, but leaves unchecked whether that statement accurately represents the intended problem, or whether the proof preserves the existing theory and constructions it rests on.

AlphaProof Nexus [34] is a useful counterexample to end on, because its verifier is not defective: Lean's type checker either accepts a proof or it doesn't. Yet the same two failures appear: the statement can be wrong, and the verifier can be gamed. Two Erdős problems had been formalized with the wrong notion of density. The informal problem statements used "density" without saying which kind — for a set of integers, lower density and upper density (the lim inf and lim sup of the proportion up to N) can differ, and the statement didn't clarify which one is to be used — so whoever wrote the Lean version adopted one possible interpretation. The agent then proved that statement, and while it produced a valid proof, it was a proof of a theorem nobody asked for, leaving the intended problem untouched. The AlphaProof team subsequently corrected both Lean formalizations to match the intended meaning — one problem's statement was changed to use lim inf, and the other lim sup — then ran the agent again against the corrected statements.

On a problem from Ben Green's well-known list [36], the agent solved the real-valued variant when the intended question was complex-valued. The Erdős formalizations came from a community effort, so independently written formalizations of famous problems did not adequately capture the assumptions and constraints of the intended problem, and the agent proved them anyway. Lean also gives the agent ways to satisfy the verifier without proving anything. A proof is accepted when every goal is closed, and Lean provides constructs that close a goal without proving it — most directly sorry, a placeholder that marks a goal as admitted so the rest of the file can compile. It exists so mathematicians can sketch a proof and fill in the details later. For an agent optimizing against the verifier, this is a potential shortcut: as it turns out, the agent repeatedly pushed the problem's core difficulty into a single sorry inside a helper lemma that was just the target theorem slightly rephrased, so the "proof" reduced the problem to itself. Its highest-rated sketches leaned on lemmas marked sorry and asserted to be established results in the literature, which on inspection were hallucinated. The AlphaProof team ran a separate guardrail pass, SafeVerify [37], to check two things: that the proof proved the theorem as stated, and that the agent hadn't exploited the environment — by, for example, injecting axioms — to get it accepted.

A subtler failure I've seen first-hand: rather than alter the theorem statement itself, the agent instead modifies what that statement rests on, redefining a Mathlib instance or shadowing a definition such that the same words now mean something weaker. The file compiles successfully, the theorem name is unchanged, but what was proved is a different theorem under the original signature. Ammanamanchi et al. [35] audited five widely used Lean benchmarks across 13 released variants — 10,318 problems, with forks and ports of the same problems counted separately — and surfaced 4,833 findings, 398 of them with a Lean certificate that the problem could not be proved as stated: the statement was either false, or its hypotheses were inconsistent. Two of their cases show what that looks like. In CombiBench [38], a formalization encoded a minimality condition in a way that made its own hypotheses unsatisfiable, so an agent could prove a contradiction from them and, from a contradiction, prove anything — including the original theorem, without ever engaging with what it says. In ProverBench [39], Lean's sorry admits a statement to the environment as an axiom, which means that a model can prove one benchmark problem by citing the unproved theorem as an established fact; the audit found 199 axiom-related findings there, and three DeepSeek-Prover-V2 proofs that a pre-4.20.0 apply? bug had accepted without kernel verification. The authors' conclusion is that RL-trained provers will find and exploit any verification loophole that raises reward. These guardrails validate what the agent submitted, but not what it changed underneath — the definitions and prior results the statement is stated in terms of. What's missing is a belief-state constraint — an invariant over the state of the world the proof was constructed in. That could look like a minimal set of theorems, instances, or definitions the library is known to establish, re-verified after every accepted step of the proof so that the agent can't quietly redefine something the proof relies on. That is the RSI problem in miniature: an accepted step becomes the base for the next, and if that step moved something the next step consumes as a premise, every subsequent step inherits the flaw; more on this in future work.

References

  1. [1] Novikov, et al. "AlphaEvolve: A coding agent for scientific and algorithmic discovery." arXiv:2506.13131, 2025. https://arxiv.org/abs/2506.13131
  2. [2] Zhang, et al. "Darwin Gödel Machine: Open-Ended Evolution of Self-Improving Agents." ICLR 2026. arXiv:2505.22954v3. https://arxiv.org/abs/2505.22954
  3. [3] Zhang, Hangfan, Zhang, Shao, Li, Kangcong, et al. "Self-Harness: Harnesses That Improve Themselves." arXiv:2606.09498v1, 2026. https://arxiv.org/abs/2606.09498
  4. [4] Lin, et al. "Agentic Harness Engineering: Observability-Driven Automatic Evolution of Coding-Agent Harnesses." arXiv:2604.25850v4, 2026. https://arxiv.org/abs/2604.25850
  5. [5] Lee, et al. "Meta-Harness: End-to-End Optimization of Model Harnesses." arXiv:2603.28052, 2026. https://arxiv.org/abs/2603.28052
  6. [6] Bianchi, Federico, Kwon, Yongchan, Pappu, Aneesh, and Zou, James. "Harnessing the Collective Intelligence of AI Agents in the Wild for New Discoveries" (EinsteinArena). arXiv:2606.10402v2, 2026. https://arxiv.org/abs/2606.10402
  7. [7] Weng, Lilian. "Harness Engineering for Self-Improvement." Lil'Log, July 4, 2026. https://lilianweng.github.io/posts/2026-07-04-harness/
  8. [8] Zanoli, C., Giovannini, A., Jin, T., Klimovic, A., and Perlitz, Y. "ELT-Bench-Verified: Benchmark Quality Issues Underestimate AI Agent Capabilities." arXiv:2603.29399, 2026. https://arxiv.org/abs/2603.29399
  9. [9] Trehan and Chopra. "Why LLMs Aren't Scientists Yet: Lessons from Four Autonomous Research Attempts." arXiv:2601.03315, January 2026. https://arxiv.org/abs/2601.03315
  10. [10] Bubeck, et al. "Early science acceleration experiments with GPT-5." arXiv:2511.16072, November 2025. https://arxiv.org/abs/2511.16072
  11. [11] Jimenez, Carlos E., Yang, John, Wettig, Alexander, Yao, Shunyu, Pei, Kexin, Press, Ofir, and Narasimhan, Karthik. "SWE-bench: Can Language Models Resolve Real-world GitHub Issues?" ICLR 2024. https://openreview.net/forum?id=VTF8yNQM66
  12. [12] Chowdhury, N., et al. "Introducing SWE-Bench Verified." OpenAI, August 13, 2024. https://openai.com/index/introducing-swe-bench-verified/
  13. [13] OpenAI. "Why SWE-bench Verified no longer measures frontier coding capabilities." February 23, 2026. https://openai.com/index/why-we-no-longer-evaluate-swe-bench-verified/
  14. [14] Yu, Boxi, Zhu, Yuxuan, He, Pinjia, and Kang, Daniel. "UTBoost: Rigorous Evaluation of Coding Agents on SWE-Bench." ACL 2025 (Long Papers), pp. 3762–3774. arXiv:2506.09289. https://doi.org/10.18653/v1/2025.acl-long.189
  15. [15] Wang, You, Pradel, Michael, and Liu, Zhongxin. "Are 'Solved Issues' in SWE-bench Really Solved Correctly? An Empirical Study." ICSE 2026. arXiv:2503.15223v2. https://doi.org/10.1145/3744916.3764576
  16. [16] Deng, Xiang, Da, Jeff, Pan, Edwin, et al. "SWE-Bench Pro: Can AI Agents Solve Long-Horizon Software Engineering Tasks?" arXiv:2509.16941v2, 2025. https://arxiv.org/abs/2509.16941
  17. [17] OpenAI. "Separating signal from noise in coding evaluations." July 8, 2026. https://openai.com/index/separating-signal-from-noise-coding-evaluations/
  18. [18] Tian, et al. "SciCode: A Research Coding Benchmark Curated by Scientists." NeurIPS 2024 Datasets and Benchmarks Track. arXiv:2407.13168. https://arxiv.org/abs/2407.13168
  19. [19] Hu, Sihan, Huang, Lyuhan, Deng, Youjin, and Chen, Kun. "SciCode-Verified: How Benchmark Defects Underestimated the Scientific-Coding Ability of Language Models." arXiv:2608.04975, 2026. https://arxiv.org/abs/2608.04975
  20. [20] "Fixing Open LLM Leaderboard with Math-Verify." Hugging Face, 2025. https://huggingface.co/blog/math_verify_leaderboard
  21. [21] Dong, Jianshuo, Zhang, Yutong, Liu, Yan, Zhong, Zhenyu, Wei, Tao, Zhang, Chao, and Qiu, Han. "Revisiting the Reliability of Language Models in Instruction-Following" (IFEval++). ACL 2026 (main, oral). arXiv:2512.14754v3. https://arxiv.org/abs/2512.14754
  22. [22] Zhou, et al. "Instruction-Following Evaluation for Large Language Models" (IFEval). arXiv:2311.07911, 2023. https://arxiv.org/abs/2311.07911
  23. [23] Gema, Aryo Pradipta, Ong Jun Leang, Joshua, Hong, Giwon, et al. "Are We Done with MMLU?" (MMLU-Redux). arXiv:2406.04127v3, 2024. https://arxiv.org/abs/2406.04127
  24. [24] Zhai, Weiqi, et al. "HLE-Verified: A Systematic Verification and Structured Revision of Humanity's Last Exam." arXiv:2602.13964v4, 2026. https://arxiv.org/abs/2602.13964
  25. [25] Segato, Gian. "Quantifying infrastructure noise in agentic coding evals." Anthropic, February 5, 2026. https://www.anthropic.com/engineering/infrastructure-noise
  26. [26] Stein, Adam, Brown, Davis, Hassani, Hamed, Naik, Mayur, and Wong, Eric. "Detecting Safety Violations Across Many Agent Traces" (Meerkat). arXiv:2604.11806, 2026. https://arxiv.org/abs/2604.11806
  27. [27] Von Arx, Sydney, Chan, Lawrence, and Barnes, Beth. "Recent Frontier Models Are Reward Hacking." METR, June 5, 2025. https://metr.org/blog/2025-06-05-recent-reward-hacking/
  28. [28] Gurram, Bhaskar. "Auditing Automated Evaluation, Error Propagation, and Runtime Mitigation in Tool-Using Language Agents" (AgentProp-Bench). arXiv:2604.16706v2, 2026. https://arxiv.org/abs/2604.16706
  29. [29] Bertolazzi, Leonardo, Tentori, Katya, and Bernardi, Raffaella. "FalsifyBench: Evaluating Inductive Reasoning in LLMs with Rule Discovery Games." arXiv:2606.04751, June 2026. https://arxiv.org/abs/2606.04751
  30. [30] Zhao, Justin, Bhattacharjee, Himaghna, Korevaar, Hannah, Radharapu, Bhaktipriya, and El-Arini, Khalid. "Jagged Judges: Epistemic Stability Under Perturbation, Pressure, and Persistence." arXiv:2608.12645v2, 2026. https://arxiv.org/abs/2608.12645
  31. [31] "Terminal-Bench-Science 0.1: Evaluating AI agents on scientific research workflows." Terminal-Bench, August 27, 2026. https://www.tbench.ai/news/terminal-bench-science-0-1
  32. [32] Lin, Minhua, Wu, Juncheng, et al. "Harness Updating Is Not Harness Benefit: Disentangling Evolution Capabilities in Self-Evolving LLM Agents." arXiv:2605.30621, 2026. https://arxiv.org/abs/2605.30621
  33. [33] Jin, Tengjun, Zhu, Yuxuan, and Kang, Daniel. "ELT-Bench: An End-to-End Benchmark for Evaluating AI Agents on ELT Pipelines." Proc. VLDB Endow. 19(2), 2025, pp. 84–98. arXiv:2504.04808. https://arxiv.org/abs/2504.04808
  34. [34] Tsoukalas, George, Kovsharov, Anton, Shirobokov, Sergey, et al. "Advancing Mathematics Research with AI-Driven Formal Proof Search" (AlphaProof Nexus). arXiv:2605.22763, 2026. https://arxiv.org/abs/2605.22763
  35. [35] Ammanamanchi, Pawan Sasanka, Bhat, Siddharth, and Biderman, Stella. "Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving." ICML 2026. arXiv:2606.29493. https://arxiv.org/abs/2606.29493
  36. [36] Green, Ben. "100 open problems." 2024. https://people.maths.ox.ac.uk/greenbj/papers/openproblems.pdf
  37. [37] GasStationManager. "SafeVerify." 2025. https://github.com/GasStationManager/SafeVerify (accessed 2026-05-12).
  38. [38] Liu, Junqi, et al. "CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics." arXiv:2505.03171, May 2025. https://arxiv.org/abs/2505.03171
  39. [39] Ren, Z.Z., Shao, Zhihong, Song, Junxiao, et al. "DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition" (introduces ProverBench). arXiv:2504.21801v2, 2025. https://arxiv.org/abs/2504.21801
$ cat citation.bib
@misc{vasileva2026recursiveselfinflation,
  author = {Vasileva, Mariya I.},
  title  = {Recursive Self-Inflation: how self-improvement loops hillclimb on the verifier's mistakes},
  year   = {2026},
  month  = sep,
  url    = {https://mariya.fyi/posts/recursive-self-inflation},
  note   = {Blog post}
}