정리 증명 SOTA 모델 Kimina-Prover 공개
Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models
·2025.07.10 21:54
Numina과 Kimi 팀이 테스트 시간 RL 탐색을 적용해 miniF2F 벤치마크에서 SOTA를 달성한 Kimina-Prover를 공개했다.
Numina과 Kimi 팀이 Kimina-Prover-72B를 포함한 새로운 정리 증명 모델 시리즈를 공개했다. Kimina-Prover-72B는 Qwen2.5-72B를 기반으로 하며, 8B 및 1.7B 크기의 증류(Distilled) 모델도 함께 출시되었다.
주요 기술적 혁신은 다음과 같다:
- 테스트 시간 강화학습(TTRL) 탐색: 모델이 복잡한 증명을 위해 여러 중간 보조 정리(Lemma)를 스스로 발견하고 결합하여 적용할 수 있는 에이전트 기반 프레임워크를 도입했다.
- 오류 수정 능력: Lean 언어의 오류 메시지를 해석하고 타겟팅된 수정안을 제안함으로써, 처음부터 다시 증명을 생성하는 대신 효율적으로 오류를 바로잡는다.
이러한 기술을 통해 Kimina-Prover는 miniF2F-test 벤치마크에서 **92.2%**의 통과율을 기록하며, DeepSeek-Prover-V2 및 DSP+를 제치고 새로운 SOTA(State-of-the-Art) 성능을 달성했다.
이 요약은 원문 이해를 돕기 위한 큐레이션입니다. 저작권은 원저작자에게 있으며, 정확한 내용과 맥락은 원문을 확인하세요.
요약 오류, 출처 표기 문제, 삭제 요청은 문의 · 건의로 알려주세요.