Hugging Face Overview
Overview
AI-MO/Kimina-Prover-Distill-8B is an 8 billion parameter model developed by Project Numina and Kimi teams, specifically designed for theorem proving in Lean 4. It is a distilled version of the 72 billion parameter Kimina-Prover-72B, which was trained using large-scale reinforcement learning techniques.
Key Capabilities
- Theorem Proving: Excels at solving competition-style mathematical problems within the Lean 4 formal proof system.
- Performance: Achieves a notable 77.86% accuracy with Pass@32 on the MiniF2F-test benchmark, indicating strong performance in formal mathematics.
- Efficiency: As a distilled model, it offers a more efficient solution for theorem proving compared to its larger 72B predecessor, while retaining significant capabilities.
Use Cases
This model is particularly well-suited for:
- Automated Theorem Proving: Generating formal proofs for mathematical statements.
- Lean 4 Development: Assisting developers and researchers working with the Lean 4 proof assistant.
- Mathematical Problem Solving: Tackling complex mathematical problems that require formal verification.