Instructions to use stepfun-ai/StepFun-Prover-Preview-7B with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use stepfun-ai/StepFun-Prover-Preview-7B with Transformers:

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

pipe = pipeline("text-generation", model="stepfun-ai/StepFun-Prover-Preview-7B")
messages = [
    {"role": "user", "content": "Who are you?"},
]
pipe(messages)

# Load model directly
from transformers import AutoTokenizer, AutoModelForCausalLM

tokenizer = AutoTokenizer.from_pretrained("stepfun-ai/StepFun-Prover-Preview-7B")
model = AutoModelForCausalLM.from_pretrained("stepfun-ai/StepFun-Prover-Preview-7B")
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

vLLM

How to use stepfun-ai/StepFun-Prover-Preview-7B with vLLM:

Install from pip and serve model

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

Use Docker

docker model run hf.co/stepfun-ai/StepFun-Prover-Preview-7B

SGLang

How to use stepfun-ai/StepFun-Prover-Preview-7B 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 "stepfun-ai/StepFun-Prover-Preview-7B" \
    --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": "stepfun-ai/StepFun-Prover-Preview-7B",
		"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 "stepfun-ai/StepFun-Prover-Preview-7B" \
        --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": "stepfun-ai/StepFun-Prover-Preview-7B",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Docker Model Runner
How to use stepfun-ai/StepFun-Prover-Preview-7B with Docker Model Runner:
```
docker model run hf.co/stepfun-ai/StepFun-Prover-Preview-7B
```

StepFun-Prover-Preview-7B

StepFun-Prover-Preview-7B is a theorem proving model developed by StepFun Team. It can iteratively refine the proof sketch via interacting with Lean4, and achieve 66.0% accuracy with Pass@1 on MiniF2F-test. Advanced usage examples can be seen in github.

Quick Start with vLLM

from vllm import LLM, SamplingParams
from transformers import AutoTokenizer

model_name = "Stepfun/Stepfun-Prover-Preview-7B"
model = LLM(
    model=model_name,
    tensor_parallel_size=4,
    )
tokenizer = AutoTokenizer.from_pretrained(model_name, trust_remote_code=True)

formal_problem = """
import Mathlib

theorem test_theorem (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) :
    (x^2 - z^2) / (y + z) + (y^2 - x^2) / (z + x) + (z^2 - y^2) / (x + y) ≥ 0 := by
""".strip()

system_prompt = "You will be given an unsolved Lean 4 problem. Think carefully and work towards a solution. At any point, you may use the Lean 4 REPL to check your progress by enclosing your partial solution between <sketch> and </sketch>. The REPL feedback will be provided between <REPL> and </REPL>. Continue this process as needed until you arrive at a complete and correct solution."

user_prompt = f"```lean4\n{formal_problem}\n```"

dialog = [
  {"role": "system", "content": system_prompt},
  {"role": "user", "content": user_prompt}
] 

prompt = tokenizer.apply_chat_template(dialog, tokenize=False, add_generation_prompt=True)

sampling_params = SamplingParams(
    temperature=0.999,
    top_p=0.95,
    top_k=-1,
    max_tokens=16384,
    stop_token_ids=[151643, 151666], # <｜end▁of▁sentence｜>, </sketch>
    include_stop_str_in_output=True,
)

output = model.generate(prompt, sampling_params=sampling_params)
output_text = output[0].outputs[0].text
print(output_text)