Added reference to paper.
Browse files
README.md
CHANGED
@@ -32,8 +32,8 @@ thereby facilitating significant strides in automated theorem proving.
|
|
32 |
|
33 |
## Model Sources
|
34 |
|
35 |
-
- **Paper:**
|
36 |
-
|
37 |
|
38 |
## Uses
|
39 |
|
@@ -132,7 +132,20 @@ with torch.no_grad():
|
|
132 |
|
133 |
## Training Details
|
134 |
|
135 |
-
The model was fine-tuned with the
|
136 |
dataset. Only entries with permissive licenses were used during the
|
137 |
fine-tuning process.
|
138 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
32 |
|
33 |
## Model Sources
|
34 |
|
35 |
+
- **Paper:** [Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code](https://arxiv.org/abs/2403.12627)
|
36 |
+
- **Dataset:** [florath/coq-facts-props-proofs-gen0-v1](https://huggingface.co/datasets/florath/coq-facts-props-proofs-gen0-v1)
|
37 |
|
38 |
## Uses
|
39 |
|
|
|
132 |
|
133 |
## Training Details
|
134 |
|
135 |
+
The model was fine-tuned with the [florath/coq-facts-props-proofs-gen0-v1](https://huggingface.co/datasets/florath/coq-facts-props-proofs-gen0-v1)
|
136 |
dataset. Only entries with permissive licenses were used during the
|
137 |
fine-tuning process.
|
138 |
|
139 |
+
## Cite
|
140 |
+
|
141 |
+
```
|
142 |
+
@misc{florath2024enhancing,
|
143 |
+
title={Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code},
|
144 |
+
author={Andreas Florath},
|
145 |
+
year={2024},
|
146 |
+
eprint={2403.12627},
|
147 |
+
archivePrefix={arXiv},
|
148 |
+
primaryClass={cs.AI}
|
149 |
+
}
|
150 |
+
```
|
151 |
+
|