JURY-RL: Votes Propose, Proofs Dispose for Label-Free RLVR
TL;DR 精炼摘要
JURY-RL提出一种无标签可验证奖励强化学习框架,通过模型投票生成答案候选,由Lean定理证明器验证并决定奖励,结合ResZero机制处理不可验证情况,避免虚假共识,提升训练稳定性和推理性能,在数学推理和代码生成等任务上优于无标签基线,媲美甚至超越监督训练。
摘要
000 001 002 003 004 005 006 007 008 009 010 011 012 013 014 015 016 017 018 019 020 021 022 023 024 025 026 027 028 029 030 031 032 033 034 035 036 037 038 039 040 041 042 043 044 045 046 047 048 049 050 051 052 053 Under review as a conference paper at ICLR 2026 JURY-RL: V OTES P ROPOSE , P ROOFS D ISPOSE FOR L ABEL - F REE RLVR Anonymous authors Paper under double-blind review A BSTRACT Reinforcement learning with verifiable rewards (RLVR) enhances the reasoning of large language models (LLMs), but its scalability is hampered by the high cost of human-annotated labels. Label- free alternatives, such as majority voting or LLM-as-a-judge, are susceptible to false positives that lead to reward hacking and training collapse. We introduce JURY-RL , a label-free RLVR frame- work that separates answer proposal from reward disposal: votes from model rollouts propose a consensus answer, while a formal theorem prover disposes the final reward. Specifically, a rollout is rewarded only if the majority-voted answer is formally verified by a Lean prover. When verification is inconclusive, we activate our proposed ResZero (Residual-Zero) reward: it drops the unverifiable
思维导图
论文精读
中文精读
1. 论文基本信息
1.1. 标题
JURY-RL: Votes Propose, Proofs Dispose for Label-Free RLVR (JURY-RL: 票选提议,证明处置,实现无标签可验证奖励强化学习)
1.2. 作者
匿名作者 (Anonymous authors)
1.3. 发表期刊/会议
该论文目前处于双盲评审阶段 (Paper under double-blind review),预计发布在 OpenReview 平台。
1.4. 发表年份
2025年
1.5. 摘要
可验证奖励强化学习 (Reinforcement Learning with Verifiable Rewards, RLVR) 能够增强大语言模型 (Large Language Models, LLMs) 的推理能力,但其可扩展性受限于高昂的人工标注成本。现有的无标签替代方案,如多数投票 (majority voting) 或 LLM 作为判官 (LLM-as-a-judge),容易产生假阳性 (false positives),从而导致奖励黑客攻击 (reward hacking) 和训练崩溃 (training collapse)。
本文引入了 JURY-RL,一个无标签的 RLVR 框架,它将答案提议 (answer proposal) 与奖励处置 (reward disposal) 分离:模型 推演 (rollouts) 的投票提议一个共识答案,而形式化定理证明器 (formal theorem prover) 处置最终奖励。具体来说,只有当多数投票选出的答案被 Lean 证明器 (Lean prover) 形式化验证时,推演 (rollout) 才会获得奖励。当验证结果不确定时,本文激活了所提出的 ResZero (Residual-Zero) 奖励机制:它会放弃不可验证的多数提议,并为剩余 (residual) 答案分配一个零均值、保留方差的奖励。这种设计在不强化虚假共识 (spurious consensus) 的前提下,为强化学习 (Reinforcement Learning, RL) 算法保持了稳定的优化梯度 (optimization gradient)。
在数学推理、代码生成和多任务基准测试中的实验表明,JURY-RL 不仅实现了更稳定的训练,而且始终优于无标签基线 (label-free baselines),甚至在 pass@1 和 pass@k 指标上与使用真值奖励 (ground-truth rewards) 的监督训练 (supervised training) 相匹配或超越。
1.6. 原文链接
- OpenReview 链接: https://openreview.net/forum?id=tnfvv9Wsw9
- PDF 链接: https://openreview.net/pdf?id=tnfvv9Wsw9
2. 整体概括
2.1. 研究背景与动机
核心问题: 大语言模型 (LLMs) 在数学和程序推理等任务中,虽然能力广泛,但其推理的可靠性 (reliability) 仍然是一个瓶颈。现有的 可验证奖励强化学习 (Reinforcement Learning with Verifiable Rewards, RLVR) 方法通过程序执行、数学等价性等可验证信号来对模型的正确性进行奖励,而非仅仅是其合理性 (plausibility),从而提升了 LLMs 的推理能力。然而,RLVR 的大规模应用受到其对人工标注答案 (human-annotated answers) 或精心策划的规范 (carefully curated specifications) 的高度依赖,这导致了高昂的成本 (costly) 和 覆盖范围有限 (limited in coverage) 的问题,严重阻碍了其可扩展性。
现有挑战: 为了降低标注成本,研究人员探索了无标签 (label-free) 的奖励方法,即在训练过程中不提供人类标注的真值答案。
-
自监督自奖励 (Self-supervised self-reward):这类方法从模型自身或无标签数据中获取信号,例如熵最小化 (entropy minimization)、自我确信度 (self-certainty) 和多数投票 (majority voting)。但这些方法容易产生 假阳性 (false positives),导致模型学习满足替代指标而非真正的正确性,进而引发 奖励黑客攻击 (reward hacking) 和 训练崩溃 (training collapse)。
-
LLM 作为判官 (LLM-as-a-Judge):另一种无标签方法是使用一个强大的 LLM 作为自动判官来评估模型输出。然而,这种方法在实践中容易受到 指令和格式操纵 (instruction and format manipulation) 的影响,并且在推理步骤隐藏时具有 高假阳性率。它们还对提示 (prompting) 和温度 (temperature) 参数敏感,并引入了显著的计算开销 (compute overhead) 和共享偏见 (shared-bias risks)。
现有方法的根本挑战: 无论是强化虚假共识 (reinforcing false consensus) 还是奖励黑客攻击 (reward hacking),现有无标签方法的不足都指向一个更深层次的挑战。论文指出,一个真正鲁棒的奖励信号必须同时满足三个基本属性:
- 可扩展性 (Scalable): 无需昂贵的人工监督。
- 真理对齐 (Truth-aligned): 奖励可验证的正确性,而非容易出错的共识。
- 优化稳定性 (Optimization-stable): 即使验证结果不确定,也能保证学习过程的持续进行。 以往的方法在不同程度上未能同时满足这三个标准。例如,多数投票实现了可扩展性但牺牲了真理对齐,而 LLM 作为判官在真理对齐和优化稳定性两方面都面临挑战。
这篇论文的切入点/创新思路: 基于上述挑战,论文提出了 “票选提议,证明处置 (Votes Propose, Proofs Dispose)” 的核心理念。这一策略旨在解耦候选答案的提议过程与其奖励的最终处置。为了保持可扩展性,模型推演的投票首先通过计算成本较低的多数投票提出一个共识候选答案。然后,一个形式化定理证明器 (如 Lean) 作为可靠的判官,对这唯一的候选答案处置最终奖励。这种设计避免了对每个独特答案进行形式化验证所带来的高昂成本,从而使整个框架在大规模应用中变得可行。
2.2. 核心贡献/主要发现
本文的主要贡献体现在以下三个方面:
- 提出 JURY-RL 框架: 引入了一个新颖的、无标签的 RLVR 框架 JURY-RL,它实现了“票选提议,证明处置”的范式。通过仅对多数投票选出的候选答案进行战略性验证,JURY-RL 使用形式化验证器将奖励与可证明的正确性对齐,从而消除了对人工标注答案的需求。
- 设计 ResZero (Residual-Zero) 奖励: 提出了一种原则性的备用机制 ResZero,用于处理验证结果不确定 (inconclusive) 的情况。通过放弃不可验证的多数提议,并为剩余 (residual) 候选答案分配一个零均值、保留方差的奖励,该机制确保了稳定的优化过程,并防止了因虚假共识导致的训练崩溃。
- 实验验证卓越性能: 在数学推理、代码生成和多任务基准测试中,JURY-RL 表现出更稳定的训练,并在无标签方法中取得了最先进的 (state-of-the-art) 结果。它甚至在
pass@1和pass@k指标上与使用真值奖励的监督基线相匹配或超越。这表明,形式化验证的信号不仅可以作为真值奖励的替代品,甚至可能成为学习可泛化推理能力的更有效目标。
3. 预备知识与相关工作
3.1. 基础概念
3.1.1. 强化学习 (Reinforcement Learning, RL)
强化学习 (Reinforcement Learning, RL) 是一种机器学习范式,智能体 (agent) 通过与环境 (environment) 交互来学习如何采取行动以最大化累积奖励。在 RL 中,智能体在每个时间步观察环境状态,根据其 策略 (policy) 采取一个动作,环境根据这个动作返回一个奖励并转移到新的状态。智能体的目标就是学习一个最优策略,使其在长期互动中获得最高的奖励。
3.1.2. 大语言模型 (Large Language Models, LLMs)
大语言模型 (Large Language Models, LLMs) 是指具有数亿到数万亿参数的深度学习模型,通常基于 Transformer 架构,并通过在海量文本数据上进行自监督预训练而获得。它们能够理解和生成人类语言,并在各种自然语言处理任务(如问答、文本生成、翻译等)中展现出强大的能力。在推理任务中,LLMs 通常被要求生成一步步的推理过程和最终答案。
3.1.3. 可验证奖励强化学习 (Reinforcement Learning with Verifiable Rewards, RLVR)
可验证奖励强化学习 (Reinforcement Learning with Verifiable Rewards, RLVR) 是强化学习的一个分支,其奖励信号不是基于人类偏好或模糊的启发式规则,而是基于 外部可验证的信号 (externally verifiable signals)。这些信号通常来源于程序执行结果、数学证明器的验证、单元测试或形式化规范的检查。RLVR 的核心目标是使 LLMs 学习生成不仅听起来合理,而且在逻辑上或计算上被证明是正确的推理和答案。这与传统的 RLHF (Reinforcement Learning from Human Feedback) 不同,后者往往侧重于人类偏好的对齐,可能导致模型生成“听起来对”但实际错误的内容。
3.1.4. 形式化定理证明器 (Formal Theorem Prover) 与 Lean 证明器
形式化定理证明器 (Formal Theorem Prover) 是一种软件工具,用于辅助或自动构建和验证数学证明。它基于形式逻辑系统和严格的数学公理,确保每一步推理的正确性。一个成功的形式化证明意味着该定理在逻辑上是无可辩驳的。 Lean 证明器 (Lean Prover) 是一个开源的交互式定理证明器,它结合了程序语言和证明助手的功能。Lean 允许用户以一种类似于编程的方式编写数学证明,并且它的内核会严格检查这些证明的有效性。Lean 在数学领域被广泛用于形式化大型数学定理,其提供的验证结果具有极高的可靠性,能够确保逻辑上的零假阳性。
3.1.5. 组相对策略优化 (Group Relative Policy Optimization, GRPO)
组相对策略优化 (Group Relative Policy Optimization, GRPO) 是一种在 RLVR 中使用的强化学习算法。它通过对一个问题生成的多条 推演 (rollouts) 进行 组内归一化 (group-normalized) 来计算优势函数 (advantage function)。传统的策略梯度方法通常基于单个 推演 (rollout) 的奖励进行更新,而 GRPO 考虑了一组 推演 (rollouts) 的相对表现,从而在可验证奖励稀疏或噪声较大时提供更稳定的梯度。这种方法有助于模型在复杂推理任务中更有效地学习。
3.2. 前人工作
3.2.1. 大语言模型推理 (Large Language Model Reasoning)
LLMs 在广泛能力上取得了显著进展,但可靠的数学和程序推理仍是瓶颈。模型常常优化 合理性 (plausibility) 而非 可验证的正确性 (verifiable correctness)。诸如思维链 (chain-of-thought) 和自洽性 (self-consistency) 等后训练技术可以提高平均准确率,但也可能在缺乏外部检查时放大“自信但错误”的结果。这促使了对可验证对齐训练信号 (verifiability-aligned training signals) 的研究,这些信号奖励可证明的正确性,而非表面上的正确性。
3.2.2. 无标签 RLVR (Label-Free RLVR)
为了超越标注规范的限制,无标签的替代方法从模型或无标签数据本身获取奖励信号:
- 模型内部自奖励信号 (Model-Internal Self-Reward Signals):
- 输出端代理 (Output-side proxies): 例如熵最小化 (entropy minimization) 或基于确信度 (confidence-based scores) 的方法,奖励那些表现出高确定性的假设。然而,这种方法很脆弱,当模型自信地出错时,它会放大错误。
- 单视图一致性 (Single-view agreement): 奖励来自同一输入 的多个输出之间的一致性。例如,对于 个响应 ,它识别出多数投票答案 ,并奖励匹配 的响应。主要风险是强化了错误的共识,模型可能收敛到一个流行但错误的答案,通常是通过利用格式约定等肤浅的启发式方法。
- 多视图一致性 (Multi-view agreement): 试图通过在多个语义等效的提示之间强制执行一致性来提高鲁棒性。例如,来自提示变体 的多数答案被用作伪标签 (pseudo-label) 来监督来自原始提示 的响应。这通常可以提高训练稳定性,但通常只是延迟而非消除奖励黑客攻击,因为虚假的捷径最终可能会在多个视图中传播。
- 外部判官信号 (External-Judge Signals):
- LLM 作为判官 (LLM-as-a-Judge): 使用强大的外部 LLM 作为自动化判官来评估模型的输出。虽然无标签,但它引入了对判官提示设计和解码策略的敏感性,产生了显著的计算成本,并有将判官固有偏见转移到训练信号中的风险。
- LLM 知识蒸馏 (LLM-based Knowledge Distillation, LLM-KD): 教师模型生成参考答案来指导学生模型。虽然可能提供更细粒度的信号,但同样受限于教师模型的能力和偏见。
3.2.3. Lean 和其他验证器 (Lean and Other Verifiers)
基于验证的训练利用外部可检查信号,如程序执行和单元测试、SMT 求解器或形式化证明助手(如 Lean/Coq),将奖励与正确性挂钩。以往的“生成-然后-验证”流水线 (generate-then-verify pipelines) 在验证失败时通常不提供学习信号,限制了稳定性和样本效率。
3.3. 技术演进与差异化分析
技术演进: LLMs 的推理能力从最初的基于文本生成,演进到通过思维链 (Chain-of-Thought) 引导逐步推理,再到利用外部工具 (tool-use) 和强化学习 (RL) 进行优化。其中,RLHF (Reinforcement Learning from Human Feedback) 旨在使模型行为与人类偏好对齐,但可能导致模型“看起来正确”而非“真正正确”。RLVR 则进一步推动了这一方向,旨在通过可验证的外部信号来奖励模型的逻辑正确性,从而避免“幻觉”和不准确的推理。无标签方法旨在降低RLVR的成本,但却引入了假阳性、奖励黑客攻击和训练崩溃等问题。
差异化分析: JURY-RL 与现有方法的差异主要体现在其独特的 “票选提议,证明处置” (Votes Propose, Proofs Dispose) 范式:
- 与模型内部自奖励方法的对比:
- 多数投票、自确信度、熵最小化等方法虽然实现了可扩展性,但容易强化 虚假共识 (spurious consensus),导致模型学习到流行但错误的答案,并引发训练崩溃。JURY-RL 通过引入形式化验证器,保证了奖励的 真理对齐 (truth-alignment),仅奖励被证明为正确的多数答案,从而抑制了假阳性。
- 与外部判官信号方法的对比:
- LLM 作为判官和 LLM 知识蒸馏虽然缓解了内部自确认偏见,但它们本身容易受到提示敏感性、计算成本高昂以及判官自身偏见的影响,其奖励信号的 精确率 (precision) 较低,导致仍可能强化错误。JURY-RL 的 Lean 验证器提供了极高的精确率,保证了奖励信号的可靠性,即使牺牲了一部分召回率,也通过 ResZero 机制维持了优化稳定性。
- 与传统验证器方法的对比:
- 以往的“生成-然后-验证”流水线在验证失败时通常不提供学习信号,导致学习停滞或效率低下。JURY-RL 的 ResZero 奖励机制解决了这个问题,即使验证结果不确定,也能提供一个零均值、保留方差的信号,使得 GRPO 能够保持稳定的梯度,进行有益的探索,而不是简单地停滞不前。
- 核心创新点: JURY-RL 在保持 无标签可扩展性 (label-free scalability) 的同时,通过 证明门控 (proof-gated) 的设计和 ResZero 奖励 (ResZero reward) 机制,解决了现有无标签方法在 真理对齐 (truth-alignment) 和 优化稳定性 (optimization stability) 方面的痛点,实现了三者的协同优化。
4. 方法论
JURY-RL 的设计旨在满足三个核心原则:(i) 无需昂贵的人工监督即可实现 可扩展性 (scalability),(ii) 通过基于可验证证据来确定奖励实现 真理对齐 (truth alignment),以及 (iii) 即使验证结果不确定也能确保持续学习的 优化稳定性 (optimization stability)。为了实现这些目标,本文解耦了候选答案的提议过程和其奖励的最终处置过程。策略模型自身的 推演 (rollouts) 所产生的投票作为一种可扩展的提议机制,而形式化定理证明器则作为可靠的判官来处置奖励。
这种设计选择——仅验证单个多数投票的候选答案——对于保持计算的可处理性 (computational tractability) 和可扩展性至关重要。对所有 推演 (rollouts) 生成的每个独特答案进行形式化验证将是成本过高的,这将损害无标签方法的效率。因此,多数投票作为一种有效的启发式方法,用于识别最有希望的候选答案,以进行昂贵但可靠的验证过程。
本节将详细阐述 JURY-RL 框架的两个关键组成部分:强制真理对齐的整体证明门控奖励机制,以及旨在维护优化稳定性的 Residual-Zero (ResZero) 备用机制。
4.1. 问题设置
首先,我们定义问题设置。
- 策略 LLM (Policy LLM): 用 表示一个参数为 的策略 LLM。
- 生成轨迹和答案 (Generating Trajectories and Answers): 对于给定的问题 ,模型生成一个词元序列 。然后,一个确定性的提取器 从 中解析出候选答案 。
- 无标签设置 (Label-Free Setting): 在无标签设置中,训练期间不提供真值答案 (ground-truth answers)。
- 机器可检查规范与验证器 (Machine-Checkable Specification and Verifier): 相反,每个问题 可以关联一个机器可检查的规范 ,并且一个外部验证器(例如,基于 Lean 的检查器)提供一个二元判据: 这个函数返回 1 如果 在标准健全性假设下被形式化认证为正确,否则返回 0。
4.1.1. 优化目标
我们优化一个 KL 正则化的 RLVR 目标函数 (KL-regularized RLVR objective),其中包含一个参考策略 和系数 : 符号解释:
- : 带有参数 的策略 LLM。
- : 问题分布。
- : 从 中采样的一个输入问题。
- : 策略 根据输入 生成的词元序列(轨迹)。
- : 对于输入 的轨迹 计算的奖励函数。这个奖励是根据一组 个 推演 (rollouts) 共同计算的。
- : KL 散度惩罚项的系数,用于控制策略 偏离参考策略 的程度。
- : 策略 与参考策略 在输入 上的 KL 散度 (Kullback-Leibler divergence)。这通常用于防止策略在训练过程中偏离预训练模型()过远,以保持生成质量和稳定性。
4.1.2. 组相对策略优化 (GRPO)
我们采用 组相对策略优化 (Group Relative Policy Optimization, GRPO) (Shao et al., 2024) 来估计组归一化优势函数 (group-normalized advantages)。具体来说,对于每个输入 ,我们从旧策略 中采样 个 推演 (rollouts) ,其中 ,并计算每个 推演 (rollout) 的奖励 。 标量组优势函数 (scalar group advantage) 定义为: 符号解释:
-
: 第 个 推演 (rollout) 的标量组优势。这个值表示第 个 推演 (rollout) 的奖励相对于该组平均奖励的优劣程度,并由组内奖励的标准差进行归一化。
-
: 第 个 推演 (rollout) 的奖励。
-
: 组内 个 推演 (rollouts) 奖励的平均值。
-
: 组内 个 推演 (rollouts) 奖励的标准差。
-
: 一个小的正数,用于防止标准差为零时分母为零,增加数值稳定性。
令每词元比率 (per-token ratio) 为 。GRPO 算法最大化以下目标函数: 符号解释:
-
: GRPO 的目标函数,期望在问题分布和当前策略下计算。
-
: 每个问题生成的 推演 (rollouts) 数量。
-
: 第 个 推演 (rollout) 的长度(词元数量)。
-
: 第 个 推演 (rollout) 在时间步 时,新策略 与旧策略 生成词元 的概率比率。
-
: 第 个 推演 (rollout) 在时间步 的优势。在 GRPO 中,这通常是标量组优势 的广播形式(或者可以是其每词元变体)。
-
: 一个裁剪函数,将策略比率 裁剪到 的范围内。这有助于限制策略更新的幅度,防止过大的更新导致训练不稳定。
-
: 裁剪超参数,控制裁剪范围。
-
: KL 散度惩罚项,与主目标函数中的一致。
4.2. 证明门控奖励框架 (The Proof-Gated Reward Framework)
JURY-RL 的工作流程从 提议阶段 (proposal stage) 开始。对于一个给定的问题 ,我们生成 条轨迹 并解析出它们对应的答案 。通过多数投票 (majority vote) 确定最频繁出现的答案,这成为我们的候选提议: 符号解释:
-
: 多数投票选出的共识答案。
-
: 第 个轨迹 中解析出的答案。
-
: 指示函数,如果 等于 ,则为 1,否则为 0。
-
: 返回使得求和项最大的答案 。
这个提议 随后进入 处置阶段 (disposal stage)。通过调用外部 Lean 验证器 对 的正确性进行评估,对照 的形式化规范。这会产生一个二元 证明门控 (proof-gate) 信号 ,该信号决定了奖励的分配。
最终奖励 为每个轨迹 分配,其值由 进行条件控制: 符号解释:
- : 第 个轨迹的最终奖励。
- : 验证器 的输出。如果多数答案 通过验证,则 ;如果验证不确定,则 。
- : 指示函数,如果第 个轨迹的答案 与多数答案 相同,则为 1,否则为 0。
- : Residual-Zero 奖励,当验证不确定 () 时激活。
稳定性分析: 这种证明门控设计的稳定性源于其对成功和不确定验证的原则性处理。
- 验证成功 (): 只有生成并支持被证明正确的答案的轨迹才会获得正奖励。这种方法将学习信号直接与硬证据绑定,根据标准健全性假设,这能够抑制自奖励或基于判官的代理方法中普遍存在的假阳性。
- 验证不确定 (): 系统会退回到 ResZero 备用机制,而不是简单地奖励多数共识。这种精心设计的替代方案通过保留组内方差来维持稳定的优化梯度,防止学习停滞或震荡。
- 抗攻击性: 通过仅奖励可验证的正确性,该框架固有地缩小了提示和格式黑客攻击的攻击面,而这是其他无标签系统中的关键漏洞。
4.3. RESZERO (Residual-Zero) 奖励
当形式化验证结果不确定时,仍需要一个学习信号来维持优化稳定性。然而,像直接奖励多数投票 (MV) 这样的朴素选择是脆弱的,并有导致训练崩溃的风险。将 MV 用作奖励会将一致性与正确性混淆,并可能在 GRPO 下导致熵崩溃 (entropy collapse),因为虚假共识会增强。简单的零奖励备用方案也是次优的,因为它会导致零组优势,从而有效地停止学习过程。
为了解决这个问题,我们引入了 ResZero (Residual-Zero) 奖励。其原则是惩罚不可验证的多数提议,并从剩余 (residual) 答案中构建一个有意义的零均值奖励。这种设计通过在少数意见中保持方差来保留有用的学习信号,而不会放大潜在的错误共识。此外,我们提出了一种自适应变体,当模型最自信地犯错时,这种信号会变得更强。直觉是,一个强大但未经验证的共识(由高多数份额 表示)需要更强的修正信号。ResZero 通过使用 来同时放大残差答案的奖励信号并抑制多数答案,从而实现这一点。
令 为支持多数答案的 推演 (rollouts) 集合,而 为剩余 推演 (rollouts) 的集合。多数份额为 。我们首先为残差组内答案 定义 留一法残差份额 (leave-one-out residual share): 符号解释:
-
: 对于在残差组 中的 推演 (rollout) ,其答案为 ,这个值表示在排除了 推演 (rollout) 之外,残差组中其他 推演 (rollouts) 支持答案 的比例。
-
: 残差组中除 推演 (rollout) 之外的 推演 (rollouts) 数量。
令 如果 (残差组内其同伴答案的相对支持度),并且 如果 。 ResZero 奖励随后分配为: 符号解释:
-
: 第 个轨迹的 Residual-Zero 奖励。
-
: 多数答案的份额,即 。
-
: 指示函数,如果轨迹 在残差组 中,则为 1,否则为 0。
-
: 如果 ,则为 ;如果 ,则为 0。
-
: 残差组内答案的平均支持度,即 。
-
: 一个正的超参数,控制对多数答案的惩罚强度。
-
: 指示函数,如果轨迹 在多数组 中,则为 1,否则为 0。
-
: 全局重新中心化项,确保总奖励和为零。
零均值证明 (Proof of Zero-Mean Property): 为了确保总奖励和为零 (),全局重新中心化项 的推导如下: 符号解释:
- : 全局重新中心化项,其值由惩罚强度 和多数份额 的平方决定,确保整个组的 ResZero 奖励的平均值为零。
ResZero 奖励的鲁棒优化特性:
-
方差保留 (Variance preservation): 它在不同答案之间保持非零方差,这对于 GRPO 等方差归一化优化器至关重要,以防止梯度消失。
-
零均值构造 (Zero-mean construction): 其严格的零均值特性使其成为一个原则性的、与优化器无关的信号,确保了除了 GRPO 之外,它也适用于任何通用 RL 范式。
-
自适应经济性 (Adaptive economy): 修正信号根据多数份额 动态调整,当模型最自信地犯错时施加最大压力,而所有这些行为仅由一个超参数 控制。
这种双重奖励策略取决于验证器的结果。如果验证成功 (),策略更新由可验证的正确性指导。反之,如果验证不确定 (),ResZero 备用方案惩罚未经验证的多数意见,这对于缓解由虚假共识引起的熵崩溃至关重要。这种设计通过每个步骤仅需一次验证来保持无标签训练的可扩展性。
4.4. JURY-RL 算法流程
以下是 JURY-RL 算法的完整流程(针对一个问题 的一次分组更新):
Algorithm 1 JURY-RL (one grouped update for a prompt )
- Sample rollouts ; parse .
- 翻译: 从旧策略 中采样 条轨迹 ;解析出它们的答案 。
- Compute vote shares
v(a)and majority .- 翻译: 计算每个答案的投票份额
v(a),并确定多数答案 (即投票份额最高的答案)。
- 翻译: 计算每个答案的投票份额
- Query verifier once: .
- 翻译: 对多数答案 调用验证器一次:得到二元结果 。
- if then
- 翻译: 如果 (验证通过) 则执行:
- Set .
- 翻译: 设置奖励 为指示函数 (即如果 是多数答案则奖励为 1,否则为 0)。
- else
- 翻译: 否则 (如果 ,验证不确定) 则执行:
- Form
M, R; compute and ; set via Eq. (5).- 翻译: 形成多数组 和残差组 ;计算留一法残差份额 和平均支持度 ;根据式 (5) 设置 为 。
- end if
- Compute group-normalized advantages from ; broadcast token-wise.
- 翻译: 从计算出的奖励 中计算组归一化优势 ;并将其广播到每个词元。
- Update with GRPO (clipped ratios, KL to reference).
- 翻译: 使用 GRPO 算法更新策略 (包括裁剪比率和与参考策略的 KL 散度惩罚)。
5. 实验设置
5.1. 数据集
实验使用了以下数据集:
- 训练数据集: 在 MATH 数据集 (Hendrycks et al., 2021) 的训练集子集上进行训练,该子集包含 7,500 个问题。
- 评估数据集:
- 数学推理 (Mathematical Reasoning):
- AIME24/25 (Hugging Face H4, 2024; OpenCompass, 2025): 美国数学邀请赛问题。
- MATH500 (Lightman et al., 2024): 包含 500 个数学问题,是 MATH 数据集的验证集。
- GSM8K (Cobbe et al., 2021): 8k 个小学数学文字问题。
- AMC (math-ai Team, 2024): 美国数学竞赛问题。
- 代码生成 (Code Generation):
- LiveCodeBench (Jain et al., 2024): 代码生成基准。
- CRUX (Gu et al., 2024a): 代码推理、理解和执行基准。
- 指令遵循和多任务 (Instruction-Following and Multi-Task):
- IFEval (Zhou et al., 2023): 用于评估指令遵循能力。
- MMLU-Pro (Wang et al., 2024): 用于多任务理解的基准。
- 数学推理 (Mathematical Reasoning):
5.2. 评估指标
论文中使用了以下评估指标:
pass@1准确率 (pass@1 accuracy):- 概念定义:
pass@1是衡量模型在首次尝试生成解决方案时直接给出正确答案的能力。它反映了模型在单次生成中解决问题的直接有效性。 - 数学公式:
- 符号解释:
Number of problems with at least one correct solution in 1 attempt: 在一次尝试中至少有一个正确解决方案的问题数量。Total number of problems: 总问题数量。
- 概念定义:
pass@k准确率 (pass@k accuracy):- 概念定义:
pass@k衡量模型在 次独立尝试中至少生成一个正确解决方案的能力。它反映了模型在多次尝试下解决问题的总成功率,通常用于评估生成多样性和探索能力。 - 数学公式: 论文中没有直接给出
pass@k的公式,但其标准定义通常为: 其中,更简单的计算方式是,在 个独立的采样中,如果至少有一个是正确的,则认为该问题解决。或者,如果直接从模型生成 个样本,pass@k可以通过以下公式估计: 但更常见且直观的理解是:从 个生成样本中,只要有一个通过验证,就算成功。 - 符号解释:
num_problems: 总问题数量。- : 对于问题 ,生成的所有样本中错误样本的数量。
- : 对于问题 ,生成的总样本数量。
- 论文中的具体 值:
- AIME:
- MATH500 和 GSM8K:
- AMC:
- 概念定义:
- 精确率 (Precision), 召回率 (Recall), F1-分数 (F1-Score):
- 这些指标用于评估验证器信号的质量。
- 概念定义:
- 精确率 (Precision): 在验证器标记为正确的答案中,实际正确的比例。高精确率意味着验证器很少将错误的答案误判为正确。
- 召回率 (Recall): 在所有实际正确的答案中,验证器正确标记的比例。高召回率意味着验证器能够发现大部分的正确答案。
- F1-分数 (F1-Score): 精确率和召回率的调和平均值,用于综合评估验证器的性能,特别是在两者之间需要权衡时。
- 数学公式:
- 符号解释:
TP(True Positive): 验证器正确标记为正确的答案数量。FP(False Positive): 验证器错误标记为正确的答案数量(实际是错误的)。FN(False Negative): 验证器错误标记为错误的答案数量(实际是正确的)。
5.3. 对比基线
论文将 JURY-RL 与以下几种无标签和监督奖励基线进行了比较:
- 多数投票 (Majority Voting, MV): 一种自监督共识奖励方法 (Shafayat et al., 2025)。对于每个问题,生成 条 推演 (rollouts)。如果一个 推演 (rollout) 提取的答案 与 条 推演 (rollouts) 中的多数答案匹配,则获得奖励 1,否则为 0。它直接强化流行答案,不考虑正确性。
- 自我确信度 (Self-Certainty): 一种基于信心的信号 (Zhao et al., 2025b)。奖励根据构成最终答案的词元的对数概率计算;累积对数概率越高,表示模型确信度越高,奖励也越高。
- 熵最小化 (Entropy Minimization): 一种低熵代理 (Prabhudesai et al., 2025)。奖励与最终答案词元的策略输出熵成反比,鼓励更确定、高信心的预测。
- 真值奖励 (Ground Truth, GT): 监督式预言机基线。使用人类标注的标签,如果一个 推演 (rollout) 提取的答案与真值匹配,则获得奖励 1,否则为 0。使用与 JURY-RL 相同的 GRPO 目标进行训练,以进行公平比较。
- LLM 作为判官 (LLM-as-a-Judge): 一种外部判官范式 (Pang et al., 2023; Zhao et al., 2025a)。使用
qwen-2.5-72b-instruct作为判官。它评估每个 推演 (rollout) 的推理过程和最终答案;其评估结果(数字分数或二元正确/错误标签)作为 RL 更新的奖励。 - LLM 知识蒸馏 (LLM-KD - Knowledge Distillation): 教师-学生蒸馏已被用于无标签 RLVR (Zhao et al., 2025a)。使用
qwen-2.5-72b-instruct为每个问题生成一个答案,并将其视为伪标签 (pseudo label)。策略模型被训练以使其输出与这些机器生成的参考答案对齐。
5.4. 实现细节
- 骨干模型 (Backbone Models): 实验在 Qwen2.5 (Yang et al., 2025b)、Qwen3 (Yang et al., 2025a) 和 Llama3 (Dubey et al., 2024) 系列的开源大语言模型上进行,以确保广泛适用性。
- 框架 (Framework): 所有方法均使用 VeRL 框架 (Sheng et al., 2025) 实现。
- 硬件 (Hardware): 在 NVIDIA A100 GPU 上进行训练。
- 训练参数 (Training Parameters):
- 训练批大小 (Training Batch size): 128 个采样问题。
- 每个问题的 推演 (rollouts) 数量 (): 8。
- 最大提示长度 (Max prompt length): 512。
- 最大生成词元数 (Max new tokens): 3072。
- 训练周期 (Training epoch): 6。
- 优化器 (Optimizer): AdamW。
- 学习率 (Learning rate): 。
- KL 损失系数 (): 0.005。
- 裁剪比率 (): 0.2。
- 训练温度 (Training temperature): 1.0。
- 评估温度 (Evaluation temperature): 0.8。
top-p: 0.95。
- 提示格式 (Prompting Formats): 采用所有模型官方发布的基于聊天的提示格式,以确保公平和可复现性。
- Lean 验证器细节 (Lean Verifier Details):
- 架构 (Architecture): 采用三阶段推理流水线 (three-stage inference pipeline),包括:
- 自动形式化器 (Autoformalizer): 使用 Goedel-Formalizer-V2-32B 模型 (Lin et al., 2025) 将非正式的数学语句转换为形式化的 Lean 规范。
- 一致性检查器 (Consistency-Checker): 使用 QwQ-32B (QwenTeam, 2025) 验证自动形式化器的输出。
- 证明器 (Prover): 使用 Goedel-Prover-V2-32B 模型 (Lin et al., 2025) 为已验证的规范合成形式化证明。
- 流水线操作 (Pipeline Operation):
- 自动形式化器生成 8 个候选形式化结果。
- 一致性检查器评估所有候选并选择排名靠前的检查通过的候选。
- 证明器进行多达 16 次独立采样尝试来找到有效证明 (Prover@16)。
- 验证配置 (Verification Configuration): 温度 0.7,最大词元 32,768。
- 性能与成本分析 (Performance and Cost Analysis): 针对 Lean 验证器的不同
Prover@k配置进行了分析(如 Table 5 所示),权衡准确率和词元成本后,选择Prover@16作为默认配置。
- 架构 (Architecture): 采用三阶段推理流水线 (three-stage inference pipeline),包括:
6. 实验结果与分析
6.1. 核心结果分析
6.1.1. 数学推理和域内泛化 (Mathematical Reasoning and In-Domain Generalization)
Table 1 展示了 JURY-RL 在数学推理基准测试上的表现。一个关键的发现是,虽然 JURY-RL 在域内 MATH500 测试集(与训练数据来源相同)上的优势相对温和,但其在域外数学基准测试(如 GSM8K 和 AMC)上的优势则显著增强。
本文认为,这种模式出现的原因是:包括监督式 GT (Ground Truth) 基线在内的竞争方法,往往会过度拟合 MATH 数据集的风格模式和问题解决捷径。相比之下,JURY-RL 依赖形式化验证,从而激励模型学习对这些分布偏移具有鲁棒性的底层数学原理。这种在数学领域内卓越的泛化能力带来了在所有三个骨干模型上相对于 GT 基线的显著整体性能提升:
-
Qwen3-1.7B-Base: 平均得分提升 +2.32 点 (+5.91% 相对提升)。
-
Llama-3.2-3B-Instruct: 平均得分提升 +1.91 点 (+5.93% 相对提升)。
-
Qwen2.5-7B: 平均得分提升 +1.53 点 (+3.28% 相对提升)。
例如,在 Qwen2.5-7B 上,JURY-RL 的平均得分为 48.13%,显著超过 GT 预言机 (46.60%) 和最强的无标签竞争者 LLM-KD (46.54%)。这些证据表明,形式化验证的信号不仅仅是真值奖励的代理,它可能是一个更强大的目标,用于学习可泛化的推理能力。
6.1.2. 域外泛化 (Out-of-Domain Generalization)
JURY-RL 强大的域内性能转化为跨代码生成、指令遵循和多任务知识测试的鲁棒域外泛化能力。在 Qwen2.5-7B 上,JURY-RL 再次超越了 GT 基线,平均得分达到 40.45% (提升 +2.76 点,相对提升 +7.32%)。在另外两个骨干模型上,其性能在统计学上与 GT 持平,同时始终是表现最佳的无标签方法。这些结果表明,对可验证正确性进行优化鼓励模型学习基本的可迁移技能,这些技能能够泛化到训练所用的数学领域之外。
6.1.3. 总体增益 (Overall Gains)
JURY-RL 在域内和域外任务中均展示了相对于真值 (GT) 基线的全面性能提升。具体来说:
-
在 Qwen-1.7B-Base 上,它比 GT 基线高出 +1.02 点 (+2.84% 相对提升)。
-
在 Qwen2.5-7B 上,它比 GT 基线高出 +2.08 点 (+4.88% 相对提升)。
-
在 Llama-3.2-3B-Instruct 上,它保持了 +0.99 点 (+3.13% 相对提升) 的稳健增益。
这表明 JURY-RL 的优势不仅在于解决了无标签方法中常见的训练崩溃问题,而且还在不同模型规模上提供了稳定且可扩展的性能提升。至关重要的是,这种以可验证性驱动的学习范式的好处超越了单一答案准确性 (
pass@1)。在后续分析中将展示,它还在更深层次上学习生成多样化且有效的解决方案路径,从而在多尝试成功率 (pass@k) 方面带来了更显著的改进,并有效地避免了自监督方法中常见的模式崩溃 (mode collapse)。
6.2. 数据呈现 (表格)
以下是原文 [Table 1] 的结果: Table 1: Main Results (%) of RL performance comparison on math reasoning benchmarks. Cell background colors indicate relative performance: darker colors denote better results within each model group.
| Methods | Mathematics | Code | Instruction | Multi-Task | Average | |||||
|---|---|---|---|---|---|---|---|---|---|---|
| AIME24 | AIME25 | MATH500 | GSM8K | AMC | LiveCode | CRUX | IFEval | MMLU-Pro | ||
| Qwen3-1.7B-Base | ||||||||||
| Before RL | ||||||||||
| GT-Reward | ||||||||||
| Self-Certainty | ||||||||||
| Entropy | ||||||||||
| Majority-Voting | ||||||||||
| CoReward | ||||||||||
| LLM-KD | ||||||||||
| LLM-as-a-Judge | ||||||||||
| JURY-RL (Ours) | ||||||||||
| Llama-3.2-3B-Instruct | ||||||||||
| Before RL | ||||||||||
| GT-Reward | ||||||||||
| Entropy | ||||||||||
| Self-Certainty | ||||||||||
| Majority-Voting | ||||||||||
| CoReward | ||||||||||
| LLM-KD | ||||||||||
| LLM-as-a-Judge | ||||||||||
| JURY-RL (Ours) | ||||||||||
| Qwen2.5-7B | ||||||||||
| Before RL | ||||||||||
| GT-Reward | ||||||||||
| Self-Certainty | ||||||||||
| Entropy | ||||||||||
| Majority-Voting | ||||||||||
| CoReward | ||||||||||
| LLM-KD | ||||||||||
| LLM-as-a-Judge | ||||||||||
| JURY-RL (Ours) |
分析:
- JURY-RL 的卓越性能: 在所有三个骨干模型 (Qwen3-1.7B-Base, Llama-3.2-3B-Instruct, Qwen2.5-7B) 上,JURY-RL 在数学推理任务 (AIME, MATH500, GSM8K, AMC) 上的平均表现均优于所有无标签基线,并在大多数情况下超越了 GT-Reward (真值奖励)。这尤其体现在 Qwen2.5-7B 上,JURY-RL 的平均数学推理得分达到 48.13%,高于 GT-Reward 的 46.60%。这验证了其“真理对齐”和“优化稳定性”的有效性。
- 域外泛化能力: 在代码生成 (LiveCodeBench, CRUX)、指令遵循 (IFEval) 和多任务 (MMLU-Pro) 等域外任务上,JURY-RL 同样表现出色,在 Qwen2.5-7B 上整体平均得分最高,达到 44.72%,再次超过 GT-Reward 的 42.64%。这表明 JURY-RL 学到的推理能力具有良好的泛化性,不仅仅局限于数学领域。
- 无标签基线的挑战: 其他无标签方法(如 Self-Certainty, Entropy, Majority-Voting, CoReward, LLM-KD, LLM-as-a-Judge)虽然在某些任务上可能有所提升,但总体表现不如 JURY-RL 稳定和强大,且普遍低于甚至接近或低于 GT-Reward。这印证了论文中关于这些方法可能导致奖励黑客攻击和训练崩溃的论断。
- JURY-RL 相对于 GT-Reward 的优势: JURY-RL 能够超越 GT-Reward,暗示了形式化验证的奖励信号可能比直接的人工标注真值提供了一个更纯净、更鲁棒的学习目标,因为它迫使模型学习底层的、可泛化的正确性,而非仅是表面上的匹配。
6.3. 消融实验/参数分析
6.3.1. ResZero 消融研究 (Ablation Studies of ResZero)
为了评估 ResZero 奖励机制的有效性,论文比较了在证明门控框架下,当 (验证不确定)时,三种备用设计:零奖励 (Zero Reward)、MV 奖励 (MV Reward) 和本文提出的 ResZero。同时,GT 和 Majority-Voting 作为参考。
以下是原文 [Table 2] 的结果: Table 2: Ablation results for the proposed ResZero reward () on reasoning benchmark.
| Methods | Mathematics | Code | Instruction | Multi-Task | Average | |||||
|---|---|---|---|---|---|---|---|---|---|---|
| AIME24 | AIME25 | MATH500 | GSM8K | AMC | LiveCode | CRUX | IFEval | MMLU-Pro | ||
| Qwen3-1.7B-Base | ||||||||||
| GT-Reward | 10.00_{2 . 5 . 6} |
0.00_{2 . 0 . 0} |
68.2_{2 . 2 . 1} |
83.09_{2 . 1 . 0} |
34.94_{2 . 5 . 2} |
14.84_{2 . 0 . 9} |
33.75_{2 . 1 . 7} |
38.70_{2 . 1 . 0} |
39.43_{2 . 0 . 4} |
35.88_{2 . 2 . 0} |
| Majority-Voting | 3.33_{2 . 3 . 3} |
0.00_{2 . 0 . 0} |
59.8_{2 . 2 . 2} |
81.88_{2 . 1 . 1} |
33.73_{2 . 5 . 2} |
14.29_{2 . 0 . 9} |
32.75_{2 . 1 . 7} |
37.16_{2 . 1 . 0} |
35.68_{2 . 0 . 4} |
33.18_{2 . 1 . 8} |
| Proof-Gate + Zero Reward | 3.33_{2 . 3 . 3} |
6.67_{2 . 4 . 0} |
69.0_{2 . 2 . 1} |
83.70_{2 . 1 . 0} |
36.14_{2 . 5 . 3} |
14.82_{2 . 0 . 9} |
30.63_{2 . 1 . 8} |
37.07_{2 . 1 . 0} |
37.40_{2 . 0 . 4} |
35.42_{2 . 2 . 3} |
| Proof-Gate + MV Reward | 0.00_{2 . 0 . 0} |
0.00_{2 . 0 . 0} |
41.2_{2 . 2 . 2} |
82.87_{2 . 1 . 0} |
8.43_{2 . 2 . 0} |
14.48_{2 . 0 . 9} |
34.00_{2 . 1 . 7} |
36.78_{2 . 1 . 0} |
35.33_{2 . 0 . 4} |
28.12_{2 . 1 . 1} |
| JURY-RL (Proof-Gate + ResZero) | 13.33_{2 . 6 . 3} |
6.67_{2 . 4 . 0} |
68.4_{2 . 2 . 1} |
83.32_{2 . 1 . 0} |
36.14_{2 . 5 . 3} |
14.54_{2 . 0 . 9} |
35.00_{2 . 1 . 7} |
36.55_{2 . 1 . 0} |
38.11_{2 . 0 . 4} |
36.90_{2 . 2 . 0} |
| Llama-3.2-3B-Instruct | ||||||||||
| GT-Reward | 13.33_{2 . 6 . 3} |
0.00_{2 . 0 . 0} |
48.0_{2 . 2 . 2} |
76.72_{2 . 1 . 2} |
22.89_{2 . 4 . 0} |
7.05_{2 . 0 . 0} |
32.62_{2 . 1 . 7} |
50.16_{2 . 1 . 1} |
34.26_{2 . 0 . 4} |
31.67_{2 . 2 . 0} |
| Majority-Voting | 10.00_{2 . 5 . 6} |
0.00_{2 . 0 . 0} |
47.0_{2 . 2 . 2} |
79.08_{2 . 1 . 1} |
19.28_{2 . 4 . 3} |
8.11_{2 . 0 . 7} |
31.87_{2 . 1 . 6} |
48.36_{2 . 1 . 1} |
33.94_{2 . 0 . 4} |
30.85_{2 . 1 . 9} |
| Proof-Gate + Zero Reward | 3.33_{2 . 3 . 3} |
0.00_{2 . 0 . 0} |
51.4_{2 . 2 . 2} |
78.85_{2 . 1 . 1} |
21.69_{2 . 4 . 5} |
6.81_{2 . 0 . 6} |
30.12_{2 . 1 . 6} |
50.12_{2 . 1 . 1} |
33.27_{2 . 0 . 4} |
30.62_{2 . 1 . 6} |
| Proof-Gate + MV Reward | 10.00_{2 . 5 . 6} |
0.00_{2 . 0 . 0} |
47.4_{2 . 2 . 2} |
79.23_{2 . 1 . 1} |
25.30_{2 . 4 . 8} |
7.07_{2 . 0 . 6} |
31.37_{2 . 1 . 6} |
48.49_{2 . 1 . 1} |
33.68_{2 . 0 . 4} |
31.39_{2 . 1 . 9} |
| JURY-RL (Proof-Gate + ResZero) | 16.67_{2 . 0 . 9} |
0.00_{2 . 0 . 0} |
49.0_{2 . 2 . 2} |
80.74_{2 . 1 . 1} |
24.10_{2 . 4 . 7} |
6.16_{2 . 0 . 9} |
32.62_{2 . 1 . 7} |
50.09_{2 . 1 . 1} |
34.54_{2 . 0 . 4} |
32.66_{2 . 2 . 1} |
| Qwen2.5-7B | ||||||||||
| GT-Reward | 13.33_{2 . 6 . 3} |
6.67_{2 . 4 . 0} |
76.4_{2 . 1 . 0} |
89.61_{2 . 0 . 9} |
46.99_{2 . 5 . 5} |
12.78_{2 . 0 . 7} |
51.38_{2 . 1 . 8} |
41.50_{2 . 1 . 0} |
45.09_{2 . 0 . 4} |
42.64_{2 . 2 . 6} |
| Majority-Voting | 10.00_{2 . 5 . 6} |
3.33_{2 . 3 . 3} |
71.4_{2 . 2 . 0} |
90.22_{2 . 0 . 8} |
38.55_{2 . 5 . 3} |
18.37_{2 . 0 . 9} |
52.38_{2 . 1 . 8} |
42.72_{2 . 1 . 0} |
43.83_{2 . 0 . 4} |
41.20_{2 . 2 . 4} |
| Proof-Gate + Zero Reward | 13.33_{2 . 6 . 3} |
6.67_{2 . 4 . 0} |
75.8_{2 . 1 . 0} |
90.67_{2 . 0 . 8} |
39.76_{2 . 5 . 1} |
18.14_{2 . 0 . 9} |
52.25_{2 . 1 . 8} |
41.67_{2 . 1 . 0} |
47.88_{2 . 0 . 4} |
42.91_{2 . 3 . 0} |
| Proof-Gate + MV Reward | 0.00_{2 . 0 . 0} |
0.00_{2 . 0 . 0} |
51.6_{2 . 2 . 2} |
89.69_{2 . 0 . 8} |
16.87_{2 . 4 . 1} |
17.29_{2 . 0 . 9} |
53.25_{2 . 1 . 8} |
43.64_{2 . 1 . 0} |
35.01_{2 . 0 . 4} |
34.15_{2 . 1 . 2} |
| JURY-RL (Proof-Gate + ResZero) | 13.33_{2 . 6 . 3} |
13.33_{2 . 6 . 3} |
74.6_{2 . 1 . 0} |
91.21_{2 . 0 . 8} |
48.19_{2 . 5 . 5} |
14.69_{2 . 0 . 8} |
55.62_{2 . 1 . 0} |
41.51_{2 . 1 . 0} |
50.00_{2 . 0 . 4} |
44.72_{2 . 2 . 8} |
分析:
- ResZero 的优越性: ResZero 在所有骨干模型上均取得了最高的平均得分。它平均优于零奖励 +1.8 点,优于 MV 奖励 +6.9 点,甚至超越了 GT +1.4 点。
- MV 奖励的缺陷: MV 奖励(Proof-Gate + MV Reward)表现最差,在 Qwen3-1.7B-Base 上平均仅为 28.12%,Qwen2.5-7B 上为 34.15%。这证实了奖励未经验证的多数共识是欺骗性的,会导致模型强化自身错误并崩溃。
- 零奖励的局限性: 零奖励(Proof-Gate + Zero Reward)虽然避免了错误强化,但其性能次优,因为它在验证不确定时未能提供有效的学习信号,导致学习过程停滞,效率低下。
- ResZero 的平衡性: ResZero 通过在危险强化和低效停滞之间找到平衡,提供了一个鲁棒的解决方案。它既惩罚了未经验证的多数,又在剩余答案中保留了有用的学习信号,从而维持了有效的优化梯度。
6.3.2. 训练稳定性 (Stable Training)
为了评估训练稳定性,论文追踪了 JURY-RL 与主要无标签基线在 MATH5000 验证集上整个训练过程中的准确率。
以下是原文 [Figure 2] 的结果:
Figure 2: Accuracy on MATH5000 Validation set over training steps.
分析:
- 无标签基线的崩溃: 从 Figure 2 中可以看出,熵最小化 (Entropy) 和自我确信度 (Self-Certainty) 在初始性能提升后出现了崩溃,这表明模型开始强化虚假共识。LLM-as-a-Judge/LLM-KD/Majority-Voting 也表现出噪声大且次优的收敛。
- JURY-RL 的稳定提升: 相比之下,JURY-RL 展示了稳定、单调的性能提升。这证实了其证明门控奖励机制有效地防止了自监督方法中常见的模式崩溃。
6.3.3. 多样性增强 (Diversity Enhancement)
论文探究了 JURY-RL 是否能增强解决方案的多样性。
以下是原文 [Table 3] 的结果: Table 3: Performance of JURY-RL vs. GT-Reward on math reasoning tasks (pass@k and pass@1). for AIME, for MATH500 and GSM8K, and for AMC.
| Model | Average (pass@k) | | | Average (pass@1) | | | --- | --- | --- | --- | --- | --- | --- | | GT-Reward | JURY-RL | | GT-Reward | JURY-RL | | Qwen3-1.7B-Base | 55.36 | 59.41 | +4.05 | 39.25 | 41.57 | +2.32 | Llama-3.2-3B-Instruct | 45.46 | 48.48 | +3.02 | 32.19 | 34.10 | +1.91 | Qwen2.5-7B | 62.48 | 64.04 | +1.56 | 46.60 | 48.13 | +1.53
以下是原文 [Figure 3] 的结果:
Figure 3: Average unique answers per sample over training steps on Qwen3-1.7B-Base.
分析:
pass@k显著提升: Table 3 显示 JURY-RL 在pass@k上的提升显著大于pass@1(例如,Qwen3-1.7B-Base 上pass@k提升 +4.05 pp,而pass@1提升 +2.32 pp)。这表明 JURY-RL 增加了解决方案的多样性。- ResZero 机制的作用: 这种多样性的提升源于 ResZero 奖励机制,它惩罚有缺陷的共识,并将奖励重新分配给探索性的替代推理路径。这积极对抗了模式崩溃,并激励了探索。
- 视觉确认: Figure 3 进一步证实了这一点,它追踪了训练过程中每个问题生成的平均唯一答案数量。像 Majority-Voting 这样的基线很快就遭受了模式崩溃——收敛到单一答案——而 JURY-RL 保持了高水平的多样性,这表明其鲁棒性。
6.3.4. 验证器信号质量 (Verifier Signal Quality)
论文分析了 Lean 验证器与 LLM 作为判官的信号质量。
以下是原文 [Table 4] 的结果: Table 4: Verifier signal quality on training set. All metrics reported in percent (%).
| Verifier | Prec. | Rec. | F1 |
|---|---|---|---|
| LLM-as-a-Judge | 75.9 | 96.1 | 84.8 |
| Lean Verifier (Ours) | 84.5 | 88.0 | 86.2 |
以下是原文 [Figure 6] 的结果:
Figure 6: Training dynamics of precision, recall, validation accuracy, and training entropy under different Lean pass@k verification settings.
分析:
- Lean 验证器的高精确率: Table 4 显示,Lean 验证器提供了优于 LLM-as-a-Judge 的奖励信号,具有更高的精确率 (84.5% vs. 75.9%)。尽管召回率略低 (88.0% vs. 96.1%),但高精确率至关重要,因为它能大幅减少假阳性,防止奖励黑客攻击,并使训练目标与可验证的正确性紧密对齐。
- F1-分数优势: Lean 验证器更高的 F1-分数 (86.2%) 证实了其更好的整体平衡性,验证了“证明处置”原则中对信号保真度的优先考虑,以实现稳定学习。
- Lean 验证器的不完美性及其来源: 论文指出,Lean 验证器的精确率未达到完美的 100% 并非其核心逻辑缺陷,而是源于上游的自动形式化和一致性检查等组件可能引入的误差。
pass@k对召回率的影响: Figure 6 显示,召回率随验证尝试次数 的增加而增加。单次尝试 (pass@1) 的召回率较低(约 30%),但在pass@16时能达到近 90%。这意味着多次尝试可以显著提高发现正确答案的机会。- 高精确率是主导因素: 尽管召回率有较大波动,但最终的验证准确率和训练熵在不同的 值下收敛到相似的稳定状态,这表明验证器信号的高精确率是成功和稳定训练的主导因素。这与 LLM-as-a-Judge 形成鲜明对比,后者的错误是其概率性和不透明推理过程固有的。
6.3.5. 超参数 的影响 (Impact of )
论文分析了超参数 (在 Eq. 5 中控制对未经验证的多数提议的惩罚强度)的影响。
以下是原文 [Figure 4] 的结果:
Figure 4: Training dynamics under different values of the hyperparameter .
分析:
- 对多样性的影响: Figure 4 的右侧面板清楚地表明,非零的 对于维持解决方案的多样性至关重要。当 时,框架实际上退化为零奖励备用方案,导致随着训练的进行,平均唯一答案数量急剧下降——这是模型收敛到虚假共识的典型症状。相比之下,任何正的 值都成功地保持了高水平的多样性。
- 对性能的权衡: 左侧和中心面板揭示了一个微妙的权衡:过于激进的惩罚(例如 )可能会略微抑制最终奖励和准确率。这表明,虽然惩罚对于探索至关重要,但过高的值可能会过度限制策略利用潜在正确的、高共识答案。
- 最佳平衡点: 这种消融实验验证了适度调整的 值(例如实验中使用的 )能够实现最佳平衡,确保鲁棒的训练稳定性、解决方案多样性,同时不损害主要任务目标的收敛。
6.3.6. Lean 验证器的性能和成本分析
论文在附录 C.3 中提供了 Lean 验证器不同配置下的性能和词元成本分析。
以下是原文 [Table 5] 的结果: Table 5: Performance and token cost analysis of Lean Verifier across different Prover configurations.
| Models | MATH500 | | | Token Costs | |
| :-- | :--: | :--: | :--: | :--: | :--: | :--:
| | ACC | TPR | F1-Score | Max Tokens per Verify | Avg Tokens per Verify | Avg Tokens per Response
| Prover@16 | 87.0 | 87.0 | 93.0 | 351,799 | 33,346 | 5,858
| Prover@32 | 89.0 | 89.0 | 94.0 | 658,061 | 52,064 | 6,607
| Prover@64 | 91.0 | 91.0 | 95.0 | 1,369,038 | 67,429 | 6,435
分析:
- 性能与成本的权衡: Table 5 显示,
Prover@64配置虽然实现了最高的准确率 (91.0% ACC),但其计算成本最高,平均每次验证消耗 67,429 个词元。相比之下,Prover@16配置在性能上略有下降(87.0% ACC),但其词元成本降低了一半以上(33,346)。 - 实验选择: 鉴于这种权衡,论文选择
Prover@16作为主要实验的默认配置,以在可接受的性能下降和显著的成本节约之间取得平衡,确保效率。
6.4. 案例研究 (Case Study)
为了阐明“证明处置”原则,论文提供了一个对比 LLM-as-a-Judge 和 Lean 形式化验证器的案例研究(参见附录 H)。
问题: 让 和 是正实数,使得 。求 的最大值。 答案: 1152
LLM-as-a-Judge 输出 (判官错误): LLM-as-a-Judge (Judge Wrong) 进行了复杂的微积分和对称性分析,最终得出了一个与 1152 不匹配的错误值 (357.06...),并最终判断原始答案 1152 为“False”。 LLM-as-a-Judge 的推理过程存在错误,例如它假设 来简化问题,而这并不适用于所有最大值情况。 这一案例表明,LLM 判官的可靠性受限于其自身的推理能力。当 LLM 判官的推理有缺陷时,它会生成不正确的训练信号。
Lean Prover 输出 (证明成功):
Lean Prover 则成功证明了最大值为 1152。它使用了算术几何平均不等式 (AM-GM inequality) 和严格的代数推导,例如证明了 1152 是函数值集合的上确界 (supremum)。
这一案例突出表明,一旦自动形式化和一致性检查通过,Lean 证明器能够通过形式逻辑提供确定且高度可靠的信号,具有零假阳性。
分析: 该案例研究直观地验证了 JURY-RL 的核心主张:Lean 验证器在信号保真度方面优于 LLM-as-a-Judge。即使 LLM-as-a-Judge 看起来进行了详细的“推理”,但其最终判断可能因为推理错误而不可靠。相反,Lean Prover 凭借其形式化验证的严格性,提供了无可辩驳的正确性证明。这正是 JURY-RL 选择“证明处置”最终奖励的原因,以确保学习信号的可靠性。
6.5. Pass@k 结果补充
以下是原文 [Table 7] 的结果: Table 7: Pass@k Results (%) of RL performance comparison on math reasoning benchmarks.
| Methods | AIME24 pass@16 |
AIME25 pass@16 |
MATH500 pass@4 |
GSM8K pass@4 |
AMC pass@8 |
Average |
|---|---|---|---|---|---|---|
| Qwen3-1.7B-Base | ||||||
| Before RL | ||||||
| GT-Reward | ||||||
| Entropy | ||||||
| Self-Certainty | ||||||
| Majority-Voting | ||||||
| CoReward | ||||||
| LLM-KD | ||||||
| LLM-as-a-Judge | ||||||
| JURY-RL (Ours) | ||||||
| Llama-3.2-3B-Instruct | ||||||
| Before RL | ||||||
| GT-Reward | ||||||
| Entropy | ||||||
| Self-Certainty | ||||||
| Majority-Voting | ||||||
| CoReward | ||||||
| LLM-KD | ||||||
| LLM-as-a-Judge | ||||||
| JURY-RL (Ours) | ||||||
| Qwen2.5-7B | ||||||
| Before RL | ||||||
| GT-Reward | ||||||
| Entropy | ||||||
| Self-Certainty | ||||||
| Majority-Voting | ||||||
| CoReward | ||||||
| LLM-KD | ||||||
| LLM-as-a-Judge | ||||||
| JURY-RL (Ours) |
分析:
Table 7 补充了 JURY-RL 在数学推理基准上的 pass@k 结果,进一步证实了其有效性。
- JURY-RL 的
pass@k优势: 在所有三个骨干模型上,JURY-RL 在pass@k上的平均表现均优于所有无标签基线,并且在大多数情况下超越了 GT-Reward。例如,在 Qwen2.5-7B 上,JURY-RL 的pass@k平均得分达到 64.04%,高于 GT-Reward 的 62.48%。 - 多样性验证: 结合 Table 3 的
pass@k相对pass@1的更大增益,Table 7 进一步强调了 JURY-RL 通过其 ResZero 机制有效鼓励模型探索多样化的解决方案路径,从而避免了模式崩溃。这种在多次尝试下解决问题的能力是模型深层推理能力和鲁棒性的体现。 - 无标签方法的
pass@k表现: 其他无标签方法在pass@k上的表现也印证了pass@1的趋势,即 JURY-RL 提供了更稳定和更强大的性能。
7. 总结与思考
7.1. 结论总结
本文提出了 JURY-RL,一个新颖的无标签可验证奖励强化学习 (RLVR) 框架。该框架的核心思想是 “票选提议,证明处置 (Votes Propose, Proofs Dispose)”,即通过 推演 (rollouts) 的多数投票来提议候选答案,而由形式化的 Lean 验证器来处置最终奖励。为了解决验证不确定时学习信号缺失的问题,JURY-RL 引入了 ResZero (Residual-Zero) 奖励机制,该机制放弃不可验证的多数提议,并为剩余答案分配零均值、保留方差的奖励。
JURY-RL 的设计成功地实现了三个关键目标:
-
可扩展性: 无需昂贵的人工标注,通过自动化验证流程降低成本。
-
真理对齐: 奖励信号基于形式化验证的客观正确性,而非模糊的共识或主观判断。
-
优化稳定性: 即使验证结果不确定,ResZero 奖励也能提供稳定的学习梯度,防止训练崩溃或停滞。
实验结果表明,JURY-RL 在数学推理、代码生成和多任务基准测试中,训练过程更加稳定,性能显著优于现有的无标签基线。更值得注意的是,JURY-RL 的性能甚至能够匹敌或超越使用真值奖励的监督训练,尤其是在
pass@k指标上表现出更强的解决方案多样性和泛化能力。这项工作证实了将强化学习与稀疏但形式化验证的信号相结合,是构建鲁棒且可泛化推理模型,同时摆脱人类标签依赖的有效策略。
7.2. 局限性与未来工作
论文作者指出了 JURY-RL 框架的潜在局限性,并展望了未来的研究方向:
- 验证器上游组件的缺陷: 形式化验证器(如 Lean)本身在逻辑上是健全的,但其在实际应用中的不完美性主要来源于上游组件,例如将自然语言问题转换为形式化规范的 自动形式化器 (autoformalization) 和确保语义一致性的 一致性检查器 (consistency checks)。这些组件可能引入误差,导致验证器信号的精确率无法达到 100%。
- 未来工作: 改进自动形式化和一致性检查的鲁棒性,以进一步提升验证器信号的质量。这可能包括开发更先进的 LLM 工具来辅助这些翻译和检查过程,或集成更多领域知识来提高转换的准确性。
7.3. 个人启发与批判
7.3.1. 个人启发
- 形式化验证在 LLM 推理中的巨大潜力: JURY-RL 巧妙地将形式化验证的严格性引入到 LLM 的强化学习中,为解决 LLM 推理中的“幻觉”和不可靠性问题提供了强有力的方法。它指出了一个重要的方向:未来的 LLM 不仅要“会说”,更要“能证明”。
- “票选提议,证明处置”范式的巧妙: 这种分离决策机制,既利用了多数投票的计算效率来筛选最有希望的候选答案(proposal),又通过形式化验证的可靠性来确保奖励的准确性(disposal),在可扩展性和真理对齐之间取得了精妙的平衡。
- ResZero 奖励的创新性: 在验证不确定的“灰色地带”中,ResZero 奖励能够提供有意义的学习信号,避免了训练停滞或强化虚假共识。这种零均值、方差保留的设计对于稀疏奖励环境下的强化学习具有普遍的借鉴意义。它鼓励探索,惩罚无用的高共识,这在很多需要多样化解决方案的领域都很有用。
- 超越监督学习的可能性: JURY-RL 在某些任务上超越了真值奖励的监督学习基线,这表明形式化验证的信号可能比人类标注的真值更“纯粹”,因为它强制模型学习底层的、可泛化的正确性,而非仅仅是表面匹配或过拟合特定数据集的“捷径”。
7.3.2. 批判与潜在改进
- Lean 验证器的计算成本: 尽管论文通过缓存和
Prover@16优化了成本,但 Lean 形式化验证的计算开销依然显著(特别是冷启动阶段)。对于对实时性要求高或资源受限的应用场景,这种成本可能仍然是一个障碍。- 改进方向: 探索混合验证策略,例如,在训练早期或对置信度低的答案使用轻量级、快速但不那么严格的验证器,而只对高置信度或关键决策使用 Lean 验证。或者,研究如何更高效地并行化验证过程。
- Lean 验证器的适用范围: Lean 证明器主要擅长数学和逻辑推理。对于更广泛的 RLVR 任务,例如需要与复杂外部 API 交互、涉及物理世界模拟或模糊语义的场景,形式化验证的适用性和成本效益会降低。
- 改进方向: 开发或集成特定领域的形式化验证工具,或者将 JURY-RL 的思想推广到更广义的“可信评估器 (trusted evaluator)”概念,例如,在代码生成中使用严格的单元测试套件作为“证明处置”者。
- 超参数 的敏感性: 论文提到超参数 的选择对于平衡探索和利用至关重要。一个固定的 值可能无法在所有任务或训练阶段都达到最优。
- 改进方向: 引入自适应 值策略,例如,根据训练进展、模型性能或验证不确定样本的比例动态调整 。
- 自动形式化和一致性检查的瓶颈: 论文指出当前验证器精确率的限制主要来自上游的自动形式化和一致性检查器。这意味着 LLM 在将自然语言转换为形式逻辑方面仍有提升空间。
- 改进方向: 进一步研究如何利用更强大的 LLM 或多模态 LLM 来提高自动形式化和一致性检查的准确性和鲁棒性,甚至可以考虑将这些上游组件本身作为 RL 训练的一部分进行优化。
- 样本效率: 虽然 GRPO 和 ResZero 旨在提高样本效率,但在稀疏奖励环境中,尤其是在 Lean 验证失败率较高的情况下,模型学习所需的数据量可能仍然巨大。
- 改进方向: 结合元学习 (meta-learning) 或离线强化学习 (offline RL) 技术,以在数据不充足或验证成本高昂的情况下更有效地学习。
相似论文推荐
基于向量语义检索推荐的相关论文。