카테고리
Lean 4
-
Lean 증명에서 92.2%를 만든 TTRL 검색
huggingface.co의 Kimina-Prover 글을 바탕으로 miniF2F-test에서 pass@1 63.9, pass@32 84.0, 최종 92.2%가 나온 구조와 오류 수정·lemma 재사용의 실무 포인트를 정리합니다.
-
Lean 4 정리 증명 학습 파이프라인을 공개했습니다
Hugging Face의 Kimina-Prover-RL이 공개한 Lean 4 정리 증명 학습 파이프라인을 정리합니다. 1.7B 모델의 76.63% Pass@32와 0.6B 모델의 의미, 그리고 검증 흐름 점검 포인트를 함께 봅니다.