This is the final Self-play Theorem Prover model as described in the paper
https://arxiv.org/abs/2502.00212. The training and evalution code is avaliable
here.
1@article{dong2025beyond,
2 title={Beyond Limited Data: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving},
3 author={Dong, Kefan and Ma, Tengyu},
4 journal={arXiv preprint arXiv:2502.00212},
5 year={2025}
6}
The table below compares the pass@3200 performance of STP (our model) and DeepSeek-Prover-V1.5 on miniF2F-test and ProofNet-test.
We also release the dataset
here, which contains:
Our final model is finetuned from DeepSeek-Prover-V1.5-SFT with this dataset for 1 epoch.
