Kimina Prover Distill 1.7B F32 GGUF
K
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% 的准确率。
蒸馏模型
从 72B 参数的大模型蒸馏而来，保持了高性能的同时减小了模型尺寸。
多量化版本
提供从 F32 到 Q2_K 等多种量化版本，适应不同硬件需求。
模型能力
数学定理证明
Lean 4 问题解决
竞赛风格数学问题解答
使用案例
数学教育
数学竞赛问题解答
帮助学生理解和解决竞赛风格的数学问题
在 MiniF2F-test 上达到 72.95% 准确率
形式化验证
数学定理自动证明
辅助数学家进行定理的形式化验证
Safetensors精选推荐AI模型
Llama 3 Typhoon V1.5x 8b Instruct
专为泰语设计的80亿参数指令模型，性能媲美GPT-3.5-turbo，优化了应用场景、检索增强生成、受限生成和推理任务
大型语言模型
Transformers 支持多种语言
Transformers 支持多种语言L
scb10x
3,269
16
Cadet Tiny
Openrail
Cadet-Tiny是一个基于SODA数据集训练的超小型对话模型，专为边缘设备推理设计，体积仅为Cosmo-3B模型的2%左右。
对话系统 Transformers 英语
Transformers 英语C
ToddGoldfarb
2,691
6
Roberta Base Chinese Extractive Qa
基于RoBERTa架构的中文抽取式问答模型，适用于从给定文本中提取答案的任务。
问答系统 中文
R
uer
2,694
98
%20--%3e%3cdefs%3e%3cstyle%3e%20.st0%20{%20fill:%20%23061b40;%20}%20.st1%20{%20fill:%20%23306af1;%20}%20.st2%20{%20fill:%20%235ce5cf;%20}%20%3c/style%3e%3c/defs%3e%3cg%3e%3cpath%20class='st0'%20d='M55,10.5h9v3h-9v9h12V7.5h-12v3ZM64,19.5h-6v-3h6v3Z'/%3e%3cpolygon%20class='st0'%20points='69%2016.5%2078%2016.5%2078%2019.5%2069%2019.5%2069%2022.5%2081%2022.5%2081%2013.5%2072%2013.5%2072%2010.5%2081%2010.5%2081%207.5%2069%207.5%2069%2016.5'/%3e%3cpolygon%20class='st0'%20points='95%2010.5%2095%207.5%2083%207.5%2083%2022.5%2095%2022.5%2095%2019.5%2086%2019.5%2086%2016.5%2095%2016.5%2095%2013.5%2086%2013.5%2086%2010.5%2095%2010.5'/%3e%3cpath%20class='st0'%20d='M40,1.5v21h11.6l1.4-1.4v-7.6h0c0,0-1.4-1.5-1.4-1.5l1.4-1.4V2.9l-1.4-1.4h-11.6ZM50,19.5h-7v-6h7v6ZM50,10.5h-7v-6h7v6Z'/%3e%3c/g%3e%3cpath%20class='st1'%20d='M23.1,24L14.7,4.8l-4.9,11.2h3.8l-1.8,4H3.3L12.1,0H2C.9,0,0,.9,0,2v20c0,1.1.9,2,2,2h21.1Z'/%3e%3cpath%20class='st2'%20d='M34,0h-16.8l10.6,24h6.2c1.1,0,2-.9,2-2V2C36,.9,35.1,0,34,0ZM32.5,20h-4V4h4v16Z'/%3e%3c/svg%3e)
智启未来，您的人工智能解决方案智库
简体中文