Numina & Kimi 팀이 Test-Time RL Search와 Lemma-Enabled Pattern을 도입해 형식 증명 모델의 miniF2F 벤치마크 통과율을 92.2%로 달성

Context

기존 단일 단계 추론 방식으로는 여러 중간 단계를 거쳐야 하는 복잡한 수학 증명 문제를 해결하기 어려웠다. Kimina-Prover Preview까지는 선형적 스케일링 패턴을 보였으나, 샘플링 예산 증대 시 성능 향상이 점진적으로 둔화되는 한계가 있었다.

Technical Solution

• Test-Time Reinforcement Learning(TTRL) Search 프레임워크 도입: 모델이 중간 보조정리(Lemma)를 재귀적으로 발견, 결합, 적용하여 복잡한 증명을 다단계로 구성할 수 있도록 설계
• Lemma-Enabled Pattern 구현: 입력에서 제공되는 유용한 보조정리를 식별하고 증명 구성 과정에 통합하는 구조화된 중간 결과 재사용 메커니즘
• Error-Fixing Capability 통합: Lean 4의 오류 메시지를 해석하고 목표 지정된 수정안을 제시하는 반복적 피드백 루프로 샘플 효율성 향상
• Qwen2.5-72B 기반 모델 학습: Kimi k1.5 RL 파이프라인을 적용하여 72B 기본 모델과 8B, 1.7B 버전의 증류 모델 3가지 구현
• 단일 라운드 오류 수정 추가: pass@32 84.0%에서 pass@1024 87.7%로 향상시킨 후, 오류 수정 1라운드 적용으로 86.4% 달성

Impact

• miniF2F-test 벤치마크에서 pass@1 기준 63.9% (Kimina-Prover-72B vs. DeepSeek-Prover-V2-671B 61.9%)
• pass@32 기준 84.0% 달성
• pass@1024 기준 87.7% 달성
• 전체 TTRL Search 프레임워크 적용 시 최종 92.2% 통과율 달성
• Kimina-Prover-72B가 동등한 샘플링 예산 조건에서 모든 평가 설정에서 최고 성능 기록

Key Takeaway

형식 증명과 같이 장거리 추론이 필요한 작업에서는 단일 단계 생성보다 Test-Time Search와 중간 결과 재사용 메커니즘이 샘플링 예산의 효율성을 크게 향상시킨다. 또한 증명 시스템의 오류 메시지를 모델이 직접 해석하여 반복적으로 개선하는 방식이 처음부터 다시 생성하는 것보다 표본 효율성을 높인다.