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)