Update README.md
Browse files
README.md
CHANGED
@@ -2,10 +2,19 @@
|
|
2 |
license: mit
|
3 |
---
|
4 |
|
5 |
-
Default language model for `llmstep: [L]LM proofstep suggestions in Lean
|
6 |
https://github.com/wellecks/llmstep
|
7 |
|
8 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
9 |
|
10 |
```
|
11 |
@misc{llmstep,
|
|
|
2 |
license: mit
|
3 |
---
|
4 |
|
5 |
+
Default language model for `llmstep: [L]LM proofstep suggestions in Lean` \
|
6 |
https://github.com/wellecks/llmstep
|
7 |
|
8 |
+
This model is a Pythia 2.8b language model fine-tuned on [LeanDojo Benchmark 4](https://zenodo.org/record/8040110).
|
9 |
+
|
10 |
+
The model is fine-tuned on sequences of the form:
|
11 |
+
```bash
|
12 |
+
[GOAL]tactic-state[PROOFSTEP]next-tactic[END]
|
13 |
+
```
|
14 |
+
This format corresponds to the proofstep objective from [Han et al ICLR 2022](https://arxiv.org/abs/2102.06203).\
|
15 |
+
The [python/train](python/train) directory in the repository shows how the model was fine-tuned.
|
16 |
+
|
17 |
+
Please see the repository for more details.
|
18 |
|
19 |
```
|
20 |
@misc{llmstep,
|