wellecks commited on
Commit
d4a5bb5
1 Parent(s): ad032a5

Update README.md

Browse files
Files changed (1) hide show
  1. README.md +3 -3
README.md CHANGED
@@ -2,14 +2,14 @@
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.
 
2
  license: mit
3
  ---
4
 
5
+ ### llmstep: [L]LM proofstep suggestions in Lean
6
  https://github.com/wellecks/llmstep
7
 
8
+ This model is a Pythia-2.8b-deduped 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<|endoftext|>
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.