This is a CodeLlama-7b model fine-tuned on LeanDojo Benchmark
The performance is comparable with the paper Temperature-scaled large language models for Lean proofstep prediction with around 57.7 pass@1 accuracy on LeanDojo "random" benchmark.
The training lines are formatted as follow:
GOAL $(tactic state) PROOFSTEP $(tactic)
For inference, use the following line:
GOAL $(tactic state) PROOFSTEP