File size: 849 Bytes
cbe5586 4fd168a d4a5bb5 4fd168a d4a5bb5 ad032a5 d4a5bb5 ad032a5 4fd168a |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 |
---
license: mit
---
### llmstep: [L]LM proofstep suggestions in Lean
https://github.com/wellecks/llmstep
This model is a Pythia-2.8b-deduped language model fine-tuned on [LeanDojo Benchmark 4](https://zenodo.org/record/8040110).
The model is fine-tuned on sequences of the form:
```bash
[GOAL]tactic-state[PROOFSTEP]next-tactic<|endoftext|>
```
This format corresponds to the proofstep objective from [Han et al ICLR 2022](https://arxiv.org/abs/2102.06203).\
The [python/train](python/train) directory in the repository shows how the model was fine-tuned.
Please see the repository for more details.
```
@misc{llmstep,
author = {Sean Welleck},
title = {llmstep: LLM proofstep suggestions in Lean},
year = {2023},
publisher = {GitHub},
journal = {GitHub repository},
howpublished = {\url{https://github.com/wellecks/llmstep}},
}
``` |