Search papers, labs, and topics across Lattice.
The authors formalize the "verification gap" in post-training reasoning through a joint-Gaussian copula framework of best-of-$N$ selection, establishing that verifier-gold correlation $\rho$ sets an exact polynomial penalty $N^{1/\rho^2}$ on compute scaling. Across program-synthesis benchmarks, they show that optimization pressure reliably degrades unsound verifiers鈥攃ollapsing true executed reward by 90% under standard GRPO fine-tuning. Grounding verifiers with an on-policy, reality-settled execution stream of just 10% eliminates this reward hacking and preserves 6x the executed reward, providing an empirical foundation for "proof-carrying cognition."
Optimizing against frozen reward models collapses true executed reasoning performance by 90% under GRPO, but feeding back an on-policy stream of just 10% reality-settled labels closes the hacking gap and preserves 6x the reward.
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.
