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

<!-- This model card has been generated automatically according to the information the Trainer had access to. You
should probably proofread and complete it, then remove this comment. -->

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

This model is a fine-tuned version of [formalmathatepfl/deepseek-prover-v2-cpt](https://huggingface.co/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