Search papers, labs, and topics across Lattice.
JURY-RL, a novel label-free Reinforcement Learning with Verifiable Rewards (RLVR) framework, decouples answer proposal (via majority voting) from reward disposal (via formal verification). When a candidate answer is successfully verified in Lean, only rollouts matching the plurality-voted answer are rewarded; otherwise, a ResZero fallback reward redistributes a zero-mean signal over the residual answers. Experiments across mathematical reasoning, code generation, and general benchmarks demonstrate that JURY-RL outperforms other label-free baselines and achieves performance comparable to supervised ground-truth training, with improved generalization.
Ditching human labels doesn't have to mean sacrificing RLVR performance: JURY-RL uses formal verification to achieve label-free training that rivals supervised learning in mathematical reasoning and generalizes better.
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.
