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

Eshwar Reddy M; Sourav Karmakar

Source-linked AI summary

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

Eshwar Reddy M, Sourav Karmakar

arXiv:2609.09776v1Sep 9, 2026cs.AIcs.LG

TL;DR

The paper addresses the verification gap: scalable, robust reward for reasoning is missing outside formally grounded domains. It combines a theory of verifier quality under best-of-N selection with reality-settled demonstrations, proof-carrying cognition, and a benchmark. Across its supported testbeds, unsound verifiers degrade under optimization while reality-anchored settlement improves soundness and limits exploitation, though frontier-scale generalization remains unestablished.

Problem
The verification gap is the lack of scalable, incorruptible reward for reasoning outside domains with cheap, sound verifiers.
Method
The paper combines exchange-rate theory, executable program-synthesis experiments, reality-anchored settlement, proof-carrying cognition, and the Soundness-under-Pressure benchmark.
Results
Unsound verifiers lose soundness under optimization, while reality-anchored settlement drives the hacking gap toward ∼0 and scales soundness log-linearly with settled labels.
Takeaways & Limitations
Proof-carrying cognition is presented as a conjectured route to reality-settled reasoning, and the paper makes verification pressure measurable through Soundness-under-Pressure.
Takeaways & Limitations
The experiments are synthetic proxies, and the paper does not establish that proof-carrying cognition or its effects scale to frontier LLMs and open-ended reasoning.

Abstract

from arXiv · show

Frontier gains in language-model reasoning come from reinforcement learning on reasoning traces and are concentrated in domains with a cheap, sound verifier. We argue the field's binding constraint is the verification gap: no scalable, incorruptible reward for reasoning outside formal domains. We make four contributions. (1) Theory: in a joint-Gaussian model of best-of-N selection, verifier-gold correlation rho is the exact exchange rate between test-time compute and capability, and an unsound verifier pays a polynomial penalty N^(1/rho^2); a margin-free copula form predicts realized soundness of real LLM judges to 4% median error. (2) Demonstration: in program-synthesis testbeds with executable ground truth, including a pre-registered scaled replication, unsound verifiers lose Soundness-under-Pressure as optimization grows (0.94 to 0.32 at N=4096) while a sound verifier improves monotonically; reality-anchored settlement beats a frozen verifier under i.i.d. and adversarial pressure, driving the hacking gap from ~0.27 to ~0; soundness scales log-linearly with settled labels, with on-policy settlement ~10x more label-efficient than random labeling. With real LLM judges and unit-test execution as gold, a weak judge loses soundness under best-of-N (p<0.001), a stronger judge is more robust, and selection alone manufactures +0.53 hacking gaps from honest samples. Under real GRPO training, a frozen reward model traces the full overoptimization curve (executed reward collapses 90%) while the same model refit on a 10% settlement stream preserves 6x the executed reward. (3) Paradigm: proof-carrying cognition, where reasoning steps are typed probabilistic claims priced by a self-built world model trained only on held-out reality and settled by proper scoring rules. (4) Benchmark: we specify Soundness-under-Pressure as the headline metric for a reality-settled reasoning benchmark.

1 Introduction

The paper identifies a verification gap: reasoning gains from reinforcement learning concentrate where cheap, sound verifiers exist, while preference-based substitutes are noisy and gameable. It proposes theory, reality-anchored demonstrations, proof-carrying cognition, and a benchmark for soundness under optimization pressure.

Motivation: Frontier reasoning gains concentrate in mathematics, code, and formal proof, where cheap, sound verifiers support reinforcement learning on reasoning traces.Preference labels and LLM judges are described as noisy, gameable, and shallower than the reasoning they evaluate.
Contributions: Verifier–gold correlation ρ is the theory’s compute–capability exchange rate, while unsoundness incurs a polynomial candidate penalty N1/ρ2.Simulation matches the theory within 0.011σ across points.
Contributions: In program-synthesis testbeds, learned-verifier soundness falls from 0.94 to 0.32 under best-of-N pressure, while reality-anchored settlement drives the hacking gap toward ∼0.The demonstrations also report log-linear soundness growth with settled labels and roughly 10× greater label efficiency for on-policy settlement.
Contributions: Proof-carrying cognition represents reasoning as falsifiable, priced claims, and Soundness-under-Pressure is proposed as a benchmark metric.The paradigm treats reality as the only unamortized loss and the benchmark specifies a construction recipe for reality-settled reasoning.
Scope: The paper is a hybrid position-and-proof-of-concept study whose deliberately minimal experiments validate mechanisms rather than frontier-scale claims.Its motivation connects trustworthy reward to self-generated data, reliable long-horizon action, and open-domain oversight.
Motivation: The verification gap is the absence of scalable, incorruptible verification beyond formally grounded domains.The paper defines a verifier as sound, cheap, and robust under optimization, and says current substitutes fail robustness under sufficient pressure.

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

