Hugging Face Overview
Model Overview
AI-MO/Kimina-Prover-Preview-Distill-1.5B is a specialized 1.5 billion parameter model designed for theorem proving, developed collaboratively by Project Numina and Kimi teams. This model is a distilled version of the larger Kimina-Prover-Preview, which was trained using extensive reinforcement learning techniques.
Key Capabilities
- Theorem Proving: Excels at formal reasoning and competition-style problem solving, particularly within the Lean 4 proof assistant environment.
- State-of-the-Art Performance: Achieves leading results on the MiniF2F-test benchmark for its size and computational resources, demonstrating strong capabilities in mathematical theorem proving.
- Distilled Architecture: Benefits from the advanced training of its larger predecessor, offering efficient performance for its parameter count.
Good For
- Lean 4 Development: Ideal for developers and researchers working with Lean 4 who need assistance in formalizing and proving mathematical theorems.
- Automated Reasoning: Suitable for applications requiring automated theorem proving, especially in competitive or research contexts.
- Educational Tools: Can be integrated into tools for teaching and learning formal methods and proof assistants.