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.
The model is fine-tuned on sequences of the form:
[GOAL]tactic-state[PROOFSTEP]next-tactic<|endoftext|>
This format corresponds to the proofstep objective from Han et al ICLR 2022.
The 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}},
}