JURY-RL: Votes Propose, Proofs Dispose for Label-Free RLVR

📄 arXiv: 2604.25419v1 📥 PDF

作者: Xinjie Chen, Biao Fu, Jing Wu, Guoxin Chen, Xinggao Liu, Dayiheng Liu, Minpeng Liao

分类: cs.AI

发布日期: 2026-04-28

备注: Preprint. 32 pages, 9 figures

💡 一句话要点

JURY-RL：基于投票提议与形式化验证的无标签强化学习

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 强化学习 可验证奖励 无标签学习 形式化验证 数学推理 代码生成 大型语言模型

📋 核心要点

  1. 传统RLVR依赖人工标注或奖励设计，成本高且易引入偏差，限制了其在可机器验证领域的应用。
  2. JURY-RL通过投票提议答案，形式化验证奖励，并引入ResZero机制，避免了对不可验证共识的强化。
  3. 实验表明，JURY-RL在数学推理、代码生成和通用基准测试中均优于其他无标签方法，泛化能力更强。

📝 摘要（中文）

本文提出了一种无标签的强化学习框架JURY-RL，用于增强大型语言模型（LLM）的推理能力。传统的基于可验证奖励的强化学习（RLVR）依赖于人工标注或精心设计的奖励规范。JURY-RL通过解耦答案提议和奖励处置来解决这个问题：模型rollout的投票提出候选答案，然后形式化验证器确定该候选答案是否可以获得正奖励。具体来说，只有与多数投票答案匹配的rollout，且该答案在Lean中成功验证时，才会获得奖励。当验证结果不确定时，采用ResZero（Residual-Zero）作为后备奖励，丢弃未验证的多数投票提议，并在剩余答案上重新分配零均值、方差保持的信号。这种设计保持了稳定的优化梯度，避免了强化不可验证的共识。在数学数据上训练的三个backbone模型上，JURY-RL始终优于其他无标签基线，并在数学推理基准测试中表现出色，并能有效迁移到代码生成和通用基准测试。它获得了与监督式ground-truth训练相当的pass@1性能，并通过更高的pass@k和响应多样性展示了卓越的泛化能力。

🔬 方法详解

问题定义：论文旨在解决在可机器验证领域，标准RLVR方法依赖人工标注或奖励设计带来的高成本和潜在偏差问题。现有无标签方法，如多数投票或LLM-as-a-judge，虽然降低了标注成本，但容易引入假阳性，导致训练不稳定。

核心思路：JURY-RL的核心思路是将答案的生成（proposal）和奖励的分配（disposal）解耦。通过多数投票机制生成候选答案，然后使用形式化验证器（如Lean）来验证该答案的正确性。只有通过验证的答案才能获得奖励，从而避免了对错误答案的强化。当验证结果不确定时，采用ResZero机制，避免训练崩溃。

技术框架：JURY-RL的整体框架包含以下几个主要阶段： 1. Rollout生成：使用强化学习策略生成多个rollout，每个rollout对应一个答案。 2. 投票提议：对所有rollout的答案进行多数投票，选出得票最多的答案作为候选答案。 3. 形式化验证：使用形式化验证器（如Lean）验证候选答案的正确性。 4. 奖励分配：如果候选答案通过验证，则给所有生成该答案的rollout分配正奖励；如果验证失败，则使用ResZero机制分配奖励。 5. 策略更新：使用强化学习算法（如PPO）更新策略。

关键创新：JURY-RL的关键创新在于将投票机制和形式化验证相结合，并引入ResZero机制。与传统的无标签方法相比，JURY-RL能够更准确地识别和奖励正确的答案，避免了对错误答案的强化，从而提高了训练的稳定性和性能。ResZero机制是另一个创新点，它在验证不确定时，通过重新分配零均值、方差保持的信号，避免了训练崩溃。

关键设计： 1. 投票机制：采用多数投票，选择出现频率最高的答案作为候选答案。 2. 形式化验证器：使用Lean等形式化验证工具，验证候选答案的正确性。 3. ResZero机制：当验证结果不确定时，将奖励设置为零均值，并保持方差不变，重新分配给其他答案。具体实现方式未知，论文中未详细描述。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，JURY-RL在数学推理基准测试中优于其他无标签基线，并能有效迁移到代码生成和通用基准测试。JURY-RL获得了与监督式ground-truth训练相当的pass@1性能，并通过更高的pass@k和响应多样性展示了卓越的泛化能力。具体性能提升数据未知，论文中未给出详细的数值对比。

🎯 应用场景

JURY-RL可应用于需要高可靠性和可验证性的任务，例如数学推理、代码生成、定理证明等。该方法降低了对人工标注的依赖，使得强化学习能够更广泛地应用于这些领域。未来，JURY-RL可以扩展到其他可机器验证的领域，并与其他技术（如知识图谱、符号推理）相结合，进一步提高性能。

📄 摘要（原文）

Reinforcement learning with verifiable rewards (RLVR) enhances the reasoning of large language models (LLMs), but standard RLVR often depends on human-annotated answers or carefully curated reward specifications. In machine-checkable domains, label-free alternatives such as majority voting or LLM-as-a-judge remove annotation cost but can introduce false positives that destabilize training. We introduce JURY-RL, a label-free RLVR framework that decouples answer proposal from reward disposal: votes from model rollouts propose a candidate answer, and a formal verifier determines whether that candidate can receive positive reward. Concretely, only rollouts matching the plurality-voted answer are rewarded when that answer is successfully verified in Lean. When verification is inconclusive, we invoke ResZero (Residual-Zero), a fallback reward that discards the unverified plurality proposal and redistributes a zero-mean, variance-preserving signal over the residual answers. This design maintains a stable optimization gradient without reinforcing unverifiable consensus. Across three backbone models trained on mathematical data, JURY-RL consistently outperforms other label-free baselines on mathematical reasoning benchmarks and transfers competitively to code generation and general benchmarks. It attains pass@1 performance comparable to supervised ground-truth training, with superior generalization demonstrated by higher pass@k and response diversity.