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

2609.09776 ↗ · 2026-09-09 · cs.AI, cs.LG

Eshwar Reddy M, Sourav Karmakar

21 pages, 13 figures

The finding

Headline claim

Reinforcement learning on reasoning is bottlenecked by verifier soundness, and anchoring learned verifiers to sparsely settled real-world outcomes (reality-anchored settlement) preserves verifier soundness under optimization pressure where frozen learned verifiers collapse.

The test

Theory (Gaussian best-of-N model) plus synthetic program-synthesis testbeds with executable ground truth, a pre-registered scaled replication in a ~10^10-program domain, and real-model experiments using a frontier-family generator, real LLM judges, and executed unit tests as gold on MBPP and HumanEval, plus GRPO training with reward-model refits on a 10% settlement stream.

Effect size & scope

Learned verifier soundness falls 0.94 to 0.32 at N=4096; settlement drives hacking gap from ~0.27 to ~0; on-policy settlement ~10x more label-efficient; executed reward preserved at 6x a frozen reward model under real GRPO with proxy reward climbing while executed reward collapses 90%; copula exchange-rate law predicts real judge soundness to 4.1% median error vs 79 points for Pearson. All evidence is small-scale testbeds; the full proof-carrying-cognition architecture is untested.

Limitations

Authors concede: experiments are deliberately minimal and validate mechanisms not frontier-scale claims; Gaussian closed form N^(1/rho^2) overstates penalty up to 24x and rho is not quantititatively predictive outside the model; two pre-registered claims were falsified; the drift-alarm criterion failed its first test; the 'world model' component at training scale is untested; linear-Gaussian model predicts plateau not decline. Unstated: only program synthesis and code domains have executable gold; authors' affiliations (Testsigma, Intuit) are industry, not academic labs; empirical sections not visible beyond abstract-level claims.

Counterpoint

Position paper with proof-of-concept experiments designed by the authors themselves; the core paradigm (self-built world models as amortized reality) is argued, not demonstrated; settlement assumes reality feedback is obtainable in domains where verification is actually hard (drug targets, strategy), which the paper admits is unsolved; benchmark construction (RSR-Bench) is a proposal, not an artifact; pre-registration is laudable but the domain is one where ground truth is cheap by construction, so generality to the claimed bottleneck domains is untested.

Economy implication

Little or nothing for near-term AI economics. If the paradigm worked at scale it could extend RL-driven capability gains beyond math and code (supporting 1.4-style inference-compute returns), but the paper itself shows only laptop-scale mechanisms and one real-model demonstration; no deployment, cost, or revenue evidence.

Who this matters for

Technical Capability: Directly relevant: it quantifies how much test-time compute is worth as a function of verifier fidelity and shows verifier gaming is driven by selection pressure, not prompt-level adversaries.

Market & Valuation: Weakly relevant: if verification is the binding constraint on RL progress, domains without sound verifiers may see slower capability gains than RL-hype implies, but this paper offers no economic data.

Bears on (advisory · papers never write evidence)

[1.4] Inference-time compute yields gains that don't saturate quickly on hard reasoning.

Abstract

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.