File size: 505 Bytes
64256e2 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
This is a CodeLlama-7b model fine-tuned on [LeanDojo Benchmark](https://github.com/lean-dojo/LeanDojo)
The performance is comparable with the paper [Temperature-scaled large language models for Lean proofstep prediction](https://mathai2023.github.io/papers/25.pdf) 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
``` |