Proof-RM: A Scalable and Generalizable Reward Model for Math Proof

1. 연구 배경 및 문제 정의 (Problem)

• RLVR 의 한계: 최근 대규모 언어 모델 (LLM) 은 검증 가능한 보상 (Verifiable Rewards, RLVR) 을 통한 강화학습을 통해 수학 추론 능력을 크게 향상시켰습니다. 그러나 기존의 RLVR 은 주로 최종 정답 (숫자, 옵션 등) 을 정답과 비교하는 방식에 의존합니다. 이는 "검증의 비대칭성 (Asymmetry of Verification)"을 활용한 것으로, 문제를 푸는 것은 어렵지만 정답을 확인하는 것은 쉽습니다.
• 증명 기반 문제의 난제: 올림피아드나 연구 수준의 고급 수학 문제는 단순한 정답이 아닌 **완전한 증명 (Proof)**을 요구합니다. 이러한 경우 정답과 증명의 논리적 흐름을 일일이 확인해야 하므로 검증이 매우 어렵습니다.
• 기존 방법의 결함:
  • 전문가 의존: 현재proof 를 정확히 검증하는 유일한 방법은 인간 전문가의 수작업이지만, 이는 비용이 매우 비싸고 확장성이 없습니다.
  • 단순화 기법의 취약성: 증명을 검증하기 쉽게 변형하는 기존 연구들 (예: 부등식을 수치 추정으로 변환 등) 은 문제의 본질을 훼손하고, 모델이 증명 과정 없이 정답만 맞추는 '쇼트컷 학습 (Shortcut Learning)'을 유도하여 신뢰성을 떨어뜨립니다.
• 핵심 문제: 증명 과정 전체를 신뢰할 수 있게 평가하고, 이를 강화학습의 보상으로 활용하여 모델의 추론 능력을 안정적으로 향상시킬 수 있는 **확장 가능하고 일반화되는 보상 모델 (Reward Model, RM)**이 부재합니다.

2. 제안 방법론 (Methodology)

저자들은 Proof-RM을 개발하기 위해 데이터 수집 파이프라인과 RL 훈련 전략을 혁신적으로 설계했습니다.

A. 확장 가능한 데이터 수집 파이프라인 (Scalable Data Construction)

• 다양한 QPC(질문 - 증명 - 검증) 데이터 생성:
  • 다양성 확보: 올림피아드 문제 (IMO, USAMO, Putnam 등), 실제 학생 답안지, 다양한 LLM(DeepSeek-R1, GPT-5-mini, Gemini 등) 을 활용하여 질문과 증명을 생성합니다.
  • 생성 기법: 기존 증명을 재구성 (Rephrase), 마스킹 후 채우기 (Masked Generation), 증강 (Augment) 등의 방법을 통해 논리적 결함, 허위 명제, 불완전한 추론 등 다양한 유형의 **잘못된 증명 (Negative Samples)**을 대량으로 생성합니다.
• 계층적 인간 검증 (Hierarchical Human Check):
  • LLM 일관성 검증: 여러 LLM 을 사용하여 증명의 옳고 그름을 5 번 이상 검증하고, 만장일치 (Unanimous Agreement) 를 기준으로 라벨을初步 설정합니다.
  • 조합 단위 인간 샘플링: 모든 데이터를 인간이 검증하는 대신, 데이터 소스, 생성 방법, 모델별로 그룹을 나누어 샘플링합니다. 특정 그룹에서 LLM 과 인간의 검증 결과가 높은 일치도 (Threshold) 를 보이면 해당 그룹 전체를 '실버 표준 (Silver-standard)'으로 간주하고 훈련 데이터로 사용합니다. 이는 인간 검증 비용을 90% 이상 절감하면서도 데이터의 품질을 보장합니다.
  • 결과: 약 100 시간의 인간 노력으로 21,000 개 이상의 고품질 QPC triplet 데이터를 확보했습니다.

B. 안정화된 RLVR 훈련 알고리즘 (Stable RL Training)

