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

Motivation

• Known: RLVR은 program execution, unit test, 수학적 검증 등 externally checkable 신호를 이용해 LLM의 추론 능력을 향상시키지만, 대개 사람이 주석한 정답(ground-truth answer)이나 정교하게 만들어진 reward specification에 의존한다. Label-free 대안인 majority voting, self-certainty, entropy minimization, LLM-as-a-Judge 등은 주석 비용을 없애지만 합의(consensus)나 confidence를 정답성 대신 최적화하게 되어 false positive와 reward hacking, training collapse에 취약하다.
• Gap: 기존 label-free 방법들은 scalability는 달성하지만 truth-alignment를 희생하거나(majority voting), truth-alignment와 optimization stability 모두에서 문제를 겪는다(LLM-as-a-Judge). 즉 scalable, truth-aligned, optimization-stable이라는 세 조건을 동시에 만족하는 label-free reward 설계가 부재했다.
• Why: 사람이 주석한 ground-truth 없이도 안정적이고 정답에 정합적인 RLVR 학습이 가능해지면, 대규모 unlabeled 데이터를 활용한 LLM reasoning 향상의 비용을 크게 줄이면서도 reward hacking 위험을 억제할 수 있어 실용적 가치가 크다.
• Approach: JURY-RL은 answer proposal(다수결 투표, Jury)과 reward disposal(Lean 기반 정형 검증, Judge)을 분리(decouple)하여, 다수결로 제안된 답안이 Lean에서 검증(verify)될 때만 해당 답안을 낸 rollout에 양의 보상을 주고, 검증이 inconclusive할 경우 ResZero(Residual-Zero) fallback 보상으로 학습 gradient의 안정성을 유지한다.

Achievement

Figure 3. Accuracy on MATH5000 validation set over training steps.

1. Label-free 방법 대비 성능 우위: 수학 추론 벤치마크에서 majority voting, self-certainty 등 기존 label-free baseline들을 능가함.
2. Transfer 성능: math 데이터로만 학습했음에도 code generation 및 general benchmark로 성능이 전이(transfer)됨.
3. TTRL 세팅에서의 우위: test-time RL(TTRL) 설정에서 majority-vote baseline을 능가함.
4. 지도학습 수준의 성능 및 다양성 우위: supervised ground-truth 학습과 pass@1에서 동등한 성능을 보이면서 pass@k와 response diversity에서는 이를 상회함.

How

Figure 4. The pipeline of our Lean Verifier: a collaborative system that combines autoformalization, formal verification

• Group Relative Policy Optimization (GRPO) 프레임워크 위에서 각 문제 x에 대해 G개의 rollout을 샘플링하고, deterministic extractor ans(·)로 후보 답안을 추출함.
• Jury(다수결 투표)가 rollout들 중 plurality-voted answer를 후보로 propose.
• Lean 기반 verifier(Judge)가 이 단일 후보에 대해서만 formal verification을 수행하여 verify(x,a)∈{0,1} 오라클로 보상을 dispose, 매 rollout마다가 아니라 그룹당 단일 검증 호출만 필요해 scalability 확보.
• 검증 성공(δ=1) 시 해당 답안을 생성한 rollout에만 양의 보상 부여, 나머지는 0.
• 검증 불확실(δ=0, inconclusive) 시, 검증되지 않은 plurality 답안은 폐기하고 residual(잔여) 답안들에 대해 zero-mean, variance-preserving 신호를 재분배하는 ResZero fallback reward를 적용, GRPO의 group-normalized advantage 계산이 붕괴하지 않도록 유지.
• Lean Verifier는 autoformalization과 proof-search를 결합한 collaborative pipeline으로 구성됨(Figure 4).
• 세 가지 backbone 모델을 수학 데이터로 학습하여 검증.

Originality

• Answer proposal(투표)과 reward disposal(정형 검증)을 명시적으로 decouple한 "Votes Propose, Proofs Dispose" 패러다임을 새롭게 제시.
• 매 후보 답안이 아니라 group당 단일 정형 검증 호출만 필요하도록 설계하여, 기존 generate-then-verify 파이프라인의 verification 실패 시 학습 신호 부재 문제를 해결.
• ResZero라는 zero-mean, variance-preserving fallback reward를 도입해 GRPO의 grouped advantage 붕괴를 막으면서도 unverifiable consensus를 강화하지 않는 독창적 보상 설계.
• LLM-as-a-Judge 대신 Lean이라는 formal proof assistant를 label-free RLVR의 최종 accept 메커니즘으로 사용한 점.

Limitation & Further Study

• Lean 기반 검증은 autoformalization과 proof-search에 의존하므로, 답이 맞아도 formalization 실패로 verify가 0이 되는 경우(잘못된 negative)가 존재할 수 있어 verification coverage의 한계가 남아있음.
• 실험이 수학(및 일부 코드/일반) 도메인에 국한되어, formal verifier가 존재하지 않는 open-domain reasoning task로의 일반화는 불명확함.
• Lean verifier 호출에 따른 계산 오버헤드(latency, 인프라 비용)에 대한 상세한 비용-효율 분석이 부족해 보임.
• 후속 연구로 다양한 도메인에 적용 가능한 verifier 확장, autoformalization 정확도 개선, ResZero의 이론적 수렴 보장에 대한 심화 분석이 필요.

Evaluation

총평: 투표와 정형 검증을 분리하는 아이디어와 ResZero fallback 설계가 label-free RLVR의 안정성과 정답 정합성 문제를 실용적으로 해결한 인상적인 워크숍 논문이며, 다만 Lean 의존성으로 인한 도메인 일반화 한계는 추가 검증이 필요하다.