Proof-Carrying Cognition: Closing the Verification Gap with Reality-Settled Reward
作者: Eshwar Reddy M, Sourav Karmakar
分类: cs.AI, cs.LG
发布日期: 2026-09-09
备注: 21 pages, 13 figures
💡 一句话要点
提出基于现实奖励的证明携带认知以缩小验证差距
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)
关键词: 证明携带认知 验证差距 程序合成 现实奖励 推理模型 强化学习 可靠性评估
📋 核心要点
- 核心问题：现有方法在非正式领域缺乏可扩展且可靠的推理奖励，导致验证差距。
- 方法要点：提出证明携带认知的范式，通过自建世界模型对推理步骤进行定价，解决验证问题。
- 实验或效果：在程序合成测试中，可靠验证器的表现优于非可靠验证器，且现实奖励的使用显著提高了执行奖励的保留率。
📝 摘要（中文）
语言模型推理的前沿进展源于对推理轨迹的强化学习，主要集中在具有廉价、可靠验证器的领域。本文提出的验证差距是该领域的主要限制：在非正式领域缺乏可扩展、不可腐蚀的推理奖励。我们做出了四项贡献：在联合高斯模型中，验证器与黄金标准的相关性是测试时计算与能力之间的确切交换率；在程序合成测试中，非可靠验证器在优化过程中失去可靠性，而可靠验证器则单调改善；提出了证明携带认知的范式；并指定了现实奖励推理基准的主要指标为压力下的可靠性。
🔬 方法详解
问题定义：本文旨在解决在非正式领域缺乏可扩展、不可腐蚀的推理奖励的问题。现有方法在验证过程中面临验证差距，导致推理能力的评估不准确。
核心思路：论文提出了证明携带认知的概念，通过将推理步骤视为经过类型化的概率性声明，并利用自建的世界模型进行定价，从而实现对推理过程的有效验证。
技术框架：整体架构包括四个主要模块：联合高斯模型用于分析验证器与黄金标准的相关性；程序合成测试床用于验证推理的可靠性；现实奖励机制用于优化推理过程；以及基于压力下的可靠性指标进行评估。
关键创新：最重要的技术创新在于提出了压力下的可靠性作为评估指标，能够更准确地反映推理模型在真实环境中的表现，与传统方法相比具有显著的优势。
关键设计：在实验中，采用了基于现实的奖励模型，设置了不同的参数以优化推理过程，并通过对比实验验证了不同验证器的表现差异。
🖼️ 关键图片
📊 实验亮点
实验结果显示，在程序合成测试中，非可靠验证器的可靠性在优化过程中显著下降，从0.94降至0.32，而可靠验证器则持续改善。此外，现实奖励机制使得执行奖励的保留率提高了六倍，显示出该方法在推理效率上的显著提升。
🎯 应用场景
该研究的潜在应用领域包括程序合成、自动化推理和智能代理系统等。通过提供可靠的推理奖励机制，可以在更广泛的非正式领域中应用语言模型，提升其在实际场景中的表现和可靠性，具有重要的实际价值和未来影响。
📄 摘要（原文）
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.