• LLM-as-a-RM-for-RM (보상 모델에 대한 보상 모델):
  • 문제: 이진 분류 (True/False) 보상을 사용할 때, 모델이 논리적 오류는 있지만 정답을 맞춘 경우나, 반복적인 문장, 문법적 불일치 등 '표면적 결함'이 있더라도 정답을 맞출 경우 잘못된 보상을 받아 모델 붕괴 (Model Collapse) 가 발생합니다.
  • 해결: 별도의 LLM 을 사용하여 보상 모델의 **생성된 추론 과정의 유창성 (Fluency)**과 행동 일관성을 추가로 검증합니다. 논리적 내용보다는 반복, 논리적 순환, 맥락 무관한 토큰 삽입 등을 감지하여 이를 부정적인 보상으로 처리합니다.
• 균형 잡힌 토큰 가중치 (Balanced Token Weighting):
  • 문제: 기존 토큰 가중치 전략 (GRPO, DAPO 등) 은 모델의 출력 길이를 극단적으로 짧게 또는 길게 만드는 경향이 있어 훈련 불안정을 초래했습니다.
  • 해결: 시퀀스 수준과 토큰 수준의 가중치를 균형 있게 결합한 전략을 도입하여, 모델이 길이에 상관없이 안정적으로 학습하도록 합니다.

3. 주요 기여 (Key Contributions)

1. 증명 검증의 비대칭성 분석: 수학 문제 해결에서 '증명 과정'의 검증이 왜 필요한지, 그리고 기존 RLVR 의 한계를 명확히 지적했습니다.
2. 고품질 데이터 파이프라인 제안: 인간 검증 비용을 최소화하면서도 다양성과 정확성을 갖춘 대규모 QPC 데이터셋 구축 방법을 제시했습니다.
3. 안정적인 RL 훈련 레시피: 'LLM-as-a-RM-for-RM'과 '균형 토큰 가중치'를 통해 이진 보상을 사용하는 증명 검증 모델의 훈련 안정성과 확장성을 획기적으로 개선했습니다.

4. 실험 결과 (Results)

• 보상 정확도 (Reward Accuracy):
  • Proof-RM 은 베이스 모델 (Distill-Qwen3) 과 Frontier LLM(DeepSeek V3.1, Gemini-2.5-Flash 등) 을 모두 능가하는 성능을 보였습니다.
  • 특히 ProofRM-32B 는 테스트 세트에서 82.4% 의 정확도를 기록하여 베이스 모델 대비 9.9%p 향상되었습니다.
• 일반화 능력 (Generalization):
  • 훈련 데이터와 완전히 다른 OPC (Open Proof Corpus) 테스트 세트에서도 강력한 성능을 발휘했습니다. ProofRM-32B 는 DeepSeek-R1 을 능가하고 Gemini-2.5-Flash 와 유사한 성능을 보여주었습니다.
• 테스트 시간 확장 (Test-time Scaling):
  • Best-of-K 실험에서 Proof-RM 은 생성된 여러 증명 중 가장 좋은 것을 선택하는 데 있어 뛰어난 식별 능력을 보여주었습니다. 이는 RLVR 기반의 추론 모델이 테스트 시 더 많은 연산 자원을 투입할 때 효과적으로 활용될 수 있음을 의미합니다.
• 오류 유형 식별:
  • 단순한 계산 실수가 아닌, 논리적 비약, 존재하지 않는 정리 사용, 가정의 오용 등 복잡한 추론 오류를 기존 모델보다 훨씬 정확하게 식별했습니다.

5. 의의 및 결론 (Significance)

이 논문은 수학 추론 분야에서 RLVR 의 적용 범위를 단순한 정답 확인에서 '전체 증명 과정의 검증'으로 확장했다는 점에서 의의가 큽니다.

• 실용성: 고비용의 인간 전문가 검증 없이도 고품질의 증명 검증 모델을 훈련할 수 있는 확장 가능한 방법을 제시하여, 수학 AI 의 발전 속도를 가속화할 수 있습니다.
• 신뢰성: 모델이 '정답만 맞추는' 쇼트컷 학습을 방지하고, 논리적 엄밀성을 갖춘 추론을 하도록 유도하여 AI 의 신뢰성을 높입니다.
• 미래 전망: 이 연구는 수학 올림피아드 수준의 난이도 문제를 해결하는 AI 에이전트 개발과, 복잡한 논리적 추론이 필요한 다른 분야 (법률, 과학 등) 로의 확장에 중요한 토대를 마련했습니다.

요약하자면, Proof-RM은 확장 가능한 데이터 생성과 안정화된 RL 훈련 기법을 결합하여, 수학 증명 과정을 자동으로 검증하고 모델의 추론 능력을 강화하는 새로운 표준을 제시한 연구입니다.