---
title: StepFun-Prover-Preview-32B
canonical_url: "https://www.modelscope.cn/models/stepfun-ai/StepFun-Prover-Preview-32B"
md_url: "https://www.modelscope.cn/models/stepfun-ai/StepFun-Prover-Preview-32B.md"
repository: stepfun-ai/StepFun-Prover-Preview-32B
last_updated: 2025-08-13
license: apache-2.0
pipeline_tag: text-generation
tasks:
  - text-generation
model_type:
  - qwen2
architectures:
  - Qwen2ForCausalLM
base_model:
  - deepseek-ai/DeepSeek-R1-Distill-Qwen-32B
base_model_relation: finetune
library_name:
  - transformer
  - safetensors
  - pytorch
frameworks:
  - pytorch
language:
  - en
inference_backends:
  - "deploy_task text/emb"
  - "lmdeploy 0.9.1"
  - "lmdeploy_turbomind 0.9.1"
  - "sglang 0.5.2"
  - "vllm 0.9.2"
downloads: 148
stars: 1
tags:
  - chat
---

# StepFun-Prover-Preview-32B

> StepFun-Prover-Preview-32B - stepfun-ai 在 ModelScope 开源的模型。StepFun-Prover-Preview-32B

stepfun-ai/StepFun-Prover-Preview-32B 是 ModelScope 魔搭社区上的text-generation模型，采用 apache-2.0 许可，基于 deepseek-ai/DeepSeek-R1-Distill-Qwen-32B 构建，可用 deploy_task text/emb、lmdeploy 0.9.1、lmdeploy_turbomind 0.9.1 部署。

- **Repository**: stepfun-ai/StepFun-Prover-Preview-32B
- **License**: apache-2.0
- **Tasks**: text-generation
- **Base model**: deepseek-ai/DeepSeek-R1-Distill-Qwen-32B
- **Inference backends**: deploy_task text/emb, lmdeploy 0.9.1, lmdeploy_turbomind 0.9.1, sglang 0.5.2, vllm 0.9.2
- **Tags**: chat
- **Downloads**: 148
- **Stars**: 1
- **Last updated**: 2025-08-13

Source: https://www.modelscope.cn/models/stepfun-ai/StepFun-Prover-Preview-32B

---

# StepFun-Prover-Preview-32B

**StepFun-Prover-Preview-32B** is a theorem proving model developed by StepFun Team. It can iteratively refine the proof sketch via interacting with Lean4, and achieve 70.0% accuracy with Pass@1 on MiniF2F-test. Advanced usage examples can be seen in [github](https://github.com/stepfun-ai/StepFun-Prover-Preview).

# Quick Start with vLLM

```python
from vllm import LLM, SamplingParams
from transformers import AutoTokenizer

model_name = "Stepfun/Stepfun-Prover-Preview-32B"
model = LLM(
    model=model_name,
    tensor_parallel_size=8,
    )
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)
```