Hugging Face Overview
Kimina-Prover-Distill-0.6B: A Specialized Theorem Prover
AI-MO/Kimina-Prover-Distill-0.6B is a compact yet powerful 0.8 billion parameter model developed by Project Numina and Kimi teams. It is a distilled version of the 72 billion parameter Kimina-Prover-72B, which was trained using large-scale reinforcement learning. This distillation process allows for efficient deployment while retaining strong capabilities in formal theorem proving.
Key Capabilities
- Lean 4 Theorem Proving: Specifically designed and optimized for generating proofs and solving problems within the Lean 4 theorem prover environment.
- Competition-Style Problem Solving: Excels at tackling mathematical problems typically found in competitive programming or formal verification contexts.
- High Accuracy on MiniF2F-test: Achieves a notable 68.85% accuracy with Pass@32 on the MiniF2F-test benchmark, demonstrating its proficiency in formal mathematics.
Good For
- Automated Theorem Proving: Ideal for tasks requiring the automatic generation of mathematical proofs.
- Formal Verification: Useful in scenarios where formal verification of mathematical statements or software properties is needed.
- Educational Tools: Can serve as a backend for tools assisting students or researchers in learning and applying Lean 4.