30hzzh/llmstep-mathlib4-Pythia410m
08
llmstep project
This model is a Pythia-410m-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 model is a Pythia-410m-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|>