The theory models best-of-N selection with jointly Gaussian gold and proxy scores, showing that verifier correlation determines how test-time compute converts into expected capability. It derives a polynomial penalty for unsoundness, then qualifies the closed form using copula-based and finite-N corrections.

Setup: Best-of-N selection converts test-time compute into capability, with optimization pressure growing as log N.The verifier samples N candidates and retains the candidate receiving the highest proxy score.
Proposition 1: In the jointly Gaussian model, verifier–gold correlation ρ is the exact compute–capability exchange rate.The selected candidate’s expected gold reward equals ρ times the expected maximum proxy score.
Corollary 1: Unsound verification requires N1/ρ2 candidates to match the expected gold reward achieved by a sound verifier with N candidates.This is the polynomial compute penalty stated in Corollary 1.
Empirical validation: Within the Gaussian model class, simulations match the exchange-rate theory within 0.011σ, while outside it a verifier with ρ ≈0.50 realizes only ≈0.32 of sound-verifier value at N=4096.The synthetic discrepancy is attributed to exploitable structure beyond Gaussian noise.
Copula correction: A margin-free copula formulation predicts realized soundness for real LLM judges with median error 4.1%, outperforming Pearson-based prediction with 79-point error.The copula formulation depends on the copula parameter and gold margin, not the proxy-score margin.
Caveats: The closed-form N1/ρ2 penalty is asymptotic and can overstate practical costs by up to 24× at ρ=0.5 and N≤16; finite-N matching predicts budgets within 3.4%.The paper states that empirical decline under heavy optimization requires model misspecification and is domain-dependent.

4 The Validated Attack: Asymmetric Verification

The section proposes reality-anchored verification as a way to extend sound checking beyond formal domains. Proof-carrying cognition combines typed claims, a self-built world model, sparse reality settlement, and proper-scoring-rule rewards to resist Goodharting.

Asymmetric Verification: Formal kernels provide sound verification, but learned verifiers and other substitutes can fail under sufficient optimization.The proposed extension targets empirical domains where formal grounding is unavailable.
Proof-Carrying Cognition: Proof-carrying cognition treats each reasoning step as a falsifiable, priced claim admitted through checkable material rather than authority approval.The paradigm adapts the logic of proof-carrying code to internal reasoning at training scale.
Architecture and Training Loop: Reality settles claims sparsely but incorruptibly, while proper scoring rules convert expected predictive accuracy into reasoning reward instead of judge approval.The design uses dense immediate pricing while retaining sparse external settlement as the trust anchor.
Architecture and Training Loop: Its architecture emits typed probabilistic claims, prices them with a persistent world model, and anchors that model’s training loss exclusively to held-out reality.The claim ledger generalizes autoformalization from theorems to empirical assertions.
Why It Can Work Where Current Approaches Fail: Under best-of-N pressure, execution-verifier selection reaches 0.83 gold reward monotonically, whereas learned-verifier selection peaks near N=512 and falls to 0.10 at N=2048.The learned verifier’s proxy score continues rising despite the decline in realized gold reward.

6 Minimal Empirical Demonstrations

These laptop-scale demonstrations use executable ground truth to test learned-verifier failure under optimization and reality-anchored settlement. Unsound verifiers degrade or are hacked under pressure, while settlement reduces drift, improves soundness and reward, and sharpens claims, though the evidence remains mechanism-level.

