Kimina-Prover-Distill-1.7B-F32-GGUFオープンソース定理証明モデル

Kimina Prover Distill 1.7B F32 GGUF

prithivMLmodsによって開発

Project NuminaとKimiチームによって開発された定理証明モデルで、Lean 4における競技スタイルの問題解決能力に特化しています。

ダウンロード数 516

リリース時間 : 7/14/2025

モデル概要

Kimina-Prover-Distill-1.7Bは、大規模な強化学習で訓練されたKimina-Prover-72Bモデルの蒸留バージョンで、Lean 4における競技スタイルの数学問題の解決に特化しています。

高性能な定理証明

MiniF2F - testでPass@32で72.95%の正解率を達成しました。

蒸留モデル

72億パラメータの大規模モデルから蒸留され、高性能を維持しながらモデルサイズを縮小しています。

複数の量子化バージョン

F32からQ2_Kまでの複数の量子化バージョンを提供し、さまざまなハードウェア要件に対応しています。

数学定理証明

Lean 4問題解決

競技スタイルの数学問題解答

数学教育

数学競技問題の解答

学生が競技スタイルの数学問題を理解して解くのを支援します。

MiniF2F - testで72.95%の正解率を達成

形式的検証

数学定理の自動証明

数学者が定理の形式的検証を行うのを支援します。

ファイル名	サイズ	形式
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