Finetuing CodeLLaMA on LeanDojo

[Some-random]

In my ATP research, I've fine-tuned a LLAMA 7B model using lean_proof_recording and used lean-gym to interact with Lean. Now, I plan to switch to LeanDoJo for improved data collection and Lean interaction. Hence, I have two queries:

1 Which exact version of miniF2F is used in the LeanDoJo paper? Was Meta's bug-reduced version employed?
2 Which repository and commit ID can enable full mathlib3 tracing, as in lean_proof_recording, to assess my fine-tuned LLAMA's performance?

[yangky11]

I'm transferring this issue to Github Discussions (see https://github.com/lean-dojo/LeanDojo#questions-and-bugs)

Regarding the questions themselves, they can be found in the paper by searching for "commit" or in our data generation script: https://github.com/lean-dojo/LeanDojo/blob/main/scripts/generate-benchmark-lean3.ipynb

[wiio12]

Hi @Some-random, do you have any results on LLAMA 7B running with lean-dojo by now? It would be valuable to see how well the Reprover works on a larger language model~.

And Hi @yangky11, great work here! Are you planning on running the Reprover with larger language models?

[yangky11]

@albertqjiang is working on finetuning Mistral and may have insights.

[wiio12]

Recent update:

1. Reducing the training budget helps, even if the training loss and validation loss are nearly identical, the downstream pass@1 varies a lot: (The tb is the abbreviation for training budget)

Model	Pass Rate @1
ReProver (without retrieval)	39%
CodeLlama (lr=5e-5, bs=8, tb=10e)	41%
CodeLlama (lr=5e-5, bs=32, tb=10e)	41%
CodeLlama (lr=5e-5, bs=32, tb=3e)	46%
CodeLlama (lr=5e-5, bs=128, tb=10e)	47%
CodeLlama (Meta setting) (lr=5e-5, bs=100, tb=3.5e, weight_decay=0.1)	46%

2. I just found this paper: Temperature-scaled large language models for Lean proofstep prediction. The paper finetuned the CodeLlama with the LeanDojo Benchmark dataset.

[yangky11]

So the model becomes worse after being trained for too many epochs? That's very interesting!

[tangzhy]

Same observation on Mistral 7b:) @albertqjiang @yangky11 wonder if you see that as well?

[albertqjiang]

yep you should not train too many epochs because it will eventually overfit.

there are things you can do to make that happen later though (the later the overfit, the better the perf I've found). This will come out in my next paper.