QED-Nano: 작은 모델이 어려운 정리 증명법을 학습하는 기술적 요약

이 논문은 국제 수학 올림피아드 (IMO) 수준의 복잡한 증명 기반 문제를 해결하기 위해, 거대하고 비공개인 AI 시스템에 의존하지 않고 **작은 오픈 소스 모델 (4B 파라미터)**을 어떻게 훈련시켜 경쟁력 있는 성능을 달성할 수 있는지를 보여줍니다. 저자들은 QED-Nano라는 4B 모델을 개발하여, 기존에 훨씬 큰 모델 (30B~685B) 이나 독점 모델 (Gemini 3 Pro) 과 경쟁할 수 있음을 입증했습니다.

1. 문제 정의 (Problem)

최근 독점 AI 시스템이 IMO 골드 메달 수준으로 복잡한 수학 증명 문제를 해결하는 능력을 보여주었지만, 그 훈련 파이프라인은 비공개이며 거대한 내부 모델과 복잡한 인프라에 의존합니다. 이는 연구의 재현성, 비용 효율성, 그리고 기술적 이해를 어렵게 만듭니다.

• 핵심 질문: 작은 오픈 소스 모델 (Small Open Models) 을 후학습 (Post-training) 시켜 IMO 수준의 어려운 수학 증명 문제를 해결할 수 있을까?
• 도전 과제: 수학 문제 풀이는 단순히 정답을 도출하는 것과 달리, 길고 일관성 있으며 수학적으로 엄밀한 논증 (Proof) 을 생성해야 하므로, 기존 검증 가능한 정답 (Verifiable Answer) 기반 훈련과는 근본적으로 다릅니다.

2. 방법론 (Methodology)

QED-Nano 는 3 단계로 구성된 후학습 (Post-training) 레시피를 따릅니다.

1 단계: 데이터 구축 및 채점 체계 (Dataset & Grading Schemes)

• 데이터 소스: Art of Problem Solving (AoPS) 포럼과 다양한 국제/국가 수학 경시대회 (IMO, USAMO 등) 의 공식 해답을 수집했습니다.
• 필터링: 이미지 기반 문제 제거, 너무 쉬운 문제나 단순 계산 문제 제거, 2025 년 벤치마크 문제 제외 등을 통해 고품질 데이터 (약 5,000 개 문제) 를 선별했습니다.
• 채점 체계 (Rubric-based Grading): 단순 이진 (정답/오답) 평가가 아닌, **0~7 점 척도의 상세한 채점 기준 (Rubric)**을 생성했습니다.
  • 각 문제마다 중간Checkpoint(부분 점수), 실수 시 감점 항목, 영점 처리 항목을 정의합니다.
  • 이 체계는 강화학습 (RL) 에 밀집된 (Dense) 보상 신호를 제공하여 모델이 긴 추론 과정에서 점진적으로 개선되도록 유도합니다.

2 단계: 훈련 레시피 (Training Recipe)

1. 지도 미세 조정 (SFT):

   • 목표: 모델에게 증명 작성 스타일을 심어줍니다.
   • 방법: 685B 모델인 DeepSeek-Math-V2 가 생성한 고품질 증명 데이터를 증류 (Distillation) 하여 약 7,500 개의 증명 쌍으로 SFT 를 수행합니다.
   • 주의점: SFT 는 모델이 긴 문맥을 모방하게 하여 '길이 폭발 (Length Explosion)' 현상을 유발할 수 있으나, 이는 RL 단계에서 교정됩니다.

2. 강화학습 (RL) - 핵심:

   • 알고리즘: GRPO (Group Relative Policy Optimization) 를 사용합니다.
   • 보상: 위에서 정의한 Rubric 기반 채점 체계 (GPT-OSS-20B 가 채점자 역할) 를 사용하여Outcome Reward 를 계산합니다.
   • 훈련 전략: 너무 쉽거나 너무 어려운 문제는 제외하고, 난이도 분포가 균형을 이루도록 프롬프트 세트를 구성합니다.

3. 추론 캐시 (Reasoning Cache, RC) 와 테스트 시간 확장:

   • 문제: 긴 증명 과정을 직접 RL 로 훈련하면 분산이 너무 커져 학습이 불안정해집니다.
   • 해결책: Reasoning Cache (RC) 프레임워크를 도입합니다.
     • 모델이 짧은 추론 세그먼트를 생성하고, 이를 요약 (Summarize) 하여 '상태 표현 (State Representation)'으로 만듭니다.
     • 다음 추론 단계는 원래 문제와 이 요약된 상태를 조건으로 생성됩니다.
     • 이를 통해 수백만 토큰에 해당하는 긴 추론 범위를 짧은 RL 롤아웃으로 학습할 수 있게 됩니다.
   • 테스트 시간: 훈련된 모델은 RC, RSA (Recursive Self-Attention), DeepSeek Math scaffold 등 다양한 테스트 시간 확장 기법과 결합하여 성능을 극대화합니다.

3. 주요 기여 (Key Contributions)

1. 작은 모델의 증명 능력 입증: 4B 파라미터 모델이 30B~685B 모델 및 독점 모델과 경쟁 가능한 수준으로 증명 능력을 향상시켰습니다.
2. 효율적인 훈련 파이프라인 공개: SFT + Rubric 기반 RL + Reasoning Cache 를 결합한 재현 가능한 오픈 소스 파이프라인을 공개했습니다.
3. 테스트 시간 적응 (Test-time Adaptation): 작은 모델이 테스트 시 계산 자원을 늘려 (Scaffold 사용) 성능을 극대화할 수 있음을 보여주었습니다.
4. 데이터 및 코드 공개: FineProofs-SFT/RL 데이터셋, QED-Nano 모델, 훈련/평가 코드를 모두 오픈했습니다.

4. 실험 결과 (Results)

벤치마크: IMO-ProofBench, ProofBench, IMO-AnswerBench

• 성능: QED-Nano 는 SFT 만으로는 4B 모델 중 최강이었으며, RL 과 테스트 시간 Scaffold(RSA) 를 결합하면 **DeepSeek-Math-V2(685B) 와 유사한 성능 (56.9% vs 57.9%)**을 보이며, Nomos-1(30B) 보다 훨씬 작은 모델임에도 불구하고 이를 압도했습니다.
• 비용 효율성: 독점 모델 (Gemini 3 Pro) 에 근접하는 성능을 내면서 추론 비용은 훨씬 낮습니다.
• 품질: 생성된 증명은 구조화되어 있고 명확하며, reward hacking(채점자 속이기) 이 거의 관찰되지 않았습니다.

5. 의의 및 결론 (Significance)

• 규모의 한계 극복: 수학 증명과 같은 고난도 추론 작업이 반드시 거대 모델 (100B+ 파라미터) 만으로 가능하다는 통념을 깨뜨렸습니다.
• 효율적인 추론: 모델 크기를 키우는 대신, **고품질의 후학습 레시피 (SFT+RL+Scaffold)**와 테스트 시간 계산 확장을 통해 성능을 극대화할 수 있음을 증명했습니다.
• 오픈 과학: 독점 시스템의 블랙박스 상태를 벗어나, 작은 오픈 모델이 어떻게 최상위 수준의 추론 능력을 획득하는지에 대한 구체적인 방법론을 제시하여 향후 연구의 기반을 마련했습니다.

결론적으로, QED-Nano 는 "작은 모델도 올바르게 훈련하면 거대 모델과 경쟁할 수 있다"는 것을 수학 증명이라는 어려운 도메인에서 입증한 획기적인 연구입니다.