---

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.

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 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

./llama-cli -m model_q4_k_m.gguf -p "Please autoformalize the following problem: ..." -n 512

llama-cpp-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.

Ollama

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
• Paper: arxiv.org/abs/2508.04440
• Code: github.com/stepfun-ai/StepFun-Formalizer