Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection

Motivation

• Known: LLM은 final-answer 수학 문제에서 RLVR(reinforcement learning with verifiable rewards)을 통해 큰 성공을 거두었으며, GenSelect와 LLM-as-a-Judge 같은 생성적 검증(generative verification) 방법이 test-time compute scaling과 solution selection에 유망하다는 것이 알려져 있다.
• Gap: 그러나 LLM이 correct answer에 도달하더라도 순환 논증, 패턴 매칭, 허위 정리 생성 등 결함 있는 추론을 사용하는 경우가 많고, 단일 벤치마크에 의존한 평가는 취약하거나 오도하는 결론을 낳을 수 있으며, 기존 연구는 proof verification 방법들을 수백만 토큰 규모로 체계적으로 스케일링하거나 여러 평가 설정을 종합적으로 검토하지 않았다.
• Why: 엄밀한 증명 기반 수학(rigorous proof-based mathematics, 예: IMO, USAMO)으로 나아가기 위해서는 신뢰할 수 있는 proof verification 능력이 필수적이며, 이는 policy-gradient RL(GRPO 등)을 통한 proof generation 개선의 전제조건이 되기 때문에 중요하다.
• Approach: 여러 evaluation setup(proof-based 및 final-answer)을 결합한 다각적 평가 프레임워크를 구축하고, GenSelect와 LLM-as-a-Judge를 수백만 토큰 규모로 확장하여 조합한 결과를 분석했으며, 프롬프트 설계와 강화학습이 성능에 미치는 영향을 실증적으로 검토했다.

Achievement

Figure 1. Left: Training curves for RL training of Qwen3-30B-A3B-Thinking-2507 on the OPC dataset. (1) Different prompts

1. 다중 벤치마크 평가 프레임워크 구축: 단일 벤치마크 평가의 취약성을 실증적으로 보이고, VerProofArena를 비롯한 6개의 상호 보완적 데이터셋을 활용해 exploitable correlation과 소규모 데이터셋 문제를 완화하는 평가 체계를 제안했다.
2. LLM-as-a-Judge 프롬프트 민감도 및 RL의 효과 규명: 프롬프트 설계가 LLM-as-a-Judge 성능에 큰 영향을 미친다는 것을 보이고, 강화학습(RL) fine-tuning이 이러한 민감도를 효과적으로 줄일 수 있음을 확인했다.
3. GenSelect와 LLM-as-a-Judge 결합 프레임워크 제안: GenSelect 토너먼트와 parallel judgment 방식을 결합함으로써 개선된 compute-performance trade-off를 달성하는 최적의 test-time scaling 전략을 제시했다.
4. RL의 한계 발견: RL이 proof-level 지표(metric)는 개선하지만 final-answer precision은 향상시키지 못함을 보여, 현재 모델이 수학적 타당성보다 stylistic 혹은 procedural correctness에 보상을 부여하는 경향이 있음을 지적했다.

How

Figure 4. LLM-as-a-Judge performance on selecting the best proof among 8 generated proofs from SelOPC. A higher number o

• LLM-as-a-Judge와 GenSelect 두 가지 생성적 검증 패러다임을 정의하고, knockout tournament와 pairwise tournament 구조로 GenSelect의 selection 정확도-비용 trade-off를 분석함.
• 6개의 상호 보완적 데이터셋(VerProofArena 등, USAMO 2025·IMO 2025·IMC 2025 기반, MathArena 인간 라벨 포함)을 구성하여 proof-based와 final-answer reasoning을 모두 평가.
• LLM-as-a-Judge의 판정 수(nj)를 조절하며 sampled judgement를 평균 또는 다수결로 집계하는 방식으로 신뢰성을 높임.
• Qwen3-30B-A3B-Thinking-2507 등의 모델에 대해 RL(GRPO 계열)로 fine-tuning을 수행하고, 학습 곡선과 프롬프트 민감도 변화를 비교.
• Best-of-n proof selection 실험(SelProofBench, SelOPC 데이터셋 활용)과 GPT-OSS-120B 등 판별 모델을 활용한 8개 후보 중 최적 증명 선택 실험을 수행.

Originality

• 기존 연구들이 개별 벤치마크나 단일 검증 방법에 집중한 반면, 본 논문은 proof-based와 final-answer 평가를 결합한 다각적(multi-faceted) 평가 프레임워크를 최초로 체계화함.
• GenSelect와 LLM-as-a-Judge를 수백만 토큰 규모로 스케일링하고 이 둘을 결합하는 새로운 test-time scaling 전략(토너먼트+병렬 판정)을 제안한 점이 독창적임.
• RL fine-tuning이 프롬프트 민감도를 줄이지만 final-answer precision 향상에는 실패한다는 역설적 결과를 실증적으로 드러내, 현재 보상 체계가 stylistic/procedural correctness에 치우쳐 있다는 통찰을 제공함.

Limitation & Further Study

• 평가 및 학습에 사용된 모델(Qwen3-30B-A3B-Thinking-2507, GPT-OSS-120B 등)의 범위가 제한적이어서 더 다양한 아키텍처와 규모의 모델에 대한 일반화 가능성 검증이 필요함.
• proof verification의 human-labeled judgement에 의존하는 데이터셋(VerProofArena 등)의 라벨 품질과 편향(annotator bias)에 대한 심층 분석이 부족함.
• RL이 stylistic/procedural correctness에 보상을 주는 근본 원인에 대한 명확한 해결책이나 개선된 보상 설계는 제시되지 않아, 후속 연구에서 mathematical validity를 직접적으로 포착하는 보상 신호 설계가 필요함.
• 수백만 토큰 규모의 스케일링에 따른 계산 비용과 실제 배포 가능성에 대한 구체적 비용-효익 분석이 제한적임.

Evaluation

총평: 단일 벤치마크의 함정을 드러내고 GenSelect와 LLM-as-a-Judge를 대규모로 결합하여 proof verification/selection의 실용적 가이드라인을 제시한 견실한 연구로, RL의 한계에 대한 통찰이 특히 향후 연구에 중요한 시사점을 제공한다.