28 lines
849 B
Markdown
28 lines
849 B
Markdown
---
|
|
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}},
|
|
}
|
|
``` |