45 lines
1.5 KiB
Markdown
45 lines
1.5 KiB
Markdown
---
|
|
base_model:
|
|
- deepseek-ai/DeepSeek-Prover-V1.5-SFT
|
|
datasets:
|
|
- kfdong/STP_Lean
|
|
- internlm/Lean-Workbook
|
|
license: mit
|
|
pipeline_tag: text-generation
|
|
library_name: transformers
|
|
---
|
|
|
|
This is the final Self-play Theorem Prover model as described in the paper [https://arxiv.org/abs/2502.00212](https://arxiv.org/abs/2502.00212). The training and evalution code is avaliable [here](https://github.com/kfdong/STP/tree/main).
|
|
|
|
|
|
```tex
|
|
@article{dong2025beyond,
|
|
title={Beyond Limited Data: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving},
|
|
author={Dong, Kefan and Ma, Tengyu},
|
|
journal={arXiv preprint arXiv:2502.00212},
|
|
year={2025}
|
|
}
|
|
```
|
|
|
|
## 1. Evaluation Results
|
|
|
|
The table below compares the pass@3200 performance of STP (our model) and DeepSeek-Prover-V1.5 on miniF2F-test and ProofNet-test.
|
|
|
|
<div align="center">
|
|
|
|
| | miniF2F-test | ProofNet-test |
|
|
|--------|------------------|------------------|
|
|
| **DeepSeek-Prover-V1.5-SFT** | 53.3% ± 0.5% | 21.0% ± 0.9% |
|
|
| **DeepSeek-Prover-V1.5-RL** | 54.9% ± 0.7% | 22.0% ± 0.5% |
|
|
| **STP** | **61.7% ± 0.6%** | **23.1% ± 0.5%** |
|
|
|
|
</div>
|
|
|
|
## 2. Dataset
|
|
|
|
We also release the dataset [here](https://huggingface.co/datasets/kfdong/STP_Lean), which contains:
|
|
- Extracted examples from mathlib4,
|
|
- Generated correct proofs of statements in LeanWorkbook,
|
|
- Generated correct proofs of conjectures proposed by our model during self-play training.
|
|
|
|
Our final model is finetuned from DeepSeek-Prover-V1.5-SFT with this dataset for 1 epoch. |