YAML Metadata
Warning:
empty or missing yaml metadata in repo card
(https://huggingface.co/docs/hub/model-cards#model-card-metadata)
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
- Downloads last month
- 4
Inference Providers
NEW
This model is not currently available via any of the supported third-party Inference Providers, and
the model is not deployed on the HF Inference API.