library_name, license, base_model, tags, model-index

library_name	license	base_model	tags	model-index
transformers	other	formalmathatepfl/deepseek-prover-v2-cpt	llama-factory full generated_from_trainer	name results deepseek-prover-v2-7b-lean-cpt-sft-32k

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

This model is a fine-tuned version of formalmathatepfl/deepseek-prover-v2-cpt on the lean_sft dataset. It achieves the following results on the evaluation set:

• Loss: 0.0615

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.0843	0.1283	600	0.0813
0.0712	0.2566	1200	0.0711
0.0654	0.3849	1800	0.0673
0.0675	0.5131	2400	0.0647
0.0613	0.6414	3000	0.0631
0.0604	0.7697	3600	0.0621
0.0625	0.8980	4200	0.0616

Framework versions

• Transformers 4.57.3
• Pytorch 2.9.0+cu129
• Datasets 3.6.0
• Tokenizers 0.22.1