Add library name and pipeline tag
Browse filesThis PR adds the missing `library_name` and `pipeline_tag` to the model card metadata. The `library_name` is set to `transformers` because the model uses the transformers library. The `pipeline_tag` is set to `text-generation` because the model generates text (Lean code).
README.md
CHANGED
@@ -1,14 +1,15 @@
|
|
1 |
---
|
2 |
-
license: mit
|
3 |
-
datasets:
|
4 |
-
- kfdong/STP_Lean_SFT
|
5 |
base_model:
|
6 |
- deepseek-ai/DeepSeek-Prover-V1.5-SFT
|
|
|
|
|
|
|
|
|
|
|
7 |
---
|
8 |
|
9 |
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).
|
10 |
|
11 |
-
|
12 |
```tex
|
13 |
@article{dong2025beyond,
|
14 |
title={Beyond Limited Data: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving},
|
|
|
1 |
---
|
|
|
|
|
|
|
2 |
base_model:
|
3 |
- deepseek-ai/DeepSeek-Prover-V1.5-SFT
|
4 |
+
datasets:
|
5 |
+
- kfdong/STP_Lean_SFT
|
6 |
+
license: mit
|
7 |
+
library_name: transformers
|
8 |
+
pipeline_tag: text-generation
|
9 |
---
|
10 |
|
11 |
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).
|
12 |
|
|
|
13 |
```tex
|
14 |
@article{dong2025beyond,
|
15 |
title={Beyond Limited Data: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving},
|