Kimina-Prover-RL: Lean 4 정리를 위한 오픈소스 학습 파이프라인 공개

DeepSeek-R1에서 영감을 받은 '추론 후 생성(reasoning-then-generation)' 패러다임을 기반으로, Lean 4 형식 정리(formal theorem proving)를 위한 오픈소스 학습 파이프라인인 Kimina-Prover-RL이 공개되었다.

이 파이프라인은 GRPO(Group Relative Policy Optimization) 강화학습 방식을 사용하며, 오픈소스 Verl 프레임워크와 완벽하게 호환된다. 모델이 자연어 추론 과정을 거친 뒤 Lean 코드를 생성하도록 설계되어, 계획과 실행을 분리함으로써 설명 가능성과 오류 복구 능력을 높인 것이 특징이다.

함께 공개된 두 가지 모델은 해당 크기 카테고리에서 MiniF2F 벤치마크 SOTA를 기록했다:

• Kimina-Prover-RL-1.7B: Pass@32 기준 76.63% 달성
• Kimina-Prover-RL-0.6B: Pass@32 기준 71.30% 달성

효율적인 학습을 위해 대규모 병렬 검증을 지원하는 kimina-lean-server와 이를 위한 Python 패키지인 kimina-client도 함께 제공된다. 학습 데이터셋은 기존 NuminaMath-LEAN에서 난이도가 높은 문제들을 선별하고 Gemini를 통해 변형을 생성한 Kimina-Prover-Promptset을 사용했다.