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)
|
|||
|
|
```
|