HaimingW/Leandojo-CodeLLama-7b

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