Kimina-Prover: 대규모 형식 추론 모델에 대한 테스트 시점 RL 검색 적용
Hugging Face는 Qwen2.5-72B를 기반으로 하고 Kimi k1.5 RL 파이프라인으로 학습된 최첨단 형식 정리 증명 모델 Kimina-Prover-72B를 출시했습니다. 테스트 시점 강화 학습(Test-Time Reinforcement Learning, TTRL) 검색 프레임워크와 통합 오류 수정 메커니즘을 도입함으로써, 이 모델은 miniF2F 벤치마크에서 사상 최고 **92.2%**의 통과율을 기록했습니다.
72B 플래그십 모델 외에도 두 가지 증류 변형이 제공됩니다: Kimina-Prover-Distill-8B(Qwen3-8B 기반)와 Kimina-Prover-Distill-1.7B(Qwen3-1.7B 기반).
miniF2F에서의 최첨단 성능
Kimina-Prover-72B는 여러 샘플링 예산에 걸쳐 기존 형식 추론 모델들을 능가합니다. 제공된 벤치마크에 따르면, 이 모델은 pass@1 63.9%, pass@32 84.0%, pass@1024 87.7%를 달성했습니다. 전체 TTRL 검색 프레임워크를 적용하면 통과율이 92.2%까지 상승합니다.
| 모델 | pass@1 | pass@32 | pass@1024 |
|---|---|---|---|
| Kimina-Prover-1.7B | 46.7 | 73.4 | — |
| DSP+ | 52.5 | 71.3 | 80.7 |
| DeepSeek-Prover-V2-7B | 58.6 | 75.6 | 79.9 |
| Kimina-Prover-8B | 61.1 | 78.3 | — |
| DeepSeek-Prover-V2-671B | 61.9 | 82.4 | 86.6 |
| Kimina-Prover-72B | 63.9 | 84.0 | 87.7 |
테스트 시점 강화 학습 (TTRL) 검색
긴 시간 지평의 추론이 필요한 복잡한 문제를 해결하기 위해, Kimina-Prover는 모델이 중간 보조정리를 스스로 발견·조합·재사용할 수 있게 하는 TTRL 검색 프레임워크를 활용합니다.
Lemma-Enabled 패턴
RL 훈련 중에 모델은 문제 컨텍스트 앞에 1~3개의 형식 보조정리를 무작위로 추가하는 "lemma-enabled pattern"에 노출됩니다. 모델이 실제로 이러한 보조정리를 사용하도록 하기 위해, 선호 기반 보상 형태 전략을 적용합니다: 제공된 보조정리를 활용한 솔루션은 더 높은 보상을 받고, 무시한 경우는 벌점을 받습니다. 이 결과 보조정리 활용 비율은 30–40%에 달했습니다.
재귀적 검색 및 필터링
TTRL은 다음 메커니즘을 통해 무작위 탐색에서 전략적 검색으로 전환됩니다:
- 동적 스코어링: 시스템은 각 후보 보조정리에 대해 "보조정리 활용 점수"를 추적합니다. 각 RL 반복에서 입력의 60%는 상위 점수 보조정리를 사용하고, 40%는 무작위 보조정리를 포함해 탐색을 장려합니다.
- 가지치기: 50번 시도 후 활용 점수가 $\tau=0.10$ 이하인 보조정리는 제거됩니다.
- 재귀적 분해: 정리나 보조정리가 $N=128$번 시도 후에도 해결되지 않으면, 시스템은 새로운 후보 하위 보조정리를 생성해 문제를 더 작은 하위 문제로 재귀적으로 분해합니다.
- 부정 필터링: 모델이 논리적으로 일관되지 않은 보조정리를 악용하는 것을 방지하기 위해, 시스템은 모든 새로운 보조정리의 부정을 증명하려 시도합니다. 부정이 증명되면 해당 보조정리는 폐기됩니다.
통합 오류 수정 기능
Kimina-Prover는 Lean 4 오류 메시지를 해석하고 목표에 맞는 수정을 제안할 수 있으며, 이는 처음부터 증명을 다시 생성하는 것보다 샘플 효율이 높습니다.
SFT 데이터와 배치 실패 재생
일반 LLM이 Lean 오류 메시지를 다루기 어려워, 팀은 (잘못된 증명, Lean 피드백, 올바른 증명) 형태의 삼중항으로 구성된 특수 지도 학습(Supervised Fine-Tuning, SFT) 데이터셋을 만들었습니다. 이 데이터는 Claude 3.7 Sonnet이 생성한 추론 체인으로 보강되었습니다.
훈련 안정성을 위해 팀은 Batched Failure Replay 전략을 구현했습니다. 즉시 수정하는 대신, 반복 $N$에서 실패한 시도들을 수집해 다음 반복 $N+1$에 표준 문제와 섞어 모델이 지속적으로 오류 수정 작업에 노출되도록 했습니다.
효율성 향상
오류 수정은 고정된 계산 예산 하에서 성공률을 크게 끌어올립니다. 59개의 어려운 MiniF2F 문제에 대해 "16+16 시도‑수정" 전략(초기 16 시도 + 16번 수정)으로 35.6%의 성공률을 달성했으며, 이는 32개의 독립 시도를 사용하는 "32x1 무차별" 전략의 28.8%보다 높았습니다.
추가 기술 개선 사항
- 연속 사전 학습 (Continuous Pre-training, CPT): 모델은 60억 토큰 데이터셋(그 중 GitHub에서 2.6억 토큰, 컴파일러 검증 롤아웃 데이터 55억 토큰)으로 CPT를 수행했습니다.
- 무작위 증명 절단 증강: 인간이 주석 달은 증명을 활용하기 위해 팀은 "Proof truncation"(증명의 끝을 제거)과 "Proof infilling"(내부 블록을
sorry로 교체) 방식을 사용해 모델이 논리적 공백을 메우고 완성하도록 학습시켰습니다. - 프롬프트 세트 큐레이션: 훈련 세트는 약 90K개의 대회 중심 문제로 정제되었으며, 동적 필터링을 통해 너무 쉬워진 문제를 제거하고, 여전히 어려운 문제는 분해했습니다.
- 비증명 문제 해결: 모델은 최종 답을 먼저 도출한 뒤, 그 답을 정당화하는 형식 증명을 생성함으로써 답을 요구하는 문제도 처리할 수 있습니다.
SUMMARY: Hugging Face는 Lean 4용 최첨단 정리 증명 모델인 Kimina-Prover-72B를 발표했으며, 새로운 테스트 시점 강화 학습(TTRL) 검색 프레임워크를 활용해 miniF2F 벤치마크에서 92.2%의 통과율을 달성했습니다.
TITLE: Kimina-Prover: 대규모 형식 추론 모델에 대한 테스트 시점 RL 검색 적용