Proof-Carrying Cognition: Closing the Verification Gap with Reality-Settled Reward

# Proof-Carrying Cognition:Closing the Verification Gap with Reality-Settled Reward
Source: [https://arxiv.org/html/2609.09776](https://arxiv.org/html/2609.09776)
Eshwar Reddy MAI Engineer, TestsigmaUniversity of San Diegomalireddy\.eshwar@gmail\.comSourav KarmakarSenior AI Scientist, Intuit Indiasouravkarmakar29@gmail\.com

###### Abstract

Recent frontier progress in large language models has come predominantly from reinforcement learning on reasoning traces—and has been sharply concentrated in domains that possess a cheap, sound verifier\. We argue that the field’s binding constraint is therefore the*verification gap*: the absence of a scalable, incorruptible source of reward for reasoning outside narrowly formal domains\. We make four contributions\.\(1\) Theory:in a joint\-Gaussian model of best\-of\-NNselection we prove that verifier–gold correlationρ\\rhois the exact exchange rate between test\-time compute and capability, and that an unsound verifier must pay a polynomial compute penaltyN1/ρ2N^\{1/\\rho^\{2\}\}to match a sound one\.\(2\) Demonstration:in program\-synthesis testbeds with an executable ground truth—a minimal six\-token domain and a pre\-registered scaled replication in a∼1010\\sim\\\!10^\{10\}\-program domain with 2–4×\\timesmore tasks and stronger instruments—we show that unsound verifiers lose Soundness\-under\-Pressure as optimization pressure grows \(from 0\.94 to 0\.32 for a shallow verifier atN=4096N\{=\}4096\), collapsing absolutely in the small domain and plateauing in the rich one, while a sound verifier improves monotonically; that reality\-anchored settlement beats a frozen verifier under both i\.i\.d\. and directed adversarial pressure, including against an adversary that explicitly models the settlement process, driving the hacking gap from∼0\.27\\sim\\\!0\.27to∼0\\sim\\\!0; that soundness scales log\-linearly with settled labels, with on\-policy settlement∼10×\\sim\\\!10\\timesmore label\-efficient than random labeling and decisively better than an uncertainty\-sampling control; and that settlement improves the*resolution*of claims, not merely their calibration\. The replication also falsified two of our quantitative claims, which we report and repair: outside the Gaussian model the exchange rateρ\\rhois not quantitatively predictive, and the closed formN1/ρ2N^\{1/\\rho^\{2\}\}overstates the penalty at practicalNN\(the exact finite\-NNform of Proposition[1](https://arxiv.org/html/2609.09776#Thmproposition1)predicts matching budgets to within 3\.4%\)\.\(2b\) Real\-model evidence:in pre\-registered experiments with a real frontier\-family generator, real LLM judges, and real unit\-test execution as gold, the weak judge loses soundness under best\-of\-NNon both MBPP and HumanEval \(p<10−3p<10^\{\-3\}\); a stronger judge is significantly more robust—so the gap binds*conditionally*on judge capability relative to task difficulty; a learned settlement model anchored to executed outcomes cuts the judge’s pricing error by 59%, while naive in\-context anchoring makes it worse; and a prompt\-level LLM adversary failed to inflate the judge—while mining the same candidate banks shows selection alone manufactures\+0\.53\+0\.53hacking gaps from honest samples: the operative Goodhart pressure is selection, not persuasion\. A pre\-registered diagnosis of every failure yields a repaired, margin\-free exchange\-rate law \(the copula form predicts realized soundness of real LLM judges to 4% median error\) and a design constraint for the paradigm: average\-calibration anchoring provably cannot move soundness and empirically amplifies tail deceptions—the world model must match the expressiveness of the deception surface\.\(3\) Paradigm:we propose*proof\-carrying cognition*, a training loop in which reasoning steps are emitted as typed probabilistic claims, priced by a self\-built world model whose only loss is prediction of held\-out reality, and settled by strictly proper scoring rules—making reality, rather than human judgment, the ultimate reward function\.\(4\) Benchmark:we specify Soundness\-under\-Pressure, the headline metric for a reality\-settled reasoning benchmark, and argue that building this benchmark is the field’s single most important near\-term action\.\(2c\)Under real GRPO training, a frozen learned RM traces the full overoptimization curve—proxy reward climbs while executed reward collapses by 90%—and the identical RM refit on a 10% settlement stream preserves executed reward at 6×\\timesthe frozen arm’s and outperforms an equal\-budget LLM\-judge\-updated control, isolating reality as the label source; the registered drift\-alarm criterion failed its first test and is reported as such\.

## 1 Introduction

Two inventions define modern machine learning: backpropagation, which solved credit assignment over parameters\([Rumelhart et al\., 1986](https://arxiv.org/html/2609.09776#bib.bib24)\), and the transformer, which solved bandwidth over context\([Vaswani et al\., 2017](https://arxiv.org/html/2609.09776#bib.bib32)\)\. We argue that the next invention of comparable consequence must solve*credit assignment over thoughts*: determining, scalably and incorruptibly, whether a step of reasoning is correct\.

The argument proceeds from an empirical observation\. Frontier capability gains now come predominantly from reinforcement learning on chains of thought\([Wei et al\., 2022](https://arxiv.org/html/2609.09776#bib.bib33);[OpenAI, 2024](https://arxiv.org/html/2609.09776#bib.bib22);[Guo et al\., 2025](https://arxiv.org/html/2609.09776#bib.bib12)\), and these gains are sharply concentrated in domains with a cheap, sound verifier: mathematics with checkable answers\([Hendrycks et al\., 2021](https://arxiv.org/html/2609.09776#bib.bib15)\), code with executable tests\([Chen et al\., 2021](https://arxiv.org/html/2609.09776#bib.bib5)\), and formal proof with a kernel\([Trinh et al\., 2024](https://arxiv.org/html/2609.09776#bib.bib30);[AlphaProof and AlphaGeometry teams, Google DeepMind, 2024](https://arxiv.org/html/2609.09776#bib.bib1)\)\. The underlying recipe—sample many traces, keep those a verifier accepts, reinforce\([Zelikman et al\., 2022](https://arxiv.org/html/2609.09776#bib.bib35)\)—is a self\-improvement engine whose throttle is verifier coverage\. Where the verifier is sound, months of training have produced superhuman\-adjacent performance\. Where the only reward is a human preference label\([Christiano et al\., 2017](https://arxiv.org/html/2609.09776#bib.bib6);[Ouyang et al\., 2022](https://arxiv.org/html/2609.09776#bib.bib23)\)or an LLM judge, the same models plateau at fluent but unaccountable reasoning, because preference\-based reward is noisy, gameable, and shallower than the reasoning it evaluates\([Gao et al\., 2023](https://arxiv.org/html/2609.09776#bib.bib9)\)\.

This paper names that constraint the*verification gap*and attacks it from four directions:

- •Theory \(§[3](https://arxiv.org/html/2609.09776#S3)\)\.We prove that in best\-of\-NNselection, verifier–gold correlationρ\\rhois the exchange rate between compute and capability, with an unsound verifier paying a polynomial penaltyN1/ρ2N^\{1/\\rho^\{2\}\}in candidates \(Proposition[1](https://arxiv.org/html/2609.09776#Thmproposition1), Corollary[1](https://arxiv.org/html/2609.09776#Thmcorollary1)\); simulation matches theory to within0\.011​σ0\.011\\sigma\(Figure[1](https://arxiv.org/html/2609.09776#S2.F1)\)\.
- •Demonstration \(§[6](https://arxiv.org/html/2609.09776#S6)–§[7](https://arxiv.org/html/2609.09776#S7)\)\.In program\-synthesis testbeds with an executable gold verifier: learned verifiers are Goodharted under best\-of\-NNpressure \(relative soundness0\.94→0\.320\.94\\to 0\.32at scale; absolute collapse in the minimal domain\) while a sound verifier climbs monotonically; reality\-anchored settlement beats a frozen verifier under directed adversarial pressure, including a settlement\-aware adversary, driving the hacking gap to∼0\\sim\\\!0; verifier soundness scales log\-linearly with settled labels, with on\-policy settlement∼10×\\sim\\\!10\\timesmore label\-efficient than random labeling; and settlement raises claim*resolution*, rebutting the concern that settlement\-based reward favors vague claims\. §[7](https://arxiv.org/html/2609.09776#S7)reports a pre\-registered scaled replication, including the parts of our story it falsified\.
- •Paradigm \(§[5](https://arxiv.org/html/2609.09776#S5)\)\.We propose*proof\-carrying cognition*\(Algorithm[1](https://arxiv.org/html/2609.09776#alg1)\): reasoning as portfolios of falsifiable, priced claims, with reality as the only unamortized loss\.
- •Benchmark \(§[9](https://arxiv.org/html/2609.09776#S9)\)\.We give a formal metric, Soundness\-under\-Pressure, and a construction recipe for a reality\-settled reasoning benchmark\.

Scope note:this is a hybrid position\-and\-proof\-of\-concept paper\. The experiments in §[3](https://arxiv.org/html/2609.09776#S3)–§[6](https://arxiv.org/html/2609.09776#S6)are real and reproducible but deliberately minimal; they validate mechanisms, not frontier\-scale claims\.

## 2 The Bottleneck: Generation Has Scaled; Verification Has Not

### 2\.1 The verification gap

Define a*verifier*for a domainDDas an oracleV:claims⁡\(D\)→\[0,1\]V:\\mathrm\{claims\}\(D\)\\to\[0,1\]that is \(a\)*sound*—its acceptances track ground truth; \(b\)*cheap*—evaluatingVVcosts far less than generating a candidate; and \(c\)*robust under optimization*—an adversarially trained generator cannot systematically obtain reward fromVVfor false claims\. The verification gap is the observation that such oracles exist today only for formally grounded domains \(proof kernels, program execution, game rules\), and that every substitute used elsewhere—human raters, reward models, LLM judges—fails property \(c\) under sufficient optimization pressure\.[Gao et al\. \(2023\)](https://arxiv.org/html/2609.09776#bib.bib9)quantified the failure directly: optimizing against a fixed learned reward model yields proxy reward that rises while gold reward peaks and then falls—Goodhart’s law\([Strathern, 1997](https://arxiv.org/html/2609.09776#bib.bib28)\)operating as a hard ceiling\. A model cannot climb above the discrimination ability of its judge\([Leike et al\., 2018](https://arxiv.org/html/2609.09776#bib.bib20);[Bowman et al\., 2022](https://arxiv.org/html/2609.09776#bib.bib4)\)\.

Figure 1:Simulation \(dots; 20,000 trials per point\) versus theory \(lines;ρ​𝔼​\[maxN\]\\rho\\,\\mathbb\{E\}\[\\max\_\{N\}\]\) for best\-of\-NNselection under a proxy verifier with correlationρ\\rhoto gold\. Maximum absolute deviation from theory across all points:0\.011​σ0\.011\\sigma\. AtN=4096N\{=\}4096, theρ=0\.5\\rho\{=\}0\.5verifier realizes 50\.2% of the sound verifier’s gain, matching Proposition[1](https://arxiv.org/html/2609.09776#Thmproposition1)exactly\.
### 2\.2 Other bottlenecks reduce to it

The data wall\.High\-quality human text is finite, but self\-generated data is unbounded—*if*it can be trusted\. AlphaGo Zero\([Silver et al\., 2017](https://arxiv.org/html/2609.09776#bib.bib26)\)showed that with a perfect verifier \(game rules\), self\-play alone yields superhuman skill with no human data\. AlphaProof\([AlphaProof and AlphaGeometry teams, Google DeepMind, 2024](https://arxiv.org/html/2609.09776#bib.bib1)\)extended this to mathematics, reaching IMO silver\-medal standard on millions of autoformalized problems adjudicated by the Lean kernel\. The data wall is not a shortage of text; it is a shortage of trustworthy reward for synthetic reasoning\.

Unreliable agency\.Long\-horizon autonomy fails because errors compound with no mechanism to check intermediate steps before commitment\. A sound step\-level verifier converts open\-loop generation into closed\-loop, auditable action\.

Superhuman reasoning in open domains\.In science, strategy, law, and medicine, humans can no longer reliably grade superhuman homework; scalable oversight\([Amodei et al\., 2016](https://arxiv.org/html/2609.09776#bib.bib2);[Bowman et al\., 2022](https://arxiv.org/html/2609.09776#bib.bib4)\)is precisely the demand for verification that outruns the verifier’s unaided competence\.

## 3 Theory: Verifier Correlation Is the Compute–Capability Exchange Rate

We first make the cost of unsoundness quantitative in the cleanest possible model\. Best\-of\-NNselection—sampleNNcandidates, keep the one the verifier scores highest—is the canonical mechanism by which test\-time compute is converted into capability\([Cobbe et al\., 2021](https://arxiv.org/html/2609.09776#bib.bib7);[Snell et al\., 2024](https://arxiv.org/html/2609.09776#bib.bib27)\), and its induced optimization pressure grows aslog⁡N\\log N\.

###### Proposition 1\(Verifier exchange rate\)\.

Let\(Gi,Pi\)i=1N\(G\_\{i\},P\_\{i\}\)\_\{i=1\}^\{N\}be i\.i\.d\. jointly Gaussian pairs, standardized, withCorr⁡\(G,P\)=ρ\\mathrm\{Corr\}\(G,P\)=\\rho, whereGGis gold reward andPPthe proxy verifier’s score\. Leti∗=arg⁡maxi⁡Pii^\{\*\}=\\arg\\max\_\{i\}P\_\{i\}\. Then

𝔼⁡\[Gi∗\]=ρ​𝔼​\[maxi⁡Pi\]=ρ​2​ln⁡N​\(1\+o⁡\(1\)\)\.\\mathbb\{E\}\[G\_\{i^\{\*\}\}\]\\;=\\;\\rho\\,\\mathbb\{E\}\\\!\\left\[\\max\_\{i\}P\_\{i\}\\right\]\\;=\\;\\rho\\sqrt\{2\\ln N\}\\,\\big\(1\+o\(1\)\\big\)\.

###### Proof\.

DecomposeGi=ρ​Pi\+1−ρ2​ZiG\_\{i\}=\\rho P\_\{i\}\+\\sqrt\{1\-\\rho^\{2\}\}\\,Z\_\{i\}withZiZ\_\{i\}standard Gaussian, independent of\(P1,…,PN\)\(P\_\{1\},\\dots,P\_\{N\}\)\. The indexi∗i^\{\*\}is a function of\(P1,…,PN\)\(P\_\{1\},\\dots,P\_\{N\}\)alone; conditioning on these,Zi∗Z\_\{i^\{\*\}\}remains standard Gaussian with mean zero, so𝔼⁡\[Zi∗\]=0\\mathbb\{E\}\[Z\_\{i^\{\*\}\}\]=0and𝔼⁡\[Gi∗\]=ρ​𝔼​\[Pi∗\]=ρ​𝔼​\[maxi⁡Pi\]\\mathbb\{E\}\[G\_\{i^\{\*\}\}\]=\\rho\\,\\mathbb\{E\}\[P\_\{i^\{\*\}\}\]=\\rho\\,\\mathbb\{E\}\[\\max\_\{i\}P\_\{i\}\]\. The asymptotic𝔼⁡\[maxi⁡Pi\]∼2​ln⁡N\\mathbb\{E\}\[\\max\_\{i\}P\_\{i\}\]\\sim\\sqrt\{2\\ln N\}is standard extreme\-value theory for Gaussians\. ∎

###### Corollary 1\(Polynomial compute penalty of unsoundness\)\.

To match the expected gold reward that a sound verifier \(ρ=1\\rho\{=\}1\) attains withNNcandidates, a proxy verifier with correlationρ\\rhorequires

N′=N1/ρ2\(asymptotically\)\.N^\{\\prime\}\\;=\\;N^\{1/\\rho^\{2\}\}\\quad\\text\{\(asymptotically\)\.\}

###### Proof\.

Setρ​2​ln⁡N′=2​ln⁡N\\rho\\sqrt\{2\\ln N^\{\\prime\}\}=\\sqrt\{2\\ln N\}and solve:ln⁡N′=ln⁡N/ρ2\\ln N^\{\\prime\}=\\ln N/\\rho^\{2\}\. ∎

Two readings\.First,*within this model class, verifier correlation is the exchange rate between test\-time compute and capability*: every unit of inference compute is worth exactlyρ\\rhoof its sound\-verifier value \(Figure[1](https://arxiv.org/html/2609.09776#S2.F1)and the 100,000\-trial replication of §[7](https://arxiv.org/html/2609.09776#S7)confirm this to within0\.011​σ0\.011\\sigmaand0\.007​σ0\.007\\sigmarespectively\)\. Outside the model class the identity is*not quantitatively predictive in either direction*: in the synthetic testbed of §[7](https://arxiv.org/html/2609.09776#S7), a verifier with measuredρ≈0\.50\\rho\\approx 0\.50realizes only≈0\.32\\approx 0\.32of the sound verifier’s value atN=4096N\{=\}4096\(exploitable structure beyond Gaussian noise\), while real LLM judges \(§[8](https://arxiv.org/html/2609.09776#S8)\) with near\-zero*linear*correlation \(ρ≈0\.12\\rho\\approx 0\.12\) realize0\.740\.74atN=32N\{=\}32\(good top\-ranking despite poor linear fit\)\. Only the qualitative ordering—higher\-fidelity judges convert pressure to capability better—survived every testbed\. The repair \(§[8\.1](https://arxiv.org/html/2609.09776#S8.SS1)\) is to state the law in the invariant that selection actually sees:

###### Proposition 2\(Margin\-free exchange rate\)\.

Let\(Gi,Pi\)i=1N\(G\_\{i\},P\_\{i\}\)\_\{i=1\}^\{N\}be i\.i\.d\. with continuous margins and Gaussian copula parameterρc\\rho\_\{c\}, andi∗=arg⁡maxi⁡Pii^\{\*\}=\\arg\\max\_\{i\}P\_\{i\}\. Then the law ofGi∗G\_\{i^\{\*\}\}—henceSnd​@​N\\mathrm\{Snd\}@N—depends only onρc\\rho\_\{c\}and the margin ofGG; the margin ofPPis irrelevant\.

###### Proof\.

i∗i^\{\*\}is invariant under strictly increasing transforms ofPP, so transformPPto standard Gaussian; the conditional law ofGGgiven the ranks of\(P1,…,PN\)\(P\_\{1\},\\dots,P\_\{N\}\)is determined by the copula andGG’s margin\. ∎

Estimatingρc\\rho\_\{c\}from rank correlation and simulating with empirical margins predicts per\-problem realized soundness with median error 4\.1% on real LLM\-judge data, where Pearson\-based prediction errs by 79 points \(§[8\.1](https://arxiv.org/html/2609.09776#S8.SS1)\)\. Second, the penalty for unsoundness is superlinear in candidates\. Two cautions on the closed formN1/ρ2N^\{1/\\rho^\{2\}\}: it is asymptotic, and at practical budgets it materially overstates the penalty \(by up to 24×\\timesatρ=0\.5\\rho\{=\}0\.5,N≤16N\\leq 16; §[7](https://arxiv.org/html/2609.09776#S7)\)\. The exact finite\-NNconsequence of Proposition[1](https://arxiv.org/html/2609.09776#Thmproposition1)—N′N^\{\\prime\}solvesρ​𝔼​\[maxN′\]=𝔼⁡\[maxN\]\\rho\\,\\mathbb\{E\}\[\\max\_\{N^\{\\prime\}\}\]=\\mathbb\{E\}\[\\max\_\{N\}\]—predicts empirical matching budgets to within 3\.4% and should be used instead at finiteNN\. We note honestly that this linear\-Gaussian model predicts a slowed climb, not the*decline*observed empirically under heavy optimization\([Gao et al\., 2023](https://arxiv.org/html/2609.09776#bib.bib9)\); decline requires misspecification, and §[7](https://arxiv.org/html/2609.09776#S7)shows it is domain\-dependent: present in the minimal domain, absent \(plateau instead\) in a richer one at the pressures we could apply\.

## 4 The Validated Attack: Asymmetric Verification

The strongest evidence\-backed approach to the gap exploits a structural asymmetry: checking is often far cheaper than generating—morally the P\-versus\-NP gap, and the only free lunch available to this program\. Three mechanisms have real support\.

Formal grounding\.Autoformalization\([Wu et al\., 2022](https://arxiv.org/html/2609.09776#bib.bib34)\)lets a sound kernel adjudicate reasoning with zero Goodharting: a proof checker cannot be flattered\. AlphaGeometry\([Trinh et al\., 2024](https://arxiv.org/html/2609.09776#bib.bib30)\)and AlphaProof\([AlphaProof and AlphaGeometry teams, Google DeepMind, 2024](https://arxiv.org/html/2609.09776#bib.bib1)\)are existence proofs that self\-improvement loops close when the verifier is sound\. The kernel functions as a*trust anchor*—analogous to the small trusted computing base of secure systems—from which learned verifiers extend coverage but to which they must be re\-anchored\.

Process\-level verification\.Outcome reward is sparse and rewards lucky wrong reasoning; step\-level reward is dense and localizes error\. Process reward models outperform outcome\-only supervision on hard mathematics\([Uesato et al\., 2022](https://arxiv.org/html/2609.09776#bib.bib31);[Lightman et al\., 2024](https://arxiv.org/html/2609.09776#bib.bib21)\), extending[Cobbe et al\. \(2021\)](https://arxiv.org/html/2609.09776#bib.bib7), and verifier\-guided search gives test\-time compute its own scaling behavior\([Snell et al\., 2024](https://arxiv.org/html/2609.09776#bib.bib27)\)—which, by Proposition[1](https://arxiv.org/html/2609.09776#Thmproposition1), is worth exactly as much as the verifier is sound\.

Adversarial prover–verifier co\-training\.Debate\([Irving et al\., 2018](https://arxiv.org/html/2609.09776#bib.bib16)\)and prover–verifier games\([Kirchner et al\., 2024](https://arxiv.org/html/2609.09776#bib.bib18)\)train generator and verifier against each other;[Kirchner et al\. \(2024\)](https://arxiv.org/html/2609.09776#bib.bib18)report the property we most need—models trained to convince a weaker verifier produce reasoning that is genuinely easier for humans to check\.

Limits\.\(1\)*Coverage*: autoformalization of empirical claims \(“this drug target is promising”\) is unsolved\. \(2\)*Drift*: learned verifiers degrade under optimization pressure when the anchor is distant\([Gao et al\., 2023](https://arxiv.org/html/2609.09776#bib.bib9)\)\. \(3\)*The legibility tax*: checkable formats may exclude valid intuitions that resist formalization\. These limits motivate our proposal\.

## 5 Proof\-Carrying Cognition

We now state the central hypothesis of this paper\.

Hypothesis\.*Stop verifying reasoning against human judgment\. Verify it against predicted reality, using a world model the system itself constructs and is scored on—so that every chain of thought becomes a portfolio of falsifiable bets, and reality becomes the reward function\.*

We call the paradigm*proof\-carrying cognition*\(PCC\), by analogy to proof\-carrying code: an artifact is admitted not because an authority approves it, but because it carries the material needed to check it\. Science operates this way institutionally; PCC makes an AI system’s internal reasoning operate this way, step by step, at training scale\.

Figure 2:Proof\-carrying cognition\. Reasoning steps are emitted as typed, probabilistic claims in a claim ledger\. A self\-built world model prices claims densely and immediately; reality settles them sparsely but incorruptibly, and the world model’s own loss is anchored exclusively to that settlement\. Reward for reasoning is expected score under proper scoring rules, not judge approval\.### 5\.1 Architecture and training loop

PCC has three components \(Figure[2](https://arxiv.org/html/2609.09776#S5.F2); Algorithm[1](https://arxiv.org/html/2609.09776#alg1)\)\.

Claim ledger\.Reasoning steps are emitted not only as natural\-language thoughts but as typed, probabilistic claims: causal graphs with quantitative edges, executable snippets, fully formal statements where possible, calibrated forecasts where not\. The ledger generalizes autoformalization\([Wu et al\., 2022](https://arxiv.org/html/2609.09776#bib.bib34)\)from theorems to empirical assertions\.

Self\-built world model\.A persistent, versioned model prices ledger claims\. Its*only*training loss is prediction of held\-out reality: experimental outcomes, execution traces, time\-lagged observations\. This extends the world\-model tradition\([Ha and Schmidhuber, 2018](https://arxiv.org/html/2609.09776#bib.bib13);[LeCun, 2022](https://arxiv.org/html/2609.09776#bib.bib19)\)with a specific institutional role: the world model is*amortized reality*—dense, immediate reward now, with periodic settlement keeping the amortizer honest\.

Terminology\.We reserve*world model*for the full generative component above\. The learned predictors in our experiments \(§[6](https://arxiv.org/html/2609.09776#S6)–§[8](https://arxiv.org/html/2609.09776#S8)\) are deliberately minimal*settlement models*—amortizers of settled outcomes over shallow features—and should not be read as world models in the model\-based\-RL or generative sense; building the latter at training scale is untested \(§[10](https://arxiv.org/html/2609.09776#S10)\)\.

Internal prediction market\.Instances of the reasoner stake calibration capital on claims; settlement uses strictly proper scoring rules\([Savage, 1971](https://arxiv.org/html/2609.09776#bib.bib25);[Gneiting and Raftery, 2007](https://arxiv.org/html/2609.09776#bib.bib11)\), adjudicated by the world model near\-term and reality long\-term\. The construction is deliberately reminiscent of logical induction\([Garrabrant et al\., 2016](https://arxiv.org/html/2609.09776#bib.bib10)\), where market dynamics over settled claims yield asymptotically calibrated, non\-exploitable beliefs\.

Algorithm 1Proof\-Carrying Cognition \(one epoch\)1:reasoner

πθ\\pi\_\{\\theta\}; world model

WϕW\_\{\\phi\}; settlement queue

QQ; proper scoring rule

SS; drift threshold

τ\\tau
2:foreach batch of tasksdo

3:

πθ\\pi\_\{\\theta\}emits traces with typed claims

\{\(ci,pi\)\}\\\{\(c\_\{i\},p\_\{i\}\)\\\}
4:near\-term reward

r←∑iS⁡\(pi,Wϕ​\(ci\)\)r\\leftarrow\\sum\_\{i\}S\(p\_\{i\},W\_\{\\phi\}\(c\_\{i\}\)\)
5:update

πθ\\pi\_\{\\theta\}by RL on

rr
6:enqueue claims with settlement handles in

QQ
7:endfor

8:foreach settled claim

\(c,y\)\(c,y\)dequeued from

QQdo

9:update

WϕW\_\{\\phi\}on loss

ℓ​\(Wϕ​\(c\),y\)\\ell\(W\_\{\\phi\}\(c\),y\)⊳\\trianglerightonly loss: reality

10:pay/charge staked instances by

S⁡\(p,y\)S\(p,y\)
11:endfor

12:drift

D←𝔼⁡\[\|Wϕ​\(c\)−y\|\]D\\leftarrow\\mathbb\{E\}\\big\[\\,\|W\_\{\\phi\}\(c\)\-y\|\\,\\big\]on settled claims

13:if

D\>τD\>\\tauthen

14:downweight near\-term reward; raise settlement rate

15:endif

### 5\.2 Why it can work where current approaches fail

PCC dissolves the Goodhart problem structurally rather than patching it\. Every existing reward source—human labels, LLM judges, learned PRMs—is a*model*of correctness, and a sufficiently strong optimizer eventually games any fixed model of correctness\([Gao et al\., 2023](https://arxiv.org/html/2609.09776#bib.bib9)\)\. Reality is the unique reward function that cannot be gamed, only predicted\. The classical objection—reality’s feedback is too sparse and slow to train on—is answered by amortization, and the amortizer’s drift is itself measurable \(line 10 of Algorithm[1](https://arxiv.org/html/2609.09776#alg1)\) rather than an invisible failure mode\. PCC thus combines the density of a learned verifier with the incorruptibility of a formal kernel, extended for the first time into empirical domains, and it obeys the bitter lesson\([Sutton, 2019](https://arxiv.org/html/2609.09776#bib.bib29)\): it substitutes computation and settled data for hand\-built judgment\.

## 6 Minimal Empirical Demonstrations

We validate the paper’s two core mechanisms in a testbed small enough to be fully reproducible on a laptop, yet possessing the one property that matters: an executable, incorruptible gold verifier\. All numbers below are measured, not estimated\. We stress the scope honestly: these are mechanism demonstrations, not frontier\-scale evidence\.

Figure 3:Goodharting under optimization pressure\. Best\-of\-NNselection by the sound \(execution\) verifier improves monotonically to 0\.83 gold reward\. Selection by the learned verifier inflates its own proxy score \(dashed\) while realized gold reward peaks nearN=512N\{=\}512and*falls*to 0\.10 atN=2048N\{=\}2048—the overoptimization signature of[Gao et al\. \(2023\)](https://arxiv.org/html/2609.09776#bib.bib9), reproduced with a fully transparent gold standard\.### 6\.1 Setup: program synthesis with executable ground truth

Tasks are drawn by sampling a hidden target program of length 4 over a six\-token integer DSL \(\+1\+1,−1\-1,×2\\times 2,×3\\times 3, negate, square\); a candidate program’s*gold reward*is the fraction of eight input–output points it matches under execution \(the sound verifier\)\. The*learned verifier*is a ridge regressor over token unigram/bigram counts and length—a deliberately shallow judge, standing in for any verifier that evaluates surface features of reasoning rather than executing it—fit on 1,000 labeled random programs per task\. Results aggregate 60 tasks; shaded bands are±1\\pm 1s\.e\.

Table 1:Soundness\-under\-Pressure \(Definition[1](https://arxiv.org/html/2609.09776#Thmdefinition1)\) of the learned verifier in the program\-synthesis testbed\. A sound verifier scores 1\.00 at everyNNby construction\.
### 6\.2 Result 1: learned verifiers collapse under pressure; sound ones do not

Figure[3](https://arxiv.org/html/2609.09776#S6.F3)shows gold reward of the selected program as optimization pressure \(best\-of\-NN\) increases\. Both verifiers start at 0\.079 atN=1N\{=\}1\. The execution verifier climbs monotonically to 0\.831 atN=2048N\{=\}2048\. The learned verifier’s*proxy*score rises throughout, but the gold reward of its selections peaks nearN=512N\{=\}512and declines to 0\.104—the qualitative overoptimization curve of[Gao et al\. \(2023\)](https://arxiv.org/html/2609.09776#bib.bib9), here with a fully transparent gold standard\. Table[1](https://arxiv.org/html/2609.09776#S6.T1)reports the induced soundness metric \(defined in §[9](https://arxiv.org/html/2609.09776#S9)\): it collapses from 1\.00 to 0\.13 asNNgrows\. Optimization pressure does not merely fail to help an unsound verifier; it actively*inverts*it\.

Figure 4:The settlement loop of Algorithm[1](https://arxiv.org/html/2609.09776#alg1)in miniature \(60 tasks,±1\\pm 1s\.e\.\)\.Left:anchor drift\|proxy−gold\|\|\\text\{proxy\}\-\\text\{gold\}\|on selected claims\. Anchored settlement reduces drift by 26%; the frozen verifier does not improve\.Right:gold reward of the top selection per round\. Anchoring roughly doubles achieved reward \(0\.154→0\.3060\.154\\to 0\.306\) while the frozen verifier stagnates and slightly degrades \(0\.154→0\.1250\.154\\to 0\.125\)\.
### 6\.3 Result 2: reality\-anchored settlement bounds drift and compounds capability

We then run the settlement loop of Algorithm[1](https://arxiv.org/html/2609.09776#alg1)in miniature: each round, sample a pool of 512 programs, select the top 32 by the learned verifier,*settle*them by execution, append the settled labels to the verifier’s training set, and refit—versus a frozen\-verifier baseline\. Over ten rounds \(Figure[4](https://arxiv.org/html/2609.09776#S6.F4)\), the frozen verifier’s anchor drift stays flat \(≈0\.10\\approx 0\.10\) and its achieved gold reward*decreases*from 0\.154 to 0\.125: repeatedly harvesting the same exploitable features yields no compounding\. The anchored verifier’s drift falls by 26% \(0\.101→0\.0750\.101\\to 0\.075\) and its achieved gold reward roughly*doubles*\(0\.154→0\.3060\.154\\to 0\.306\)\. The mechanism is exactly the paper’s thesis in microcosm: settlement converts the verifier’s own selection pressure into training signal, so the places where the verifier is most wrong are precisely the places reality corrects it first\.

### 6\.4 Result 3: an adversarial generator hacks a frozen verifier; settlement inverts the exploit

Best\-of\-NNapplies i\.i\.d\. pressure; RL applies*directed*pressure\. We therefore attack each verifier with an adaptive adversary: steepest\-ascent search that proposes 16 mutations per step and moves to the highest\-scoring one, for 250 steps \(40 tasks\)\. The anchored condition settles the adversary’s own trajectory \(25 visited programs\) by execution every 25 steps and refits—charging a total settlement budget of 250 reality queries per run, which we report as the explicit price of trust\.

Figure 5:Adversarial optimization against three verifiers \(40 tasks,±1\\pm 1s\.e\.\)\.Left:against a sound verifier, adversarial pressure is capability \(0\.869\); against a frozen learned verifier, the adversary locks into a hacked optimum within∼15\\sim\\\!15steps \(0\.178, flat\); anchored settlement keeps repairing the landscape \(0\.297 and rising,\+67%\+67\\%over frozen\)\.Right:the frozen verifier’s hacking gap \(proxy−\-gold\) locks in positive; settlement*inverts*it—the verifier learns to distrust the adversary’s region\.Figure[5](https://arxiv.org/html/2609.09776#S6.F5)shows three regimes\. Against the*sound*verifier, adversarial pressure is simply capability: gold reward climbs to 0\.869\. Against the*frozen*learned verifier, the adversary saturates the proxy within∼15\\sim\\\!15steps and locks permanently into a hacked optimum: gold reward flatlines at 0\.178 with a persistent positive hacking gap \(\+0\.037\+0\.037\)—the verifier permanently overvalues exactly the programs the adversary produces\. Against the*anchored*verifier, settlement re\-prices the adversary’s region each round: the hacking gap does not merely shrink but*inverts*to−0\.101\-0\.101—after settlement, the verifier systematically distrusts the region the adversary inhabits—and gold reward reaches 0\.297, a 67% improvement over frozen, still rising at step 250\. Two honest observations: anchoring restores*trustworthiness*\(the adversary can no longer sustain inflated scores\) but does not close the capacity gap to the sound verifier—a shallow feature model remains shallow—and the inverted gap means anchored pricing errs conservative, which is the safe failure direction but not a free one\.

Figure 6:Soundness scales with settlement \(40 tasks,±1\\pm 1s\.e\.\)\. Soundness AUC vs\. settled\-label budgetSS\. On\-policy settlement \(label what the verifier selects\) scales log\-linearly; 150 on\-policy labels beat 1,500 random labels—over 10×\\timeslabel efficiency\.
### 6\.5 Result 4: soundness scales with settlement, and on\-policy settlement is\>\>10×\\timesmore label\-efficient

If settlement is the fuel of trustworthy verification, soundness should scale with the settled\-label budget—and settling*where the verifier is deployed*should beat settling at random\. We sweep settlement budgetsS∈\{0,50,150,500,1500\}S\\in\\\{0,50,150,500,1500\\\}on a weaker base verifier \(500 random labels\) under two acquisition policies:*on\-policy*\(iteratively label the programs the current verifier selects\) and*random*\(the same number of labels on random programs\), then measure the Soundness AUC of Definition[1](https://arxiv.org/html/2609.09776#Thmdefinition1)on fresh pools \(40 tasks\)\.

Figure[6](https://arxiv.org/html/2609.09776#S6.F6): on\-policy settlement scales approximately log\-linearly,0\.500→0\.7060\.500\\to 0\.706, while random labeling crawls,0\.531→0\.5950\.531\\to 0\.595\. Strikingly, 150 on\-policy settled labels \(0\.617\) outperform 1,500 random labels \(0\.595\): on\-policy settlement is more than10×10\\timesmore label\-efficient\. The mechanism is the thesis in one line—*the verifier’s selection pressure concentrates settlement exactly where the verifier is most wrong*—and it is why Algorithm[1](https://arxiv.org/html/2609.09776#alg1)settles the claims the reasoner actually stakes, not a random audit sample\.

### 6\.6 Result 5: settlement buys resolution, not just calibration

A standing objection to settlement\-based reward \(§[11](https://arxiv.org/html/2609.09776#S11), failure mode 2\) is that it teaches systems to make safe, vague claims: probabilities near base rate are never badly wrong\. Proper scoring rules decompose exactly along this axis\([Gneiting and Raftery, 2007](https://arxiv.org/html/2609.09776#bib.bib11)\): the Brier score splits into*reliability*\(miscalibration; lower is better\) and*resolution*\(how far claims usefully depart from the base rate; higher is better\)\. We run twelve settlement rounds of probabilistic claims \(“this program matches at least 2/8 I/O points”\), 1,920 settled claims per round across 60 tasks, refitting the claim model on settled outcomes each round\.

Figure 7:Brier decomposition over twelve settlement rounds \(1,920 settled claims per round\)\. Settlement improves calibration \(reliability−40%\-40\\%,left\) while*doubling*resolution \(\+98%\+98\\%,right\): claims get sharper, not vaguer\.Figure[7](https://arxiv.org/html/2609.09776#S6.F7): reliability falls0\.0064→0\.00390\.0064\\to 0\.0039\(−40%\-40\\%\)*and*resolution doubles,0\.051→0\.1010\.051\\to 0\.101\(\+98%\+98\\%\)\. In this setting, settlement did not push claims toward the vague base rate; it sharpened them, because a claim model refit on settled outcomes gains exactly the discriminative signal that resolution measures\. This does not retire the failure mode—an agent choosing*which*claims to stake could still select easy ones, which is why RSR\-Bench must score resolution explicitly—but it shows the training dynamics do not intrinsically collapse toward vagueness\.

### 6\.7 What these demonstrations do and do not show

They show, with measured numbers, that \(i\) the exchange\-rate law of §[3](https://arxiv.org/html/2609.09776#S3)is quantitatively exact in its model class; \(ii\) unsound verifiers invert under i\.i\.d\. pressure and are locked into hacked optima under directed adversarial pressure; \(iii\) the anchoring mechanism at the heart of PCC produces the predicted behavior—bounded and even inverted exploitation, compounding capability—against both kinds of pressure; \(iv\) soundness scales with settlement, log\-linearly and with a large on\-policy efficiency multiplier; and \(v\) settlement sharpens claims rather than blunting them\. They do*not*show that a claim language rich enough for open\-ended reasoning exists, that world\-model amortization scales, that these effects survive when the generator is a frontier LLM trained by RL rather than a search process, or that anchoring can close \(rather than narrow\) the capacity gap to a sound verifier\. Those are precisely the questions the programme of §[10](https://arxiv.org/html/2609.09776#S10)is designed to answer\.

## 7 Scaled Pre\-registered Replication

The demonstrations of §[6](https://arxiv.org/html/2609.09776#S6)are deliberately minimal, so we commissioned an adversarial replication at larger scale, with every pass/fail criterion*pre\-registered before any experiment ran*\. The suite was designed to break our claims, not to confirm them: it uses a 10\-token DSL with∼1010\\sim\\\!10^\{10\}candidate programs \(versus∼4\.6×104\\sim\\\!4\.6\\times 10^\{4\}\), 16 I/O points, 2–4×\\timesmore tasks with paired Wilcoxon statistics, a*strong*learned verifier \(gradient\-boosted trees over 359 features, held\-outρ≈0\.77\\rho\\approx 0\.77\) alongside the shallow ridge verifier \(ρ≈0\.50\\rho\\approx 0\.50\), an*uncertainty\-sampling*control for the on\-policy claim, and—the gap our Limitations previously conceded—a*settlement\-aware*adversary that detects refits and deliberately relocates to unsettled regions\. Verdicts on the ten registered hypotheses: six passed, three failed, and one registered criterion was itself invalid; we report all of it\.

Table 2:Pre\-registered verdicts\.∗Our registered H2b criterion \(final gold below per\-task peak overNN\) is biased toward detecting decline; a valid exploratory test shows the strong verifier does*not*collapse \(see text\)\.Figure 8:Theory at scale\.\(a\)Proposition[1](https://arxiv.org/html/2609.09776#Thmproposition1)holds to0\.007​σ0\.007\\sigmaover 100,000 trials per point,NNto2142^\{14\}\.\(b\)But the asymptotic penaltyN1/ρ2N^\{1/\\rho^\{2\}\}\(dashed\) overstates the empirically required budget \(dots\) by up to 24×\\timesat practicalNN; the exact finite\-NNform \(solid\) matches within 3\.4%\.What survived—and got stronger\.The anchoring mechanism replicated everywhere we could aim pressure at it\. Under the settlement loop \(H3; 120 tasks weak, 60 tasks strong, 12 rounds\), anchored settlement beat the frozen verifier on achieved gold reward for*both*verifier classes \(weak: 0\.312 vs\. 0\.180,p=2\.7×10−9p=2\.7\\times 10^\{\-9\}; strong: 0\.358 vs\. 0\.272,p=5\.5×10−6p=5\.5\\times 10^\{\-6\}\) while reducing anchor drift \(−12%\-12\\%and−44%\-44\\%respectively, bothp<10−7p<10^\{\-7\}\)\. Under directed adversarial pressure \(H4; 100 tasks, 300 steps, Figure[11](https://arxiv.org/html/2609.09776#S7.F11)\), the frozen verifier stays hacked against every adversary \(persistent gap∼0\.26\\sim\\\!0\.26–0\.280\.28\), while anchored settlement drives the gap to∼0\\sim\\\!0–0\.040\.04against all three—*including the settlement\-aware adversary*, which relocated to unsettled regions after each refit and still could not sustain inflated scores \(gap 0\.039 vs\. frozen 0\.264,p<10−15p<10^\{\-15\}; gold 0\.279 vs\. 0\.206,p=4\.0×10−6p=4\.0\\times 10^\{\-6\}\)\. The registered H4 verdict is nonetheless*partial*: in the steepest\-ascent cell, anchored gold did not beat frozen \(0\.207 vs\. 0\.211,p=0\.46p=0\.46\)\. Exploratory diagnosis attributes this to adversary paralysis—that hill climber compares candidates against a stale pre\-refit score and freezes after the first settlement; with the incumbent rescored after refits, anchoring wins the cell too \(0\.282 vs\. 0\.211,p=5\.8×10−6p=5\.8\\times 10^\{\-6\}\)\. We report the registered failure and the diagnosis together\. Settlement scaling \(H5, 80 tasks\) replicated with a sharper control: Soundness AUC scales log\-linearly in the settled budget \(R2=0\.92R^\{2\}=0\.92\), on\-policy settlement atS=300S\{=\}300already beats random labeling atS=3000S\{=\}3000\(p=3\.7×10−4p=3\.7\\times 10^\{\-4\}; the∼10×\\sim\\\!10\\timesmultiplier\), and the uncertainty\-sampling control barely improves on random \(0\.587 vs\. 0\.579 atS=3000S\{=\}3000\)—the efficiency comes specifically from settling*where selection pressure concentrates*, not from generic active learning\. Calibration\-versus\-resolution \(H6, 100 tasks, 15 rounds\) replicated: resolution\+70%\+70\\%\(p=3\.2×10−10p=3\.2\\times 10^\{\-10\}\) with reliability improved, not traded away\.

Figure 9:Goodharting in the rich domain \(120 tasks,±1\\pm 1s\.e\.\)\.\(a\)The weak verifier*plateaus*rather than collapsing; the strong verifier keeps climbing throughN=4096N\{=\}4096\.\(b\)Relative soundnessSnd​@​N\\mathrm\{Snd\}@Nnonetheless degrades for both \(0\.94→0\.320\.94\\to 0\.32weak,0\.94→0\.590\.94\\to 0\.59strong\): pressure is increasingly wasted, even when it is not inverted\.Figure 10:Settlement scaling at scale \(80 tasks\)\. On\-policy settlement scales log\-linearly \(R2=0\.92R^\{2\}\{=\}0\.92\) and dominates both random labeling and an uncertainty\-sampling control:S=300S\{=\}300on\-policy labels beatS=3000S\{=\}3000random labels\.What failed—and how we repair it\.Three registered claims did not survive, all on the quantitative\-theory side\.*\(i\) The exchange rate does not transfer quantitatively*\(H1c\): across 120 tasks the ordering is preserved \(Spearman 0\.59 between per\-taskρ\\rhoand realizedSnd​@​4096\\mathrm\{Snd\}@4096\), but the realized fraction falls short ofρ\\rhoon 76% of tasks \(median gap 0\.27; mean 0\.32 realized vs\.ρ≈0\.50\\rho\\approx 0\.50\)\. Proposition[1](https://arxiv.org/html/2609.09776#Thmproposition1)should therefore be read as an*optimistic ceiling*once the proxy has exploitable structure; we have revised §[3](https://arxiv.org/html/2609.09776#S3)accordingly\.*\(ii\) The closed\-form penalty is asymptotic\-only*\(H1b\): atρ=0\.5\\rho\{=\}0\.5the empirical budget needed to match a sound verifier atN∈\{4,8,16\}N\\in\\\{4,8,16\\\}is 8–24×\\times*smaller*thanN1/ρ2N^\{1/\\rho^\{2\}\}predicts, while the exact finite\-NNform matches within 3\.4% \(Figure[8](https://arxiv.org/html/2609.09776#S7.F8)b\); the corollary is now stated with that caveat\.*\(iii\) Absolute collapse is domain\-dependent*\(H2a\): in the rich domain the weak verifier’s gold reward plateaus \(0\.191 peak atN=256N\{=\}256, 0\.184 atN=4096N\{=\}4096; decline not significant,p=0\.25p=0\.25\) instead of inverting as it does in the minimal domain—the collapse of Figure[3](https://arxiv.org/html/2609.09776#S6.F3)is real but not universal at these pressures\. Finally, our own registered H2b criterion turned out to be statistically invalid \(comparing a final value to a per\-task maximum over 13 noisy points detects “decline” even in monotone curves\), and the honest exploratory answer runs*against*our generalized claim: the strong verifier’s gold reward rises monotonically throughN=4096N\{=\}4096\(0\.056→0\.3570\.056\\to 0\.357; 4096 vs\. 1024:p=0\.0023p=0\.0023\) even as itsSnd​@​N\\mathrm\{Snd\}@Nerodes to 0\.59\. Within the pressure this suite could apply, verifier strength bought real robustness, not merely delay\. Whether a strong verifier inverts at pressures beyondN=4096N\{=\}4096is open; what is already established is that its compute is increasingly wasted relative to a sound verifier—which is the economic argument for settlement either way\. We also note the toy suite’s*inverted*hacking gap \(§[6](https://arxiv.org/html/2609.09776#S6), Result 3\) did not reproduce at scale: anchored gaps go to approximately zero \(honest pricing\) rather than negative \(conservative distrust\)\.

Figure 11:Adversarial pressure at scale \(100 tasks, 300 steps,±1\\pm 1s\.e\.\)\. Top: gold reward of the adversary’s champion against sound \(green\), anchored \(blue\), and frozen \(red\) verifiers, for steepest\-ascent, evolutionary, and*settlement\-aware*adversaries\. Bottom: hacking gap \(proxy−\-gold\)\. Frozen verifiers stay hacked \(gap∼0\.26\\sim\\\!0\.26–0\.280\.28\); anchored settlement drives the gap to∼0\\sim\\\!0against all three adversaries, including the one that models the settlement process\. The steepest\-ascent gold cell is the registered failure discussed in the text\.
## 8 Real\-Code and Real\-Model Experiments

Synthetic testbeds, however hardened, are proxies\. We therefore ran two further pre\-registered suites on real substrate \(criteria frozen before execution\)\. The*real\-code*suite uses MBPP\([Austin et al\., 2021](https://arxiv.org/html/2609.09776#bib.bib3)\): 974 human\-written Python programs whose real unit tests, executed locally, are the sound verifier; learned verifiers are trained*across*problems \(486 train / 487 eval\), like reward models, over surface and AST features of real code\. The*real\-model*suite, run by the author against the production Claude API, uses a real generator \(claude\-haiku\-4\-5, 32–48 samples/problem\), two real LLM judges scoring code*without executing it*\(claude\-haiku\-4\-5 weak; claude\-sonnet\-4\-6 strong\), and local execution of the real test suites of MBPP and HumanEval\([Chen et al\., 2021](https://arxiv.org/html/2609.09776#bib.bib5)\)as gold\.

Figure 12:Real LLM judges under best\-of\-NNselection over real generated code \(executed tests as gold; problems with zero gold variance excluded,n=60n\{=\}60MBPP / 18 HumanEval\)\. The weak judge’sSnd​@​N\\mathrm\{Snd\}@Ndegrades significantly on both benchmarks; the strong judge is significantly more robust\.The Goodhart mechanism is real \(registered passes\)\.The weak LLM judge loses Soundness\-under\-Pressure asNNgrows:Snd​@​2=0\.835→Snd​@​32=0\.729\\mathrm\{Snd\}@2=0\.835\\to\\mathrm\{Snd\}@32=0\.729on MBPP \(p=10−4p\{=\}10^\{\-4\},n=60n\{=\}60\) and0\.889→0\.7500\.889\\to 0\.750on HumanEval \(p=\.004p\{=\}\.004\)—Figure[12](https://arxiv.org/html/2609.09776#S8.F12)\. On real human code with cross\-problem verifiers, the collapse is catastrophic: the surface verifier falls fromSnd​@​4=0\.325\\mathrm\{Snd\}@4=0\.325toSnd​@​256=0\.016\\mathrm\{Snd\}@256=\\mathbf\{0\.016\}, and even the gradient\-boosted verifier reaches only 0\.052—real code under a global verifier is a far harsher regime than any of our per\-task synthetic worlds\.

Judge capability buys robustness \(registered pass, against our strong\-form thesis\)\.The strong judge’s soundness AUC exceeds the weak judge’s \(0\.856 vs\. 0\.814,p=9×10−4p\{=\}9\\times 10^\{\-4\}\), and—exploratory—its ownN=2→32N\{=\}2\\to 32degradation is not significant \(0\.855→0\.8210\.855\\to 0\.821,p=0\.43p\{=\}0\.43\)\. This converges with §[7](https://arxiv.org/html/2609.09776#S7)’s finding that a strong learned verifier kept climbing: across two independent methodologies,*the verification gap binds conditionally—when judge capability is at or below task difficulty—and scaling the judge materially repairs soundness at the pressures we could apply*\. Whether the repair persists at frontier\-difficulty tasks under RL\-scale pressure is precisely what RSR\-Bench \(§[9](https://arxiv.org/html/2609.09776#S9)\) must measure\.

Anchoring: the mechanism matters, and so does headroom \(registered failures, reported\)\.In the LLM settlement loop \(40 problems, 8 rounds\), neither anchored arm raised achieved gold over the frozen judge—a ceiling effect: the generator solves MBPP so well \(mean candidate gold 0\.81; the frozen judge’s top\-1 was already perfect on 34/40 problems\) that there was no headroom, and the registered RL2a/RL2b verdicts are FAIL\. Where headroom existed—the real\-code suite, whose frozen cross\-problem verifier earned gold 0\.000—anchored settlement lifted achieved gold to 0\.153 \(p=\.004p\{=\}\.004\), though its registered drift clause failed \(drift rose as selections moved into higher\-value, harder\-to\-price regions\)\. The sharpest real\-model result is*how*to anchor: a learned settlement head over the judge’s score and code features, refit on executed outcomes \(a deliberately minimal instantiation of Algorithm[1](https://arxiv.org/html/2609.09776#alg1)’s amortizer\), cut pricing drift by 59% \(0\.352→0\.1460\.352\\to 0\.146,p≈0p\\approx 0\) and cut\|judge−gold\|\|\\text\{judge\}\-\\text\{gold\}\|on adversarial code from 0\.326 to 0\.254; naive in\-context anchoring \(showing the judge a ledger of its own settled errors\) made the judge*worse*on both metrics \(p<10−9p<10^\{\-9\}\)\. Amortize reality into a trained pricing model; do not merely show a judge its mistakes\.

Positioning against standard baselines\.The frozen\-vs\-anchored contrast*is*the comparison to online reward\-model retraining: the anchored arm retrains its verifier online, and what the paradigm adds is the label source \(settled execution rather than fresh preference or judge labels\) and the schedule \(the verifier’s own selections\)\. The uncertainty\-sampling control of §[7](https://arxiv.org/html/2609.09776#S7)separates this from generic active learning: committee\-variance acquisition barely beat random labeling \(0\.587 vs\. 0\.579 atS=3000S\{=\}3000\) where on\-policy settlement reached 0\.664\. Verifier ensembles and process reward models are verifier\-strength interventions, orthogonal to the settlement axis; the verifier\-strength axis is measured directly here \(H2b, RL1b\) and buys real robustness\. Table[3](https://arxiv.org/html/2609.09776#S8.T3)gives the mechanism\-level ablation of anchoring itself; a full\-architecture ablation \(typed claims, market, staking\) requires those components to exist and is future work \(§[10](https://arxiv.org/html/2609.09776#S10)\)\.

Table 3:Mechanism ablation of anchoring on the real\-model data \(weak judge\)\. Loop drift: final\-round\|score−gold\|\|\\text\{score\}\-\\text\{gold\}\|on selections \(RL2\)\. Adv\.\|\|gap\|\|: out\-of\-problem\|judge−gold\|\|\\text\{judge\}\-\\text\{gold\}\|on adversarial candidates \(RL3c\); the isotonic row reports its signed tail effect on mined deceptions \(F4\)\. Only the feature\-level settlement head helps on both\.Adversarial pressure: selection, not persuasion \(registered failures, informative\)\.The prompt\-level adversary failed its manipulation check—the “subtly wrong” code it wrote was mostly right \(adversarial gold 0\.839, matching honest quality\)—so RL3a is an invalid test of hackability rather than evidence of robustness\. The iterative adversary, shown the judge’s score after each of four revisions, drove score and gold*down*\(0\.679→0\.5670\.679\\to 0\.567;0\.878→0\.7330\.878\\to 0\.733\): at this capability level, directed prompt\-space search could not climb a real judge, and the operative Goodhart pressure on LLM judges is the selection pressure of RL1, not persuasion\. One registered criterion \(RL3c\) passed for the wrong reason: it assumed judges overvalue adversarial code, but these judges undervalue everything \(mean gap−0\.20\-0\.20\), so the in\-context ledger “reduced the gap” by worsening underconfidence; on the substantive\|gap\|\|\\text\{gap\}\|metric only the world\-model head helps\. We disclose this as the suite’s second mis\-specified criterion \(with §[7](https://arxiv.org/html/2609.09776#S7)’s H2b\) and record the process lesson: register criteria on\|error\|\|\\text\{error\}\|\. Finally, the on\-policy label\-efficiency claim failed on real code for a second time \(on\-policy@240 AUC 0\.144 vs\. random@720 0\.170,p=0\.64p\{=\}0\.64\): when the verifier is very weak, its selections are uninformative places to settle, so the10×10\\timesmultiplier of §[7](https://arxiv.org/html/2609.09776#S7)is a property of moderately\-competent verifiers, not a universal\.

### 8\.1 From failures to findings: a pre\-registered diagnosis\-and\-repair program

Rather than leave the registered failures as caveats, we treated each as a hypothesis about mechanism, froze numerical predictions for every diagnosis before computing it, and ran the analyses on the raw data\. Four repairs succeeded; two failed and are kept failed\.

Repaired: the exchange rate lives in the copula \(F1\)\.Proposition[2](https://arxiv.org/html/2609.09776#Thmproposition2)resolves both directions of the transfer anomaly at once: RichDSL’s heavy, clumped margins made Pearsonρ\\rhooverstate tail concordance \(realized0\.32<ρp=0\.500\.32<\\rho\_\{p\}\{=\}0\.50\), while the LLM judge’s coarse, saturated scores made it understate massively \(ρp=0\.12\\rho\_\{p\}\{=\}0\.12yet realized 0\.74\)\. Rank\-copula simulation with empirical margins predicts per\-problemSnd​@​32\\mathrm\{Snd\}@32with median error 0\.041 on the real LLM data versus 0\.793 for Pearson \(p=2×10−4p\{=\}2\\times 10^\{\-4\},n=21n\{=\}21\); on RichDSL a residual 0\.137 error remains \(p=0\.37p\{=\}0\.37\)—its verifier errors are feature\-structured beyond any elliptical copula, which is precisely the misspecification settlement exists to correct\.

Repaired: selection is the adversary \(F3\)\.The instructed adversary of RL3a failed its manipulation check, but mining the candidate banks shows that ordinary sampling plus selection*manufactures*deception: choosing the max\-\(judge−\-gold\) candidate from 32 honest samples yields a\+0\.527\+0\.527hacking gap against the weak judge, versus−0\.209\-0\.209for instructed deception \(p=3×10−13p\{=\}3\\times 10^\{\-13\}\), with severe natural hacks \(judge≥0\.8\\geq 0\.8, gold≤0\.2\\leq 0\.2\) on 13% of informative problems\. Two sub\-predictions failed: severe hacks were rarer than predicted, and the strong judge’s maximum gap \(0\.631\) exceeds the weak judge’s—the gap statistic conflates ranking with calibration\. The unification stands: RL1’s soundness decay and reward hacking are the same phenomenon, selection pressure over honest variation; no deceptive generator is required\. The mined max\-gap programs form a natural seed corpus for RSR\-Bench’s adversarial split\.

Repaired, with a warning: calibration is not soundness \(F4\)\.The minimal settlement model—an isotonic judge→\\togold map fit on executed outcomes from half the problems—cuts out\-of\-problem pricing error by 29\.9% \(p=5×10−119p\{=\}5\\times 10^\{\-119\}; registered threshold 30%, missed by 0\.1pp\)\. But a monotone recalibration provably cannot change selection, hence cannot moveSnd​@​N\\mathrm\{Snd\}@N; and because these judges are underconfident on average, recalibration raises scores and*amplifies*the overvalued tail \(mined\-deception gap0\.52→0\.760\.52\\to 0\.76\)\. Deception lives in the residual, not the mean\. This yields the paradigm’s sharpest design constraint:*the settlement model must be at least as expressive as the deception surface*; average\-calibration anchoring is not merely insufficient but tail\-perverse\. The feature\-based head also failed to transfer Snd across problems \(p=0\.55p\{=\}0\.55\), consistent with cross\-problem code verification being the hard regime throughout our suites\.

Bounded: the conditional\-binding conjecture \(F2\)\.Weak\-judge degradation concentrates on hard problems \(hardest tercile 0\.092 vs\. easiest−0\.001\-0\.001;p=0\.054p\{=\}0\.054\), but the strong judge is flat across all of MBPP’s difficulty range—MBPP\-hard is not hard for it\. “The gap binds where task difficulty reaches judge capability” therefore remains a conjecture with directional weak\-judge support only, and it fixes RSR\-Bench’s design brief: difficulty\-stratified, selection\-pressure\-swept, execution\-settled\.

Failed repairs, kept failed \(F5, F6\)\.The competence\-threshold explanation of the on\-policy\-efficiency discrepancy is ruled out: in RichDSL the on\-policy advantage is significantly positive even for a near\-incompetent base verifier \(\+0\.087\+0\.087at 150 labels,p=0\.018p\{=\}0\.018\) and not increasing in competence \(\+0\.096\+0\.096at 600,\+0\.050\+0\.050at 2400\); and the coverage hypothesis is ruled out as well \(F7, predictions frozen before running\): a mixed policy—half on\-policy, half random labels per batch—performs like pure on\-policy \(0\.148 vs\. 0\.147 AUC atS=720S\{=\}720\) and below random \(0\.170\) under the identical protocol\. With competence and coverage both excluded, the leading untested candidate is covariate shift: settled\-selection labels correct pricing in the selected region while degrading global ranking under a cross\-problem verifier—consistent with settlement improving drift but not selection throughout the real suites\. Why on\-policy settlement wins in per\-task worlds and loses for cross\-problem code verifiers is the program’s top open problem\. And on the real\-data hard subset, the hybrid head improved pricing \(p=0\.009p\{=\}0\.009\) but not achieved gold \(p=0\.36p\{=\}0\.36,n=19n\{=\}19\): capability gains from anchoring remain demonstrated only in the synthetic and real\-code CPU suites\.

### 8\.2 Reality\-anchored reward under real policy\-gradient training

The proxies above \(best\-of\-NN, search, iterative prompting\) approximate but do not instantiate the optimization process of modern RLVR\. A fourth pre\-registered suite \(criteria R\-A–R\-E and amendment R\-B′frozen before any run\) closes that gap: GRPO fine\-tuning of Qwen2\.5\-1\.5B\-Instruct \(QLoRA, group size 8, 400 steps, fixed small KL\) on MBPP, under four reward arms identical in everything but the reward signal: \(A\)*frozen*—a settlement RM \(ridge over surface/AST features\) fit once on 1,600 executed base\-model samples, then frozen \(the overoptimization setup of[Gao et al\. \(2023\)](https://arxiv.org/html/2609.09776#bib.bib9)\); \(B\)*anchored*—the identical RM, refit every 25 steps on a settledσ=10%\\sigma\{=\}10\\%of the window’s rollouts \(Algorithm[1](https://arxiv.org/html/2609.09776#alg1), live\); \(C\)*execution*—real test execution as reward \(sound ceiling\); \(D\)*online\-judge*—identical to \(B\) but refit labels come from an LLM judge rather than execution, isolating the label source from online\-ness\. The RM is deliberately minimal—a model organism: arms \(A\), \(B\), \(D\) share an identical model class, so the treatment isolates the settlement update rule itself, and a weak RM makes overoptimization observable at accessible scale\. RM strength is not assumed orthogonal to settlement; their interaction is characterized in §[7](https://arxiv.org/html/2609.09776#S7)\(H2b\), §[8](https://arxiv.org/html/2609.09776#S8)\(RL1b\), and F4\. True executed reward is logged for every rollout in every arm \(as metrics; it trains only arm C\)\.

Table 4:Final\-window \(25\-step\) training outcomes, seed 0\. Gold = executed reward; Peak = best rolling\-window gold; Gap = proxy−\-gold\. The frozen arm’s proxy is the highest and its reality the lowest\.Results\.Table[4](https://arxiv.org/html/2609.09776#S8.T4)and Figure[13](https://arxiv.org/html/2609.09776#S8.F13)report the four matched runs\. The frozen arm traces the full overoptimization curve of[Gao et al\. \(2023\)](https://arxiv.org/html/2609.09776#bib.bib9): proxy reward climbs0\.442→0\.6150\.442\\to 0\.615while executed reward rises to a rolling peak of 0\.617 and then collapses to 0\.063—a 90% destruction of real capability under continued proxy gains—as the policy converges to∼17\\sim\\\!17\-token degenerate completions at KL 1\.35 from base\. The anchored twin ends the same 400 steps at executed reward 0\.397 \(6×\\timesfrozen\), hacking gap\+0\.131\+0\.131vs\.\+0\.552\+0\.552, ordinary∼44\\sim\\\!44\-token completions, and KL 0\.096: each of its 15 refits repriced what the RM had begun to overpay before the policy could commit to it—at roughly one\-tenth of the ceiling arm’s execution budget, while retaining 86% of the ceiling arm’s final executed reward \(0\.397 vs\. 0\.460\)\.

Figure 13:The overoptimization curve with a settlement knob \(seed 0; rolling mean, window 15\)\.Left:executed reward \(solid\) and proxy reward \(dashed\)\. The frozen RM’s proxy climbs while executed reward collapses; the identical RM refit on a 10% settlement stream \(anchored\) tracks the execution ceiling; the equal\-budget judge\-labeled control sits between them\.Right:the hacking gap \(proxy−\-gold\) during training, with the anchored arm’s settled\-drift measurements \(×\\times\)\. Settlement repeatedly closes the gap the frozen arm rides to collapse—but drift magnitude does not rank\-track the gap \(the registered R\-D criterion fails; see text\)\.Reality as the label source \(R\-B′\)\.The online\-judge control isolates the paper’s title claim: identical RM, identical refit cadence, identical 10% budget—only the labels differ \(an LLM judge’s estimates instead of executed outcomes\)\. Online updating alone recovers much of the damage \(0\.288 vs\. frozen’s 0\.063\), but reality\-sourced labels beat judge\-sourced labels by\+0\.109\+0\.109executed reward with half the hacking gap \(\+0\.131\+0\.131vs\.\+0\.241\+0\.241\), and the judge arm partially degenerates anyway \(∼24\\sim\\\!24\-token completions, KL 0\.443\)\. The mechanism is visible in the logs: the judge’s labels erred against execution by 0\.321 on average across refits \(range 0\.18–0\.46\)—the RM was being re\-anchored to a proxy of a proxy\. Online\-ness is worth a lot; reality is worth more, and the difference is the judge’s blindness on\-policy\.

Registered criteria at seed 0—including a failure\.Both R\-A clauses hold \(proxy\+0\.173≥0\.10\+0\.173\\geq 0\.10; final gold0\.063≤0\.063\\leqpeak−0\.03\-0\.03\); both R\-B clauses hold \(anchored gold exceeds frozen by0\.334≥0\.050\.334\\geq 0\.05; smaller gap\); both R\-B′clauses hold; R\-C holds \(0\.397≥0\.8×0\.460=0\.3680\.397\\geq 0\.8\\times 0\.460=0\.368\)\. R\-D*fails*: the settled\-drift statistic does not rank\-predict the concurrent hacking gap \(Spearmanρs=0\.06\\rho\_\{s\}=0\.06over 15 refits, vs\. the registered≥0\.5\\geq 0\.5\), and an exploratory cross\-arm variant \(drift vs\. the frozen\-minus\-anchored gap\) is also null \(ρs=−0\.40\\rho\_\{s\}=\-0\.40,p=0\.14p=0\.14\) with no range\-restriction excuse available \(gap variance is comparable across arms\)\. At this scale and refit cadence, settlement repaired the reward while its drift alarm did not see what it was repairing—the repair effect and the alarm effect are separable, and prediction 4 of §[9\.1](https://arxiv.org/html/2609.09776#S9.SS1)is already under adverse pressure\. We also note the anchored arm’s final gold sits below its own mid\-run peak \(0\.665\); replication seeds run identically under the same registration, and held\-out evaluations \(R\-E\) accompany the full\-suite verdicts\. All runs execute on a single consumer machine \(Apple M1, 16GB\); the canonical 972\-problem split and initial RM were computed once and fixed before any training run\.

## 9 RSR\-Bench: A Reality\-Settled Reasoning Benchmark

Every prior revolution in this field was preceded by the metric that made it legible: ImageNet before deep learning’s coronation\([Deng et al\., 2009](https://arxiv.org/html/2609.09776#bib.bib8)\), scaling\-law perplexity before large pretrained models\([Kaplan et al\., 2020](https://arxiv.org/html/2609.09776#bib.bib17)\), MATH and HumanEval before reasoning RL\([Hendrycks et al\., 2021](https://arxiv.org/html/2609.09776#bib.bib15);[Chen et al\., 2021](https://arxiv.org/html/2609.09776#bib.bib5)\)\. Today the field optimizes judges it knows to be gameable because nothing better exists to climb\. We therefore specify the missing metric\.

###### Definition 1\(Soundness\-under\-Pressure\)\.

For a proxy verifierVV, gold standardGG, and candidate distributionμ\\mu, letxNVx^\{V\}\_\{N\}be the candidate selected byVVfromNNi\.i\.d\. draws ofμ\\mu, andxNGx^\{G\}\_\{N\}the candidate selected byGG\. Then

Snd​@​N=𝔼⁡\[G⁡\(xNV\)\]𝔼⁡\[G⁡\(xNG\)\],\\mathrm\{Snd\}@N\\;=\\;\\frac\{\\mathbb\{E\}\\big\[G\(x^\{V\}\_\{N\}\)\\big\]\}\{\\mathbb\{E\}\\big\[G\(x^\{G\}\_\{N\}\)\\big\]\},and the headline benchmark score is the area underSnd​@​N\\mathrm\{Snd\}@Noverlog⁡N\\log N\.

A sound verifier scores 1 at everyNN; Table[1](https://arxiv.org/html/2609.09776#S6.T1)shows how sharply a shallow verifier departs from it\. On cost:Snd​@​N\\mathrm\{Snd\}@Nis an*evaluation*metric, not a training\-loop requirement, and it amortizes—one pool ofNmaxN\_\{\\max\}candidates, generated and scored once, yields the whole curve by subsampling \(our entire real\-model measurement of two judges on two benchmarks cost∼3\.5×104\\sim\\\!3\.5\\times 10^\{4\}API calls, i\.e\. tens of dollars\)\. Inside training, PCC’s marginal cost over standard RLVR is the settlement rate—the fraction of staked claims actually executed—which Algorithm[1](https://arxiv.org/html/2609.09776#alg1)\(line 10\) adapts to measured drift, and which the label\-efficiency results bound where they hold\. The crucial design property is thatSnd​@​N\\mathrm\{Snd\}@Nmeasures verifiers*under the optimization pressure they will actually face*, which single\-point accuracy does not\.

Table 5:Reward sources by density, soundness, and robustness under optimization pressure\.∼\\sim= partial;†= conjectured, contingent on anchor\-drift control; §[6](https://arxiv.org/html/2609.09776#S6)validates both cells at toy scale and §[10](https://arxiv.org/html/2609.09776#S10)tests them at scale\. Formal kernels are sound and robust but cover only formalizable domains\.Construction recipe\.Assemble tens of thousands of typed claims across science, engineering, and forecasting, each with a known settlement date and mechanically checkable ground truth: time\-sliced scientific claims settled by later replication, performance\-engineering claims settled by execution, forecasts settled by events\([Halawi et al\., 2024](https://arxiv.org/html/2609.09776#bib.bib14)\)\. Freeze corpora at dateTT; settle afterTT\. Score submitted verifiers bySnd​@​N\\mathrm\{Snd\}@Nagainst the settled gold, and score submitted reasoners by settled claim portfolios under proper scoring rules\([Gneiting and Raftery, 2007](https://arxiv.org/html/2609.09776#bib.bib11)\)\. Table[5](https://arxiv.org/html/2609.09776#S9.T5)situates the paradigm this benchmark is designed to measure\.

### 9\.1 What would falsify the paradigm: registered predictions at the next scale

We do not claim to have established a paradigm; paradigm claims are not establishable by their authors\. We claim to have made one*measurable*, and we stake it on numbered predictions that any frontier laboratory can test in days\. Each is stated so that a clean negative result refutes the corresponding component\.

1. 1\.Conditional binding\.For every judge, on tasks in its frontier stratum \(single\-sample accuracy in\[0\.3,0\.7\]\[0\.3,0\.7\]\),Snd​@​N\\mathrm\{Snd\}@Ndeclines by≥0\.10\\geq 0\.10fromN=2N\{=\}2toN=256N\{=\}256\. Evidence so far: confirmed for the weak judge; untestable for the strong judge on MBPP \(no frontier stratum exists there—§[8\.1](https://arxiv.org/html/2609.09776#S8.SS1), F2\)\.*Refuted if*a frontier judge holdsSnd​@​256\\mathrm\{Snd\}@256within 0\.05 ofSnd​@​2\\mathrm\{Snd\}@2on its own frontier stratum\.
2. 2\.Copula law\.For frontier judges on frontier tasks, per\-problem realized soundness lies within±0\.10\\pm 0\.10\(median\) of the rank\-copula prediction of Proposition[2](https://arxiv.org/html/2609.09776#Thmproposition2)\(measured: 0\.041 for the weak judge on MBPP\)\.*Refuted by*systematic departures beyond that band\.
3. 3\.Overoptimization boundary\.Policy\-gradient training against a frozen learned RM diverges \(proxy up, executed reward flat or down\) whenever the RM’s on\-policy soundness is below the policy’s achievable gold, and reality\-anchored refitting at a settlement rate adapted to measured drift removes the divergence at a small fraction of full settlement\. Operationalized at 1\.5B scale in our registration \(criteria R\-A–R\-C\); predicted to persist at every scale at which the precondition holds\.
4. 4\.Drift is a universal alarm\.Wherever divergence occurs, the settled\-drift statistic of Algorithm[1](https://arxiv.org/html/2609.09776#alg1)\(line 10\) rank\-predicts the frozen\-vs\-anchored gap online \(ρs≥0\.5\\rho\_\{s\}\\geq 0\.5; registered as R\-D\)\.*Refuted by*hacking that drift does not see\. First evidence is adverse: the registered seed\-0 test failed \(ρs=0\.06\\rho\_\{s\}\{=\}0\.06; §[8\.2](https://arxiv.org/html/2609.09776#S8.SS2)\)\.
5. 5\.Selection\-manufactured deception\.The maximum hacking gap obtainable by pure best\-of\-NNselection over honest samples grows withNNat the extreme\-value rate implied by the copula, and dominates instructed deception until adversary capability exceeds judge capability \(measured at one point:\+0\.53\+0\.53vs\.−0\.21\-0\.21; §[8\.1](https://arxiv.org/html/2609.09776#S8.SS1), F3\)\.

We commit to reporting confirmations and refutations of these predictions alike; each is stated so that it can be tested without our involvement\.

## 10 Validation Programme at Scale

The full hypothesis is falsifiable through three staged experiments\.

Retrodiction gyms\.Train the claim\-ledger system on time\-sliced corpora—papers, markets, codebases up to dateTT—and score claims against reality afterTT, yielding millions of settled “experiments” at zero laboratory cost\([Halawi et al\., 2024](https://arxiv.org/html/2609.09776#bib.bib14)\)\.*Falsification criterion:*if PCC\-trained reasoning does not beat judge\-rewarded reasoning on retrodictive forecasting and on reproduction of later\-discovered results, the hypothesis fails\.

Closed\-loop empirical domains\.Deploy where reality settles fast and automatically: software performance engineering \(execution is the settler\), robotic manipulation, automated cloud\-lab biology\. Measure whether world\-model\-priced reward beats PRM reward on downstream success*and*on calibration under distribution shift—the metric distinguishing a self\-improving loop from a self\-deceiving one\.

Anchor\-drift audits\.Continuously measure divergence between world\-model settlement and realized settlement \(Algorithm[1](https://arxiv.org/html/2609.09776#alg1), line 10\)\. This scalar is the health metric of the system and, not incidentally, an alignment metric: a system rewarded for calibrated truth\-tracking is structurally disincentivized from deceiving its overseers, because deception manifests as settlement loss\.

## 11 Failure Modes

We flag three honestly\. \(1\) The claim language may be too lossy to carry the best reasoning—the legibility tax, sharpened\. \(2\) Market dynamics may reward safe, vague claims; scoring must pay for resolution as well as calibration\([Gneiting and Raftery, 2007](https://arxiv.org/html/2609.09776#bib.bib11)\)\. \(3\) A system optimizing predicted reality could learn to make reality predictable in undesirable ways; settlement must score prediction of a world the agent does not manipulate\. This is an open, safety\-critical design problem \(see Ethics Statement\)\.

Meta\-reward hacking and the trusted computing base\.Settlement does not eliminate trust; it relocates it\. An agent can attack the settlement substrate itself: sandbox exploits, manipulation of the measured environment, strategic delay of settlement, or staking only easy\-to\-settle claims\. The honest accounting is a trusted computing base \(TCB\): PCC’s TCB is the executor/measurement apparatus plus the settlement scheduler and staking rules—small and auditable, like a proof kernel’s checker, but not zero\. Concrete mitigations: hardened and randomized execution environments, audit\-by\-resettlement of a random claim fraction, scoring rules that price claim selection \(paying for resolution, §[6](https://arxiv.org/html/2609.09776#S6)Result 5\), and settlement\-lag limits\. In our own suites the TCB was subprocess isolation with resource limits; every mined deception was semantic—none attacked the harness—but at higher capability that will not remain true by default, and TCB hardening should be treated as a first\-class component of the paradigm\.

## 12 Conclusion

The verification gap is the binding constraint on the next major leap in language\-model capability\. We have made its cost exact—unsound verification pays a polynomial compute penaltyN1/ρ2N^\{1/\\rho^\{2\}\}—and demonstrated, in the smallest system that can express them, the collapse of learned verifiers under i\.i\.d\. pressure, their capture by adversarial pressure, and the repair mechanism: reality\-anchored settlement, which inverted the adversary’s exploit, scaled soundness log\-linearly with settled labels at over10×10\\timeson\-policy label efficiency, and sharpened claims rather than blunting them\. Proof\-carrying cognition is our conjecture for how this mechanism scales to open\-ended empirical reasoning\. We have not established that conjecture, and no laboratory\-scale study could; what we have done is make it measurable—an exchange\-rate law that survives its own falsification in repaired form, a soundness metric that prices verifiers under the pressure they will actually face, a settlement rule that preserved real reward under live policy\-gradient pressure \(even as its registered drift alarm failed its first test—reported as such\), and five registered predictions \(§[9\.1](https://arxiv.org/html/2609.09776#S9.SS1)\) that any frontier laboratory can confirm or refute\. The reality\-settled benchmark of §[9](https://arxiv.org/html/2609.09776#S9)is the field’s single most important near\-term investment for the same reason ImageNet was: paradigms are not argued into existence, they are climbed into existence—and this one makes truth, rather than persuasion, the thing that wins\.

## Limitations

The experiments in §[3](https://arxiv.org/html/2609.09776#S3)–§[7](https://arxiv.org/html/2609.09776#S7)are synthetic: DSLs of six and ten tokens, ridge/gradient\-boosted/logistic verifiers, and best\-of\-NN, hill\-climbing, evolutionary, and settlement\-aware search are proxies for—not instances of—frontier reasoners, learned reward models, and RL training; a single\-CPU suite cannot test frontier\-scale claims\. The scaled replication \(§[7](https://arxiv.org/html/2609.09776#S7)\) falsified the quantitative transfer of Proposition[1](https://arxiv.org/html/2609.09776#Thmproposition1)outside its Gaussian model class \(it is a ceiling, with realized value≈0\.32\\approx 0\.32at measuredρ≈0\.50\\rho\\approx 0\.50\), showed the closed\-form penaltyN1/ρ2N^\{1/\\rho^\{2\}\}overstates costs at practicalNN, and showed that absolute Goodhart collapse is domain\-dependent: a strong learned verifier kept converting pressure into capability throughN=4096N\{=\}4096, so “sufficient pressure inverts any surface verifier” remains unestablished beyond that range\. Anchoring was tested against a settlement\-aware search adversary and survived, but not against a learning adversary trained end\-to\-end against the settlement process; anchoring also narrows rather than closes the capacity gap to a sound verifier \(0\.28–0\.31 vs\. 0\.59–0\.68 under adversarial pressure\), so verifier expressiveness remains a separate axis, and one registered adversarial cell failed as registered \(steepest ascent; diagnosed, exploratorily, as adversary paralysis\)\. Result 5 and H6 show the training dynamics do not intrinsically favor vague claims, but do not test an agent that strategically selects which claims to stake\. The real\-model suite \(§[8](https://arxiv.org/html/2609.09776#S8)\) covers one model family, two code benchmarks at or below the generator’s capability frontier \(with heavy saturation: 50% of MBPP and 89% of HumanEval problems showed zero gold variance and were excluded by the pre\-specified filter\), anchoring by in\-context learning and a learned reranker rather than RL training, pressure only toN=32N\{=\}32, and a prompt\-level adversary that failed its own manipulation check; its adversarial results bound the threat model rather than the defense\. Two registered criteria across the program \(H2b, RL3c\) were themselves mis\-specified and are disclosed as such\. The single most important untested regime is tasks at the judge’s capability frontier under RL\-scale optimization pressure\. Key unresolved questions for PCC itself include the expressiveness of the claim language relative to latent reasoning, scoring rules that reward resolution without incentivizing vagueness or manipulation, the cost of a versioned world model at training scale, and whether retrodiction transfers to genuinely novel discovery\. The framing of the field’s trajectory reflects the authors’ reading of the 2023–2026 literature and may not represent consensus\.

## Ethics Statement

A system trained to predict reality could act to make reality more predictable in harmful ways; settlement design must score prediction of unmanipulated outcomes, and we identify this as a safety\-critical open problem rather than a solved one\. Conversely, the paradigm has a favorable alignment property: reward for calibrated truth\-tracking structurally penalizes deception of overseers, and the anchor\-drift scalar is a deployable oversight signal\. Reality\-settled benchmarks in sensitive domains \(e\.g\., biology\) must be curated to avoid creating dual\-use optimization targets\. No human subjects or private data are involved\.

## References

- AlphaProof and AlphaGeometry teams, Google DeepMind \(2024\)AlphaProof and AlphaGeometry teams, Google DeepMind\.AI achieves silver\-medal standard solving International Mathematical Olympiad problems\.DeepMind Blog, 2024\.
- Amodei et al\. \(2016\)Dario Amodei, Chris Olah, Jacob Steinhardt, Paul Christiano, John Schulman, and Dan Mané\.Concrete problems in AI safety\.*arXiv preprint arXiv:1606\.06565*, 2016\.
- Austin et al\. \(2021\)Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, et al\.Program synthesis with large language models\.*arXiv preprint arXiv:2108\.07732*, 2021\.
- Bowman et al\. \(2022\)Samuel R\. Bowman, Jeeyoon Hyun, Ethan Perez, Edwin Chen, Craig Pettit, Scott Heiner, Kamilė Lukošiūtė, Amanda Askell, Andy Jones, Anna Chen, et al\.Measuring progress on scalable oversight for large language models\.*arXiv preprint arXiv:2211\.03540*, 2022\.
- Chen et al\. \(2021\)Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al\.Evaluating large language models trained on code\.*arXiv preprint arXiv:2107\.03374*, 2021\.
- Christiano et al\. \(2017\)Paul F\. Christiano, Jan Leike, Tom Brown, Miljan Martic, Shane Legg, and Dario Amodei\.Deep reinforcement learning from human preferences\.In*Advances in Neural Information Processing Systems*, volume 30, 2017\.
- Cobbe et al\. \(2021\)Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman\.Training verifiers to solve math word problems\.*arXiv preprint arXiv:2110\.14168*, 2021\.
- Deng et al\. \(2009\)Jia Deng, Wei Dong, Richard Socher, Li\-Jia Li, Kai Li, and Li Fei\-Fei\.ImageNet: A large\-scale hierarchical image database\.In*IEEE Conference on Computer Vision and Pattern Recognition*, 2009\.
- Gao et al\. \(2023\)Leo Gao, John Schulman, and Jacob Hilton\.Scaling laws for reward model overoptimization\.In*International Conference on Machine Learning*, 2023\.
- Garrabrant et al\. \(2016\)Scott Garrabrant, Tsvi Benson\-Tilsen, Andrew Critch, Nate Soares, and Jessica Taylor\.Logical induction\.*arXiv preprint arXiv:1609\.03543*, 2016\.
- Gneiting and Raftery \(2007\)Tilmann Gneiting and Adrian E\. Raftery\.Strictly proper scoring rules, prediction, and estimation\.*Journal of the American Statistical Association*, 102\(477\):359–378, 2007\.
- Guo et al\. \(2025\)Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al\.DeepSeek\-R1: Incentivizing reasoning capability in LLMs via reinforcement learning\.*arXiv preprint arXiv:2501\.12948*, 2025\.
- Ha and Schmidhuber \(2018\)David Ha and Jürgen Schmidhuber\.Recurrent world models facilitate policy evolution\.In*Advances in Neural Information Processing Systems*, volume 31, 2018\.
- Halawi et al\. \(2024\)Danny Halawi, Fred Zhang, Chen Yueh\-Han, and Jacob Steinhardt\.Approaching human\-level forecasting with language models\.*arXiv preprint arXiv:2402\.18563*, 2024\.
- Hendrycks et al\. \(2021\)Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt\.Measuring mathematical problem solving with the MATH dataset\.In*NeurIPS Datasets and Benchmarks Track*, 2021\.
- Irving et al\. \(2018\)Geoffrey Irving, Paul Christiano, and Dario Amodei\.AI safety via debate\.*arXiv preprint arXiv:1805\.00899*, 2018\.
- Kaplan et al\. \(2020\)Jared Kaplan, Sam McCandlish, Tom Henighan, Tom B\. Brown, Benjamin Chess, Rewon Child, Scott Gray, Alec Radford, Jeffrey Wu, and Dario Amodei\.Scaling laws for neural language models\.*arXiv preprint arXiv:2001\.08361*, 2020\.
- Kirchner et al\. \(2024\)Jan Hendrik Kirchner, Yining Chen, Harri Edwards, Jan Leike, Nat McAleese, and Yuri Burda\.Prover\-verifier games improve legibility of LLM outputs\.*arXiv preprint arXiv:2407\.13692*, 2024\.
- LeCun \(2022\)Yann LeCun\.A path towards autonomous machine intelligence\.OpenReview preprint, 2022\.
- Leike et al\. \(2018\)Jan Leike, David Krueger, Tom Everitt, Miljan Martic, Vishal Maini, and Shane Legg\.Scalable agent alignment via reward modeling: a research direction\.*arXiv preprint arXiv:1811\.07871*, 2018\.
- Lightman et al\. \(2024\)Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe\.Let’s verify step by step\.In*International Conference on Learning Representations*, 2024\.
- OpenAI \(2024\)OpenAI\.Learning to reason with LLMs\.OpenAI Blog, 2024\.
- Ouyang et al\. \(2022\)Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, et al\.Training language models to follow instructions with human feedback\.In*Advances in Neural Information Processing Systems*, volume 35, 2022\.
- Rumelhart et al\. \(1986\)David E\. Rumelhart, Geoffrey E\. Hinton, and Ronald J\. Williams\.Learning representations by back\-propagating errors\.*Nature*, 323\(6088\):533–536, 1986\.
- Savage \(1971\)Leonard J\. Savage\.Elicitation of personal probabilities and expectations\.*Journal of the American Statistical Association*, 66\(336\):783–801, 1971\.
- Silver et al\. \(2017\)David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al\.Mastering the game of Go without human knowledge\.*Nature*, 550\(7676\):354–359, 2017\.
- Snell et al\. \(2024\)Charlie Snell, Jaehoon Lee, Kelvin Xu, and Aviral Kumar\.Scaling LLM test\-time compute optimally can be more effective than scaling model parameters\.*arXiv preprint arXiv:2408\.03314*, 2024\.
- Strathern \(1997\)Marilyn Strathern\.‘improving ratings’: audit in the British university system\.*European Review*, 5\(3\):305–321, 1997\.
- Sutton \(2019\)Richard S\. Sutton\.The bitter lesson\.Incomplete Ideas \(blog\), 2019\.
- Trinh et al\. \(2024\)Trieu H\. Trinh, Yuhuai Wu, Quoc V\. Le, He He, and Thang Luong\.Solving olympiad geometry without human demonstrations\.*Nature*, 625\(7995\):476–482, 2024\.
- Uesato et al\. \(2022\)Jonathan Uesato, Nate Kushman, Ramana Kumar, Francis Song, Noah Siegel, Lisa Wang, Antonia Creswell, Geoffrey Irving, and Irina Higgins\.Solving math word problems with process\- and outcome\-based feedback\.*arXiv preprint arXiv:2211\.14275*, 2022\.
- Vaswani et al\. \(2017\)Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N\. Gomez, Lukasz Kaiser, and Illia Polosukhin\.Attention is all you need\.In*Advances in Neural Information Processing Systems*, volume 30, 2017\.
- Wei et al\. \(2022\)Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed Chi, Quoc V\. Le, and Denny Zhou\.Chain\-of\-thought prompting elicits reasoning in large language models\.In*Advances in Neural Information Processing Systems*, volume 35, 2022\.
- Wu et al\. \(2022\)Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N\. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy\.Autoformalization with large language models\.In*Advances in Neural Information Processing Systems*, volume 35, 2022\.
- Zelikman et al\. \(2022\)Eric Zelikman, Yuhuai Wu, Jesse Mu, and Noah Goodman\.STaR: Bootstrapping reasoning with reasoning\.In*Advances in Neural Information Processing Systems*, volume 35, 2022\.

## Appendix AExperimental Details

The DSL world\.Programs are strings of length 1–6 over six tokens acting on an integer register initialized to the inputxx:A\(v\+1v\{\+\}1\),S\(v−1v\{\-\}1\),D\(v×2v\{\\times\}2\),T\(v×3v\{\\times\}3\),N\(−v\-v\),Q\(v2v^\{2\}\), with executions aborted if\|v\|\>106\|v\|\>10^\{6\}\. A task is drawn by sampling a hidden target program of length 4 whose outputs on the evaluation inputsx∈\{−3,…,4\}x\\in\\\{\-3,\\dots,4\\\}are all defined and take more than two distinct values\. Gold reward of a candidate is the fraction of the eight input–output pairs it matches under execution\. Random programs average gold reward 0\.079; multiple functionally equivalent solutions typically exist\.

Verifiers\.The learned verifier is ridge regression \(α=1\\alpha\{=\}1\) over 43 features: 6 token counts, 36 bigram counts, and length—a deliberately shallow judge evaluating the surface of a program rather than executing it\. Experiment 6 uses logistic regression \(C=1C\{=\}1, predictions clipped to\[0\.001,0\.999\]\[0\.001,0\.999\]; a clipped constant predictor when training labels are degenerate\)\.

Experiment 1\.20,000 trials per\(ρ,N\)\(\\rho,N\)point;N∈\{20,…,212\}N\\in\\\{2^\{0\},\\dots,2^\{12\}\\\};ρ∈\{0\.2,0\.5,0\.8,1\.0\}\\rho\\in\\\{0\.2,0\.5,0\.8,1\.0\\\}\. Theory lines use Monte\-Carlo𝔼⁡\[maxN\]\\mathbb\{E\}\[\\max\_\{N\}\]\(2×1052\\times 10^\{5\}trials\), not the asymptotic formula\.

Experiment 2\.60 tasks; learned verifier trained on 1,000 labeled random programs per task; candidate pools of 2,048 fresh programs;N∈\{20,…,211\}N\\in\\\{2^\{0\},\\dots,2^\{11\}\\\}subsampled without replacement per point\.

Experiment 3\.60 tasks, 10 rounds; pool 512, settle top 32 by proxy per round; anchored condition appends settled labels and refits, frozen does not; both start from 300 base labels\.

Experiment 4\.40 tasks, 250 steps of steepest\-ascent search: 16 mutations \(substitute/insert/delete a token\) per step, moving to the best\-scoring candidate when it does not decrease the score\. Anchored condition settles up to 25 recently visited programs every 25 steps \(250 reality queries per run\) and refits\. The sound condition scores candidates by execution directly\.

Experiment 5\.40 tasks; base verifier trained on 500 random labels; budgetsS∈\{0,50,150,500,1500\}S\\in\\\{0,50,150,500,1500\\\}\. On\-policy acquisition alternates pools of 256, settling the top 16 by the current verifier and refitting; the random condition addsSSlabels of random programs at once\. Soundness AUC is the mean ofSnd​@​N\\mathrm\{Snd\}@NoverN∈\{20,…,211\}N\\in\\\{2^\{0\},\\dots,2^\{11\}\\\}on a fresh pool of 2,048\.

Experiment 6\.60 tasks, 12 rounds; claim event “gold reward≥0\.25\\geq 0\.25”; pools of 256 per round, mixed acquisition \(16 top\-probability \+ 16 random\), 32 claims settled per round \(1,920 per round pooled across tasks\); 200 initial random labels per task\. Brier decomposition uses 10 equal\-width probability bins; reliability and resolution are computed on each round’s settled claims*before*that round’s refit, so every point is out\-of\-sample\.

Compute and seeds\.All experiments complete in under ten minutes total on a single CPU\. Seeds: 0–4 \(suite 1\), 10–12 \(suite 2\), fixed in the scripts\.

## Appendix BScaled Replication Details

RichDSL\.Programs of length 1–10 over ten tokens acting on an integer registervvinitialized to inputxx:A\(v\+1v\{\+\}1\),S\(v−1v\{\-\}1\),D\(v×2v\{\\times\}2\),T\(v×3v\{\\times\}3\),H\(v​div​2v\\ \\mathrm\{div\}\\ 2, truncating\),N\(−v\-v\),Q\(v2v^\{2\}\),P\(v\+xv\{\+\}x\),M\(vmod7v\\bmod 7\),G\(max⁡\(v,0\)\\max\(v,0\)\)\. Values with\|v\|\>109\|v\|\>10^\{9\}become invalid \(scored as mismatch\)\. Inputsx∈\{−8,…,7\}x\\in\\\{\-8,\\dots,7\\\}; targets are length\-6 programs valid on all inputs with more than three distinct outputs\. Random programs average gold reward 0\.018\. Statistical unit is the task; tests are paired two\-sided Wilcoxon signed\-rank unless a direction was pre\-registered; intervals are 95% bootstrap CIs\.

Verifiers\.Weak: ridge \(α=1\\alpha\{=\}1\) on 111 features \(unigrams, bigrams, length\)\. Strong: gradient\-boosted trees \(HistGradientBoostingRegressor, 100 iterations; 60 in the H3 loop\) on 359 features \(adding positional token indicators, 128 hashed trigrams, first/last one\-hots\)\. Both trained on 2,000 labeled random programs per task \(600 base labels in the loop experiments\)\.

H1\.Gaussian simulation: 100,000 trials per point,N∈\{20,…,214\}N\\in\\\{2^\{0\},\\dots,2^\{14\}\\\},ρ∈\{0\.1,0\.3,0\.5,0\.7,0\.9,1\.0\}\\rho\\in\\\{0\.1,0\.3,0\.5,0\.7,0\.9,1\.0\\\}; the penalty sweep uses 20,000 trials toN=217N\{=\}2^\{17\}\. Transfer \(H1c\): per\-task Pearsonρ⁡\(proxy,gold\)\\rho\(\\text\{proxy\},\\text\{gold\}\)on fresh pools of 4,096 vs\. realizedSnd​@​4096\\mathrm\{Snd\}@4096, 120 tasks\.

H2\.120 tasks; pools of 4,096;N∈\{20,…,212\}N\\in\\\{2^\{0\},\\dots,2^\{12\}\\\}, eight subsample repetitions per point\.

H3\.12 rounds; pool 1,024/round; settle the top 32 by proxy; anchored refits on all settled labels; 120 tasks \(weak\), 60 \(strong\)\.

H4\.300 steps, 24 mutations \(substitute/insert/delete\) per step, 100 tasks; anchored settlement of the 25 most recent unique visited programs every 25 steps \(300 reality queries/run\)\. Steepest ascent moves to the best mutation when not worse; the evolutionary adversary keeps the top 16 of population\-plus\-children; the settlement\-aware adversary detects refits \(score drop without moving\) and restarts at the proxy\-best of 64 random probes filtered to the 32 most edit\-distant from all settled programs\. Its population \(evolutionary\) or the anchored model’s scores are recomputed after refits; the steepest climber’s stale incumbent score is the registered\-failure artifact discussed in §[7](https://arxiv.org/html/2609.09776#S7)\.

H5\.BudgetsS∈\{0,100,300,1000,3000\}S\\in\\\{0,100,300,1000,3000\\\}in batches of 20; on\-policy settles the top 20 by the current verifier from pools of 512; uncertainty sampling scores pool variance under a 3\-member bootstrap\-ridge committee; Soundness AUC is the mean ofSnd​@​N\\mathrm\{Snd\}@NoverN∈\{20,…,212\}N\\in\\\{2^\{0\},\\dots,2^\{12\}\\\}on fresh pools of 4,096; 80 tasks\.

H6\.Claim event “gold≥0\.125\\geq 0\.125” \(base rate≈0\.19\\approx 0\.19; a pre\-run, documented amendment from the minimal suite’s 0\.25, whose base rate≈0\.05\\approx 0\.05in RichDSL is too degenerate for 10\-bin decomposition\); 15 rounds; pools of 256; 16 top\-probability \+ 16 random claims settled per round; decomposition computed out\-of\-sample before each refit; 100 tasks\.

Compute and seeds\.∼75\\sim\\\!75minutes on a single CPU\. Tasks are independently seeded by index \(bases 20,000 / 50,000 / 60,000 / 70,000 / 90,000 / 110,000\), so chunked and monolithic invocations produce identical results\.