AI-MO/Kimina-Prover-Preview-Distill-7B
AI-MO/Kimina-Prover-Preview-Distill-7B is a 7.6 billion parameter theorem proving model developed by Project Numina and Kimi teams. This model is a distillation of Kimina-Prover-Preview, optimized for competition-style problem solving in Lean 4. It achieves state-of-the-art results on MiniF2F-test and ranks #1 on the PutnamBench Leaderboard within its model size and compute budget. The model is specifically designed for formal reasoning and mathematical proof generation.
Loading preview...
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.
Top 3 parameter combinations used by Featherless users for this model. Click a tab to see each config.