下载量
0
参数
3.1B
上下文
未说明
架构 / 任务
smollm3
许可证
other
MODEL POSITIONING
这个模型解决什么问题？
模型卡明确定位为形式逻辑推理专用模型，针对 FOL 翻译、蕴涵标签、语义解析、Lean 形式化与评审五类目标微调；强于同规模通用模型在结构化形式输出上的表现。仓库同时提供 bf16 原生权重与 Q4_K_M、Q5_K_M、Q6_K、Q8_0、F16 五种 GGUF 量化版本，支持 llama.cpp、Ollama、LM Studio 等本地推理工具直接加载。模型卡未说明对多模态、检索增强或工具调用的支持，也未提供商用授权。
更适合谁
- 关注形式逻辑自动求解与结构化输出的研究人员
- 需要自动 FOL 翻译、语义解析、Lean 形式化输入的机器学习工程师
- 偏好小显存本地部署的学术与教学实验用户
- 评估小模型在严格评分下推理能力的基准作者
典型使用场景
- 将自然语言句段转写为一阶逻辑公式
- 对推理对进行蕴涵关系自动标注
- 生成语义解析结构作为下游系统输入
- 起草 Lean 形式化陈述并点评证明
SOURCE-BASED CAPABILITIES
模型卡透露的核心特点
形式逻辑专项微调
针对 FOL 翻译、蕴涵标签、语义解析、Lean 形式化与评审训练
同规模领先优势
多数 Track A 客观指标超过 3B 基线与 8B 量级模型
兼顾保留能力
WiSE-FT 保守插值保留域外基准而不发生灾难性遗忘
短答案高吞吐倾向
生成长度较短，单位时间完成题目数优于更大参数模型
硬件怎么准备
- 4GB 内存配合约 2GB 显存即可加载 Q4_K_M 版本（来源数据估算）
- 8GB 内存与约 3GB 显存为仓库推荐配置
- Q6_K 起步显存约 2.5GB，Q8_0 起步显存约 3.5GB
- 模型卡未提供推理速度数据，本档案不承诺吞吐
量化版本怎么选
- Q4_K_M：体积最小，适合 4GB VRAM 或纯 CPU 入门部署
- Q5_K_M：质量略好于 Q4，体积增加有限
- Q6_K：接近 Q8_0 表现，体积约为 F16 的五分之二
- Q8_0：接近无损，显存需求更高
GGUF VARIANTS
量化版本与硬件要求
HARDWARE MATCH
哪些显卡或设备更适合运行？
按当前最小量化文件估算，至少需要 2GB 显存；如果希望为运行框架和上下文保留余量，优先参考推荐显存 3GB。
阅读 4GB 显存选型指南 →可以怎样运行
- llama.cpp 直接加载仓库内 GGUF 文件
- Ollama 拉取并运行
- LM Studio 本地加载与对话
- transformers 加载 bf16 权重并通过 vLLM 复现评测
采用前要知道的限制
- 模型卡明确不是通用助手，无额外安全与偏好对齐
- 指令跟随能力相对基线略有退化
- 评测依赖 2048 token 贪心解码，截断会显著降低得分
- 许可证为 webAI 非商用 1.0，禁止商业用途