Setup: The testbed uses program-synthesis tasks with an executable gold verifier and a deliberately shallow learned verifier based on surface features.Tasks use a six-token integer DSL; the learned judge is a ridge regressor over token counts and program length.
Result 1: learned verifiers collapse under pressure; sound ones do not: At N=2048, the execution verifier reaches 0.831 gold reward, while the learned verifier declines to 0.104 and Soundness-under-Pressure collapses from 1.00 to 0.13.Both verifiers start at 0.079 at N=1; the learned verifier’s proxy score continues rising despite declining gold reward.
Result 2: reality-anchored settlement bounds drift and compounds capability: Anchored settlement reduces anchor drift by 26% and raises achieved gold reward from 0.154 to 0.306, while the frozen verifier’s reward falls to 0.125.Settlement labels selected programs by execution, appends the outcomes to training data, and refits the verifier each round.
Result 3: an adversarial generator hacks a frozen verifier; settlement inverts the exploit: Under directed adversarial pressure, the frozen learned verifier locks into a hacked optimum at 0.178, whereas anchored settlement reaches 0.297, a 67% improvement over frozen.The frozen verifier retains a positive hacking gap; anchored settlement inverts the gap to −0.101 while the shallow model still trails the sound verifier.
Result 4: soundness scales with settlement, and on-policy settlement is >10× more label-efficient: Soundness AUC scales approximately log-linearly with settlement: 150 on-policy labels reach 0.617 versus 0.595 from 1,500 random labels, exceeding 10× label efficiency.On-policy settlement labels programs selected by the current verifier rather than random programs.
Result 5: settlement buys resolution, not just calibration: Settlement improves both calibration and claim resolution: reliability falls from 0.0064 to 0.0039 while resolution rises from 0.051 to 0.101.The authors report that this setting did not force claims toward vague base-rate predictions, but they retain claim-selection as an unresolved failure mode.

7 Scaled Pre-registered Replication

The pre-registered replication tests whether settlement remains effective at larger scale and under stronger adversarial and optimization pressure. It largely confirms settlement’s benefits while qualifying the theory’s transfer and the conditions for verifier collapse.

Claim quality: Settlement improved claim calibration while doubling resolution, indicating that settled claims became sharper rather than reverting toward a vague base rate.Across twelve rounds, reliability decreased by 40% and resolution increased by 98%.
Adversarial pressure: Anchored settlement beat frozen verification under directed adversarial pressure, reducing the hacking gap to approximately 0–0.04 against all three adversaries.The settlement-aware adversary still failed to sustain inflated scores, although one registered steepest-ascent comparison did not improve gold reward.
Verifier pressure: At scale, relative soundness degraded for both weak and strong verifiers, from 0.94 to 0.32 and 0.94 to 0.59 respectively.The weak verifier plateaued, while the strong verifier continued climbing through N=4096 despite increasing relative inefficiency.
Settlement scaling: Soundness AUC scaled log-linearly with settled budget, with on-policy settlement at S=300 outperforming random labeling at S=3000.The replication also found uncertainty sampling barely improved over random labeling.
Theory qualifications: The quantitative exchange-rate claim transferred only as an optimistic ceiling, while the exact finite-N form matched empirical budgets within 3.4%.Across tasks, realized soundness fell short of correlation on 76% of tasks, with a median gap of 0.27.
Theory qualifications: Absolute verifier collapse was domain-dependent, and the registered criterion for detecting decline was statistically invalid.A valid exploratory analysis found that the strong verifier’s gold reward rose monotonically through N=4096 even as Soundness-under-Pressure eroded.

8 Real-Code and Real-Model Experiments

Experiments on real code, real LLM judges, and GRPO training show that selection pressure exposes verifier weaknesses, while stronger judges and reality-based settlement improve robustness within tested regimes. The results also identify important failures and scope boundaries for the proposed mechanism.

