初始化项目，由ModelHub XC社区提供模型

Model: stepfun-ai/StepFun-Prover-Preview-7B
Source: Original Platform

README.md

@@ -0,0 +1,58 @@
+---
+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)
+```