Instructions to use openbmb/MathForm-8B with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use openbmb/MathForm-8B with Transformers:

# Use a pipeline as a high-level helper
from transformers import pipeline

pipe = pipeline("text-generation", model="openbmb/MathForm-8B")
messages = [
    {"role": "user", "content": "Who are you?"},
]
pipe(messages)

# Load model directly
from transformers import AutoTokenizer, AutoModelForCausalLM

tokenizer = AutoTokenizer.from_pretrained("openbmb/MathForm-8B")
model = AutoModelForCausalLM.from_pretrained("openbmb/MathForm-8B", device_map="auto")
messages = [
    {"role": "user", "content": "Who are you?"},
]
inputs = tokenizer.apply_chat_template(
	messages,
	add_generation_prompt=True,
	tokenize=True,
	return_dict=True,
	return_tensors="pt",
).to(model.device)

outputs = model.generate(**inputs, max_new_tokens=40)
print(tokenizer.decode(outputs[0][inputs["input_ids"].shape[-1]:]))

Notebooks
Google Colab
Kaggle
Local Apps Settings

vLLM

How to use openbmb/MathForm-8B with vLLM:

Install from pip and serve model

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

Use Docker

docker model run hf.co/openbmb/MathForm-8B

SGLang

How to use openbmb/MathForm-8B with SGLang:

Install from pip and serve model

# Install SGLang from pip:
pip install sglang
# Start the SGLang server:
python3 -m sglang.launch_server \
    --model-path "openbmb/MathForm-8B" \
    --host 0.0.0.0 \
    --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "openbmb/MathForm-8B",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker images

docker run --gpus all \
    --shm-size 32g \
    -p 30000:30000 \
    -v ~/.cache/huggingface:/root/.cache/huggingface \
    --env "HF_TOKEN=<secret>" \
    --ipc=host \
    lmsysorg/sglang:latest \
    python3 -m sglang.launch_server \
        --model-path "openbmb/MathForm-8B" \
        --host 0.0.0.0 \
        --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "openbmb/MathForm-8B",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Docker Model Runner
How to use openbmb/MathForm-8B with Docker Model Runner:
```
docker model run hf.co/openbmb/MathForm-8B
```

MathForm-8B / README.md

BigDong

update readme (#1)

8f6d09e about 14 hours ago

preview code

Raw

History Blame Contribute Delete

4.82 kB

metadata

license: apache-2.0
language:
  - en
base_model:
  - Qwen/Qwen3-8B
datasets:
  - openbmb/FormalVerse
pipeline_tag: text-generation
library_name: transformers
tags:
  - arxiv:2608.14221
  - lean4
  - autoformalization
  - mathematics
  - formal-verification
  - reasoning

MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

MathForm-8B is an autoformalization model that translates natural-language mathematical statements into Lean 4. It is released with the paper MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement.

The model is trained on FormalVerse through supervised fine-tuning followed by reinforcement learning using Lean compilation and semantic-consistency feedback.

Figure 1: Overview of the MathForm data construction and training pipeline. The system combines Mathlib knowledge retrieval, compilation and semantic verification, and iterative refinement to generate reliable formal data, followed by trajectory reconstruction and training of MathForm-8B.

Results

Pass@8 results on six benchmarks
Figure 2: Pass@8 pass rates (%) under Syntax Check (SC) and Consistency Check (CC) for specialized autoformalizers on six benchmarks. AVG is the equally weighted macro-average across all six benchmarks. For each column, the best result is shown in bold and the second best is underlined.

Usage

Transformers

import torch
from transformers import AutoModelForCausalLM, AutoTokenizer

model_id = "openbmb/MathForm-8B"
tokenizer = AutoTokenizer.from_pretrained(model_id)
model = AutoModelForCausalLM.from_pretrained(
    model_id, torch_dtype=torch.bfloat16, device_map="auto"
)

prompt = (
    "Please convert the following informal math problem to a formal one in Lean 4 with a header. "
    "Use the following theorem names: my_favorite_theorem.\n\n"
    "Show that for every real number x, x^2 is non-negative."
)

messages = [{"role": "user", "content": prompt}]
text = tokenizer.apply_chat_template(messages, tokenize=False, add_generation_prompt=True)
inputs = tokenizer(text, return_tensors="pt").to(model.device)

outputs = model.generate(
    **inputs, max_new_tokens=16384, temperature=0.6, top_p=0.95
)
print(tokenizer.decode(outputs[0][inputs.input_ids.shape[-1]:], skip_special_tokens=True))

vLLM

vllm serve openbmb/MathForm-8B \
  --served-model-name MathForm-8B \
  --dtype bfloat16 \
  --max-model-len 16384

SGLang

python -m sglang.launch_server \
  --model-path openbmb/MathForm-8B \
  --served-model-name MathForm-8B \
  --dtype bfloat16 \
  --context-length 16384

Both servers expose an OpenAI-compatible API at http://localhost:8000/v1/chat/completions.

Recommended Settings

Setting	Value
`temperature`	0.6
`top_p`	0.95
`max_new_tokens`	16384

Evaluation

The evaluation pipeline, benchmark files, and Pass@k scripts are available in the MathForm repository. Compilation checks require a running Kimina Lean Server. The experiments use Lean 4.21.0.

License

This project is licensed under the Apache License 2.0.

Citation

@misc{pu2026mathformscalingmathematicalautoformalization,
      title={MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement}, 
      author={Lushi Pu and Weiming Zhang and Xinheng Xie and Zixuan Fu and Bingxiang He and Hengyu Zhao and Hongya Lyu and Xin Li and Jie Zhou and Yudong Wang},
      year={2026},
      eprint={2608.14221},
      archivePrefix={arXiv},
      primaryClass={cs.AI},
      url={https://arxiv.org/abs/2608.14221}, 
}