Instructions to use tinyopsec/StepFun-Formalizer-7B-GGUF with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Notebooks
Google Colab
Kaggle
Local Apps Settings

How to use tinyopsec/StepFun-Formalizer-7B-GGUF with llama.cpp:

Install (macOS, Linux)

curl -LsSf https://llama.app/install.sh | sh
# Start a local OpenAI-compatible server with a web UI:
llama serve -hf tinyopsec/StepFun-Formalizer-7B-GGUF:F16
# Run inference directly in the terminal:
llama cli -hf tinyopsec/StepFun-Formalizer-7B-GGUF:F16

Install from WinGet (Windows)

winget install llama.cpp
# Start a local OpenAI-compatible server with a web UI:
llama serve -hf tinyopsec/StepFun-Formalizer-7B-GGUF:F16
# Run inference directly in the terminal:
llama cli -hf tinyopsec/StepFun-Formalizer-7B-GGUF:F16

Use pre-built binary

# Download pre-built binary from:
# https://github.com/ggerganov/llama.cpp/releases
# Start a local OpenAI-compatible server with a web UI:
./llama-server -hf tinyopsec/StepFun-Formalizer-7B-GGUF:F16
# Run inference directly in the terminal:
./llama-cli -hf tinyopsec/StepFun-Formalizer-7B-GGUF:F16

Build from source code

git clone https://github.com/ggerganov/llama.cpp.git
cd llama.cpp
cmake -B build
cmake --build build -j --target llama-server llama-cli
# Start a local OpenAI-compatible server with a web UI:
./build/bin/llama-server -hf tinyopsec/StepFun-Formalizer-7B-GGUF:F16
# Run inference directly in the terminal:
./build/bin/llama-cli -hf tinyopsec/StepFun-Formalizer-7B-GGUF:F16

Use Docker

docker model run hf.co/tinyopsec/StepFun-Formalizer-7B-GGUF:F16

LM Studio
Jan

vLLM

How to use tinyopsec/StepFun-Formalizer-7B-GGUF with vLLM:

Install from pip and serve model

# Install vLLM from pip:
pip install vllm
# Start the vLLM server:
vllm serve "tinyopsec/StepFun-Formalizer-7B-GGUF"
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:8000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "tinyopsec/StepFun-Formalizer-7B-GGUF",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker

docker model run hf.co/tinyopsec/StepFun-Formalizer-7B-GGUF:F16

Ollama
How to use tinyopsec/StepFun-Formalizer-7B-GGUF with Ollama:
```
ollama run hf.co/tinyopsec/StepFun-Formalizer-7B-GGUF:F16
```
Unsloth Desktop
Docker Model Runner
How to use tinyopsec/StepFun-Formalizer-7B-GGUF with Docker Model Runner:
```
docker model run hf.co/tinyopsec/StepFun-Formalizer-7B-GGUF:F16
```

Lemonade

How to use tinyopsec/StepFun-Formalizer-7B-GGUF with Lemonade:

Pull the model

# Download Lemonade from https://lemonade-server.ai/
lemonade pull tinyopsec/StepFun-Formalizer-7B-GGUF:F16

Run and chat with the model

lemonade run user.StepFun-Formalizer-7B-GGUF-F16

List all available models

lemonade list

Atomic Chat

StepFun-Formalizer-7B-GGUF / README.md

tinyopsec

Create README.md

186a645 verified about 1 month ago

preview code

Raw History Blame Contribute Delete

2.75 kB

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

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