File size: 2,749 Bytes
186a645 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 | ---
license: apache-2.0
base_model: stepfun-ai/StepFun-Formalizer-7B
tags:
- gguf
- qwen2
- chat
- math
- autoformalization
- lean4
language:
- en
pipeline_tag: text-generation
library_name: gguf
---
# StepFun-Formalizer-7B GGUF
GGUF quantizations of [stepfun-ai/StepFun-Formalizer-7B](https://huggingface.co/stepfun-ai/StepFun-Formalizer-7B).
## About the Model
StepFun-Formalizer-7B is a large language model designed to translate natural-language mathematical problems into formal statements in **Lean 4**. It is fine-tuned on top of [deepseek-ai/DeepSeek-R1-Distill-Qwen-7B](https://huggingface.co/deepseek-ai/DeepSeek-R1-Distill-Qwen-7B) and achieves state-of-the-art performance on autoformalization benchmarks including FormalMATH-Lite, ProverBench, and CombiBench.
## Quantization Files
| File | Bits | Size | Use Case |
|------|------|------|----------|
| model_f16.gguf | 16 | ~15 GB | Maximum quality, reference |
| model_q8_0.gguf | 8 | ~8.1 GB | Best quality, recommended if VRAM allows |
| model_q6_k.gguf | 6 | ~6.3 GB | Near-lossless, great balance |
| model_q5_k_m.gguf | 5 | ~5.5 GB | Recommended for most users |
| model_q5_k_s.gguf | 5 | ~5.3 GB | Slightly smaller than Q5_K_M |
| model_q4_k_m.gguf | 4 | ~4.7 GB | Good quality/size balance |
| model_q4_k_s.gguf | 4 | ~4.5 GB | Smaller Q4 variant |
| model_q3_k_l.gguf | 3 | ~3.9 GB | Low VRAM, acceptable quality |
| model_q3_k_m.gguf | 3 | ~3.6 GB | Lower VRAM |
| model_q3_k_s.gguf | 3 | ~3.3 GB | Minimal footprint |
| model_q2_k.gguf | 2 | ~2.8 GB | Smallest, significant quality loss |
## VRAM Requirements
| Quantization | VRAM |
|---|---|
| F16 | ~16 GB |
| Q8_0 | ~9 GB |
| Q6_K | ~7 GB |
| Q5_K_M | ~6 GB |
| Q4_K_M | ~5 GB |
| Q3_K_M | ~4 GB |
| Q2_K | ~3.5 GB |
## Usage
### llama.cpp
```bash
./llama-cli -m model_q4_k_m.gguf -p "Please autoformalize the following problem: ..." -n 512
```
### llama-cpp-python
```python
from llama_cpp import Llama
llm = Llama(model_path="model_q4_k_m.gguf", n_ctx=4096)
output = llm("Please autoformalize the following problem: ...", max_tokens=512)
print(output["choices"][0]["text"])
```
### LM Studio
Download the desired `.gguf` file and load it directly in [LM Studio](https://lmstudio.ai/).
### Ollama
```bash
ollama run hf.co/tinyopsec/StepFun-Formalizer-7B-GGUF:Q4_K_M
```
## Prompt Format
```
<｜User｜>Please autoformalize the following problem:
<informal problem here>
<｜Assistant｜>
```
## Links
- Original model: [stepfun-ai/StepFun-Formalizer-7B](https://huggingface.co/stepfun-ai/StepFun-Formalizer-7B)
- Paper: [arxiv.org/abs/2508.04440](https://arxiv.org/abs/2508.04440)
- Code: [github.com/stepfun-ai/StepFun-Formalizer](https://github.com/stepfun-ai/StepFun-Formalizer)
|