58 lines
1.9 KiB
Markdown
58 lines
1.9 KiB
Markdown
---
|
||
language:
|
||
- en
|
||
base_model: deepseek-ai/DeepSeek-R1-Distill-Qwen-7B
|
||
tags:
|
||
- chat
|
||
library_name: transformers
|
||
license: apache-2.0
|
||
---
|
||
|
||
# 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](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-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)
|
||
``` |