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.

Quick Start with vLLM

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 and . The REPL feedback will be provided between and . 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], # ,
include_stop_str_in_output=True,
)

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