Instructions to use formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e with Transformers:

# Use a pipeline as a high-level helper
from transformers import pipeline

pipe = pipeline("text-generation", model="formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e")
messages = [
    {"role": "user", "content": "Who are you?"},
]
pipe(messages)

# Load model directly
from transformers import AutoTokenizer, AutoModelForCausalLM

tokenizer = AutoTokenizer.from_pretrained("formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e")
model = AutoModelForCausalLM.from_pretrained("formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e")
messages = [
    {"role": "user", "content": "Who are you?"},
]
inputs = tokenizer.apply_chat_template(
	messages,
	add_generation_prompt=True,
	tokenize=True,
	return_dict=True,
	return_tensors="pt",
).to(model.device)

outputs = model.generate(**inputs, max_new_tokens=40)
print(tokenizer.decode(outputs[0][inputs["input_ids"].shape[-1]:]))

Notebooks
Google Colab
Kaggle
Local Apps Settings

vLLM

How to use formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e with vLLM:

Install from pip and serve model

# Install vLLM from pip:
pip install vllm
# Start the vLLM server:
vllm serve "formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e"
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:8000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker

docker model run hf.co/formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e

SGLang

How to use formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e with SGLang:

Install from pip and serve model

# Install SGLang from pip:
pip install sglang
# Start the SGLang server:
python3 -m sglang.launch_server \
    --model-path "formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e" \
    --host 0.0.0.0 \
    --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker images

docker run --gpus all \
    --shm-size 32g \
    -p 30000:30000 \
    -v ~/.cache/huggingface:/root/.cache/huggingface \
    --env "HF_TOKEN=<secret>" \
    --ipc=host \
    lmsysorg/sglang:latest \
    python3 -m sglang.launch_server \
        --model-path "formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e" \
        --host 0.0.0.0 \
        --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Docker Model Runner
How to use formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e with Docker Model Runner:
```
docker model run hf.co/formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e
```

deepseek-prover-v2-7b-lean-cpt-sft-feedback-32k

This model is a fine-tuned version of deepseek-ai/DeepSeek-Prover-V2-7B on the lean_sft_feedback dataset. It achieves the following results on the evaluation set:

Loss: 0.0217

Model description

More information needed

Intended uses & limitations

More information needed

Training and evaluation data

More information needed

Training procedure

Training hyperparameters

The following hyperparameters were used during training:

learning_rate: 1e-05
train_batch_size: 2
eval_batch_size: 2
seed: 42
distributed_type: multi-GPU
num_devices: 8
total_train_batch_size: 16
total_eval_batch_size: 16
optimizer: Use OptimizerNames.ADAMW_TORCH with betas=(0.9,0.999) and epsilon=1e-08 and optimizer_args=No additional optimizer arguments
lr_scheduler_type: cosine
lr_scheduler_warmup_ratio: 0.05
num_epochs: 1.0

Training results

Training Loss	Epoch	Step	Validation Loss
0.0399	0.0827	1000	0.0343
0.0261	0.1654	2000	0.0284
0.0283	0.2481	3000	0.0264
0.0228	0.3308	4000	0.0250
0.0215	0.4135	5000	0.0242
0.0216	0.4962	6000	0.0235
0.0228	0.5789	7000	0.0229
0.0214	0.6616	8000	0.0225
0.0232	0.7444	9000	0.0221
0.0205	0.8271	10000	0.0219
0.0214	0.9098	11000	0.0218
0.0241	0.9925	12000	0.0217

Framework versions

Transformers 4.57.3
Pytorch 2.9.0+cu129
Datasets 3.6.0
Tokenizers 0.22.1

Downloads last month: 537

Safetensors

Model size

7B params

Tensor type

BF16

Model tree for formalmathatepfl/deepseek-prover-v2-cpt-sft-feedback-1e

Base model

deepseek-ai/DeepSeek-Prover-V2-7B

Finetuned

(7)

this model