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

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

Model tree for tinyopsec/StepFun-Formalizer-7B-GGUF

Base model

deepseek-ai/DeepSeek-R1-Distill-Qwen-7B

Finetuned

stepfun-ai/StepFun-Formalizer-7B

Quantized

(3)

this model

Paper for tinyopsec/StepFun-Formalizer-7B-GGUF

StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion

Paper • 2508.04440 • Published Aug 6, 2025 • 9

tinyopsec
/

StepFun-Formalizer-7B-GGUF