Hugging Face Overview
Model Overview
AI-MO/Kimina-Prover-RL-1.7B is a specialized theorem proving model developed collaboratively by Project Numina and Kimi teams. This 1.7 billion parameter model is specifically designed for competition-style problem solving in Lean 4, a formal proof assistant.
Key Capabilities & Training
- Theorem Proving in Lean 4: The model's primary strength lies in its ability to generate formal proofs within the Lean 4 environment.
- Reinforcement Learning (RL): It was fine-tuned using a reinforcement learning approach, building upon the base model AI-MO/Kimina-Prover-Distill-1.7B.
- Performance: The model demonstrates strong performance, achieving 76.63% Pass@32 on the MiniF2F-test benchmark, representing a +3.68% improvement over its base model.
- Open-Source Training Pipeline: The training was conducted using the Kimina-Prover-RL open-source pipeline, with further details available in a Hugging Face blog article.
Use Cases
- Automated Theorem Proving: Ideal for tasks requiring the automatic generation of proofs in Lean 4.
- Mathematical Problem Solving: Particularly suited for formalizing and solving mathematical problems in a competition context.
- Research in Formal Verification: Useful for researchers exploring advanced methods in automated reasoning and proof generation.