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.