TL;DR
huggingface.co의 「Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models」는 Kimina-Prover-72B와 두 개의 축소판을 함께 공개했습니다.
원문은 miniF2F-test에서 pass@1 63.9, pass@32 84.0, pass@1024 87.7을 제시했고, 최종 통과율 92.2%를 보고했습니다.
실무에서는 단순 재생성보다 오류 수정, 중간 정리 재사용, 샘플 예산 관리가 더 중요해집니다.
Kimina-Prover-72B는 Kimi k1.5 RL 파이프라인과 TTRL 검색을 결합했습니다
huggingface.co에 실린 「Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models」은 Kimina-Prover-72B를 공개합니다. 원문은 이 모델을 Qwen2.5-72B를 바탕으로 Kimi k1.5 RL 파이프라인으로 학습했다고 밝힙니다. 같은 글은 Kimina-Prover-Distill-8B와 1.7B도 함께 공개했다고 적습니다.
핵심은 두 가지입니다. 하나는 lemma-enabled pattern을 쓰는 Test-Time Reinforcement Learning 검색입니다. 다른 하나는 Lean 오류 메시지를 읽고 표적 수정안을 제안하는 오류 수정 기능입니다.
원문은 이 조합이 복잡한 정리를 더 깊게 풀도록 돕는다고 설명합니다.
miniF2F-test에서 통과율은 샘플 수와 오류 수정에 따라 달라졌습니다
원문 수치만 보면 변화의 방향이 분명합니다.
| 항목 | 값 | 무엇을 재는 값인지 |
|---|---|---|
| pass@1 | 63.9 | miniF2F-test에서 1개 샘플 기준 통과율입니다. |
| pass@32 | 84.0 | miniF2F-test에서 32개 샘플 기준 통과율입니다. |
| pass@1024 | 87.7 | miniF2F-test에서 1024개 샘플 기준 통과율입니다. |
| 오류 수정 1회 추가 | 86.4% | pass@32에 오류 수정 한 라운드를 더한 통과율입니다. |
| 최종 TTRL | 92.2% | 전체 Test-Time Reinforcement Learning 검색 프레임워크 적용 결과입니다. |
| lemma 활용률 | 30–40% | 학습 뒤 안정적으로 관찰된 lemma 활용 비율입니다. |
원문은 다음처럼 적습니다.
Applying the full Test-Time Reinforcement Learning (TTRL) search framework yields a final pass rate of 92.2%.
또 다른 문장은 이렇게 말합니다.
This approach proved effective, increasing the lemma utilization rate to a stable 30–40% after training
이 표에서 보이는 핵심은 샘플을 더 뽑는 일과 오류를 고치는 일이 서로 다른 축이라는 점입니다. pass@32에서 84.0%였던 값이 오류 수정 한 라운드로 86.4%가 됩니다. 그 뒤 전체 TTRL 검색은 92.2%까지 올라갑니다.
단순한 재시도보다 중간 정리 재사용이 더 큰 차이를 만들었습니다
원문은 단일 단계 추론만으로는 긴 다단계 증명에 부족하다고 밝힙니다. 그래서 TTRL는 중간 정리를 찾아내고, 결합하고, 다시 쓰는 쪽으로 설계됐습니다. 이 점이 단순한 재생성과 갈리는 부분입니다.
원문은 현재 시스템이 pass@1024를 넘어서면 증가폭이 줄어든다고 적습니다. 즉 샘플을 더 늘리는 일만으로는 한계가 있습니다. 반면 lemma-enabled pattern과 오류 수정은 한 번 만든 정보를 다음 시도에 넘깁니다.
이 구조가 샘플 효율을 끌어올립니다.
Lean 4 증명 파이프라인은 내일부터 이렇게 점검할 수 있습니다
실무에서 볼 지점은 화려한 모델 이름이 아닙니다. 오류 메시지, 중간 정리, 샘플 예산이 실제 병목인지 확인해야 합니다.
1. 오류 메시지를 구조화해 남깁니다
Lean 오류를 단순 로그로 버리지 말고, 수정 후보와 함께 저장합니다. Kimina-Prover는 이 신호를 읽어 표적 수정을 제안했다고 원문은 밝힙니다.
2. 중간 정리 재사용 경로를 만듭니다
하나의 시도에서 찾은 보조 정리를 다음 시도에 넘겨야 합니다. 원문은 이 재사용이 긴 증명 문제에 중요하다고 설명합니다.
3. 샘플 수만 늘리기 전에 중복을 봅니다
pass@32와 pass@1024의 차이가 작아지는지 확인해야 합니다. 원문도 현재 시스템이 pass@1024 이후에는 증가폭이 줄어든다고 적습니다.
4. lemma 활용률을 별도 지표로 봅니다
원문은 학습 뒤 lemma 활용률이 30–40%로 안정화됐다고 밝힙니다. 통과율만 보면 놓치는 재사용 품질을 함께 봐야 합니다.
Kimina-Prover를 볼 때 자주 나오는 질문 3가지
Kimina-Prover는 단순히 큰 모델인가요?
아닙니다. 핵심은 Kimi k1.5 RL 파이프라인, TTRL 검색, 오류 수정의 결합입니다. 원문은 이런 구조가 긴 증명에서 더 강하다고 설명합니다.
pass@32와 pass@1024의 차이는 무엇인가요?
둘 다 통과율이지만, 사용하는 샘플 예산이 다릅니다. 원문에서 pass@32는 84.0, pass@1024는 87.7입니다.
lemma 활용률 30–40%는 왜 중요하나요?
중요합니다. 이 수치는 모델이 중간 정리를 실제로 재사용하고 있음을 보여줍니다. 원문은 학습 뒤 이 비율이 안정적인 30–40%가 됐다고 밝힙니다.
원문: 「Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models」