Kimina-Prover-Distill-1.7B-F32-GGUF

AI-MO/Kimina-Prover-Distill-1.7B is a theorem proving model developed by Project Numina and Kimi teams, focusing on competition style problem solving capabilities in Lean 4. It is a distillation of Kimina-Prover-72B, a model trained via large scale reinforcement learning. It achieves 72.95% accuracy with Pass@32 on MiniF2F-test.

Model Files

File Name	Size	Format
Kimina-Prover-Distill-1.7B.gitattributes	2.48 kB	Git attributes
Kimina-Prover-Distill-1.7B.BF16.gguf	3.45 GB	GGUF BF16
Kimina-Prover-Distill-1.7B.F16.gguf	3.45 GB	GGUF F16
Kimina-Prover-Distill-1.7B.F32.gguf	6.89 GB	GGUF F32
Kimina-Prover-Distill-1.7B.Q2_K.gguf	778 MB	GGUF Q2_K
Kimina-Prover-Distill-1.7B.Q3_K_L.gguf	1 GB	GGUF Q3_K_L
Kimina-Prover-Distill-1.7B.Q3_K_M.gguf	940 MB	GGUF Q3_K_M
Kimina-Prover-Distill-1.7B.Q3_K_S.gguf	867 MB	GGUF Q3_K_S
Kimina-Prover-Distill-1.7B.Q4_K_M.gguf	1.11 GB	GGUF Q4_K_M
Kimina-Prover-Distill-1.7B.Q4_K_S.gguf	1.06 GB	GGUF Q4_K_S
Kimina-Prover-Distill-1.7B.Q5_K_M.gguf	1.26 GB	GGUF Q5_K_M
Kimina-Prover-Distill-1.7B.Q5_K_S.gguf	1.23 GB	GGUF Q5_K_S
Kimina-Prover-Distill-1.7B.Q6_K.gguf	1.42 GB	GGUF Q6_K
Kimina-Prover-Distill-1.7B.Q8_0.gguf	1.83 GB	GGUF Q8_0
README.md	180 Bytes	Markdown
config.json	29 Bytes	JSON

Quants Usage

(sorted by size, not necessarily quality. IQ-quants are often preferable over similar sized non-IQ quants)

Here is a handy graph by ikawrakow comparing some lower-quality quant types (lower is better):