Hugging Face Overview
Kimina-Prover-Preview-Distill-7B Overview
AI-MO/Kimina-Prover-Preview-Distill-7B is a 7.6 billion parameter language model developed by Project Numina and Kimi teams, specifically engineered for advanced theorem proving. This model is a distilled version of the larger Kimina-Prover-Preview, which was trained using large-scale reinforcement learning techniques.
Key Capabilities
- Theorem Proving: Excels in competition-style mathematical problem-solving within the Lean 4 formal proof system.
- State-of-the-Art Performance: Achieves leading results on the MiniF2F-test benchmark for its model size and compute budget.
- PutnamBench Leaderboard: Ranked #1 on the PutnamBench Leaderboard at its release, demonstrating strong mathematical reasoning abilities.
- Efficient Inference: Designed for efficient deployment, with quick start examples provided using vLLM.
Use Cases
- Formal Verification: Ideal for tasks requiring rigorous mathematical proof generation and verification in Lean 4.
- Mathematical Research: Assists researchers in exploring and proving complex mathematical theorems.
- Educational Tools: Can be integrated into platforms for teaching and learning formal mathematics and proof writing.