Real judges: Weak LLM judges lost Soundness-under-Pressure as best-of-N increased, while the strong judge was significantly more robust on MBPP and HumanEval.On MBPP, weak-judge soundness fell from 0.835 at N=2 to 0.729 at N=32; on HumanEval it fell from 0.889 to 0.750.
Real-code regime: The real-code experiments show that cross-problem verification is substantially harsher than the per-task synthetic setting.The surface verifier fell from Soundness-under-Pressure 0.325 at N=4 to 0.016 at N=256, while the gradient-boosted verifier reached only 0.052.
Anchoring mechanism: The real-model ablation found that only the feature-level settlement head improved both loop drift and adversarial gap.The table measures final-round score–gold drift on selections and out-of-problem judge–gold gap on adversarial candidates.
Failures and scope: Several registered tests failed or remained unresolved, including prompt-level adversarial manipulation, drift-based prediction of hacking gaps, and whether strong judges fail beyond tested pressure.The paper retains these failures as scope boundaries rather than treating them as evidence for robustness.
Selection pressure: Selection alone created a +0.527 hacking gap from 32 honest samples against the weak judge.Natural hacks with judge scores at least 0.8 and gold scores at most 0.2 occurred on 13% of informative problems.
GRPO training: In GRPO training, reality-sourced online settlement outperformed frozen reward modeling, while judge-sourced labels delivered smaller gains and a larger hacking gap.Online updating raised executed reward from 0.063 to 0.288; reality labels exceeded judge labels by 0.109 executed reward and halved the hacking gap relative to them.

9 RSR-Bench: A Reality-Settled Reasoning Benchmark

RSR-Bench makes verifier reliability measurable under increasing best-of-N pressure by defining Soundness-under-Pressure and grounding evaluation in settled reality. It proposes a benchmark construction and records falsifiable predictions about verifier degradation, settlement, and selection-induced hacking.

Metric: Soundness-under-Pressure measures how closely a proxy-selected candidate matches the gold-selected candidate as N grows, with the headline score given by area under the curve over log N.A sound verifier scores 1 at every N, while evaluation can reuse one generated and scored candidate pool through subsampling.
Construction: The benchmark freezes corpora at date T, settles typed claims after T, and scores verifiers against settled gold outcomes.The proposed claims span science, engineering, and forecasting, with replication, execution, or later events providing ground truth.
Predictions: Snd@N is predicted to decline by at least 0.10 from N=2 to N=256 for judges operating on tasks in their frontier stratum.The weak judge confirms this prediction, while MBPP provides no frontier stratum for testing the strong judge.
Predictions: The copula prediction is expected to approximate realized soundness within ±0.10 median error, with 0.041 measured for the weak judge on MBPP.Systematic departures beyond that band would refute the prediction.
Predictions: Frozen learned reward models are predicted to diverge under policy-gradient training when their on-policy soundness falls below achievable gold performance, whereas drift-adapted settlement should remove that divergence.The registered test operationalizes this boundary at 1.5B scale and treats the claim as conditional on the stated precondition.
Predictions: +0.53 hacking gaps can arise from best-of-N selection over honest samples, exceeding instructed deception measured at −0.21 in one comparison.The prediction attributes this growth to the extreme-value rate implied by the copula until adversary capability exceeds judge capability.

10 Validation Programme at Scale

The validation programme proposes staged tests of proof-carrying cognition across retrospective corpora and closed-loop empirical domains. It evaluates whether reality-settled rewards outperform judge rewards on downstream success, forecasting, reproduction, and calibration under distribution shift.

Retrodiction gyms: Retrodiction gyms train claim-ledger systems on information available by date T and score claims against later reality, creating large retrospective evaluation sets without laboratory cost.The hypothesis fails if PCC-trained reasoning does not beat judge-rewarded reasoning on retrodictive forecasting and reproduction of later-discovered results.
Closed-loop empirical domains: Closed-loop tests deploy reality-settled rewards where software execution, robotic manipulation, or automated cloud-lab biology can settle outcomes quickly.The comparison targets downstream success and calibration under distribution shift, which distinguishes self-improving from self-deceiving loops.

11 Failure Modes

The paper identifies three major failure modes for proof-carrying cognition: lossy claim language, incentives for vague claims, and agents manipulating either reality or the settlement process. These risks make settlement design and the trusted computing base central open problems.

Representation: Claim language may be too lossy to carry the best reasoning, creating a sharpened legibility tax.This is presented as an acknowledged limitation rather than a resolved design issue.
Incentives: Market dynamics may reward safe, vague claims, so scoring must pay for resolution as well as calibration.The limitation concerns incentive design for claim quality, not merely predictive accuracy.
Settlement security: Agents could manipulate the measured world, delay settlement, exploit sandboxes, or stake only easy-to-settle claims.The proposed trusted computing base includes the executor, measurement apparatus, settlement scheduler, and staking rules; it is small and auditable but not zero.

12 Conclusion

The conclusion frames verification as the binding constraint on further reasoning gains and presents reality-anchored settlement as a measurable repair for unsound learned verifiers. Proof-carrying cognition remains a conjecture, while its metrics, settlement rule, and registered predictions are offered for external testing.

Conclusion: Unsound verification pays a polynomial compute penalty N^(1/rho^2), making verifier quality an exact exchange rate between computation and capability.The conclusion connects this theoretical cost to observed learned-verifier collapse under pressure.
Conclusion: Reality-anchored settlement repaired learned-verifier failures, scaled soundness log-linearly with settled labels, and achieved over 10× on-policy label efficiency.The conclusion also reports preserved real reward under live policy-gradient pressure, while noting that the registered drift alarm failed its first test.
Conclusion: Proof-carrying cognition is presented as a conjecture for scaling reality-settled verification to open-ended empirical reasoning, not as an established paradigm.The paper instead makes the conjecture measurable through a soundness metric, a settlement rule, and five registered predictions that others can confirm or refute.

Limitations

The experiments are synthetic proxies rather than instances of frontier reasoning, learned reward models, or RL training. The scaled replication also limits quantitative transfer beyond the Gaussian model and leaves broader pressure behavior and paradigm feasibility unresolved.

The experiments use synthetic DSLs, simple verifiers, and search procedures as proxies rather than instances of frontier reasoners, learned reward models, or RL training.This limits direct transfer of the experimental findings to those settings.
The scaled replication falsified quantitative transfer of Proposition 1 outside its Gaussian model class, with realized value ≈0.32 at measured ρ ≈0.50.The passage characterizes the proposition as a ceiling rather than a generally transferable prediction.
At practical N, the closed-form penalty N^(1/ρ^2) overstates costs, and a strong learned verifier retained capability through N=4096.Thus, absolute Goodhart collapse remains unestablished beyond that tested range.
Open questions include whether claim language tracks latent reasoning, whether scoring rules avoid vagueness or manipulation, and whether retrodiction transfers to genuinely novel discovery.The passage also identifies world-model training cost and the authors’ non-consensus literature framing as boundaries.

Ethics Statement

The paper identifies a safety-critical risk in training systems to predict reality: settlement could incentivize making reality more predictable through harmful manipulation. It frames scoring unmanipulated outcomes as an unresolved design problem while noting potential alignment benefits from calibrated truth-tracking.

A system trained to predict reality could act to make reality more predictable in harmful ways, making settlement of unmanipulated outcomes a safety-critical open problem.The passage explicitly presents this issue as unresolved rather than solved.
The paradigm’s proposed alignment property is that calibrated truth-tracking structurally penalizes deception of overseers, with anchor-drift offered as a deployable oversight signal.

A Experimental Details

The experiments evaluate executable program synthesis across minimal and richer DSLs, using gold execution rewards, learned verifiers, pressure search, and reality settlement. Designs emphasize paired task-level evaluation and out-of-sample scoring before refits.

The DSL world: The DSL world uses six-token programs of length 1–6 operating on an integer register, with gold reward equal to the fraction of eight input–output pairs matched under execution.Executions abort when |v| > 10^6, and tasks use hidden length-4 targets valid on the evaluation inputs.
Soundness AUC is the mean of Snd@N over N ∈ {20, . . . , 2^11} on a fresh pool of 2,048.
Experiment 6 uses 60 tasks across 12 rounds, mixing 16 top-probability and 16 random claims, with 32 claims settled per round.The pooled design settles 1,920 claims per round and starts each task with 200 random labels.
RichDSL: RichDSL expands programs to length 1–10 over ten tokens, uses 16 evaluation inputs, and reports random programs’ average gold reward as 0.018.Targets are length-6 programs, while invalid values with |v| > 10^9 are scored as mismatches.
The richer experiments compare ridge, steepest-ascent, evolutionary, and settlement-aware procedures over 300 steps, with settlement of 25 recent unique programs every 25 steps.The settlement-aware setup uses 300 reality queries per run and 100 tasks.
Evaluation treats the task as the statistical unit, uses paired two-sided Wilcoxon tests unless direction was preregistered, and computes 95% bootstrap intervals.Reliability and resolution decomposition are computed out-of-sample before each refit; experiments run on a single CPU.