Repository navigation
Tracing miniF2F and mathlib3 #4
Description
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?
Activity
yangky11 commentedon Jul 4, 2023
I'm closing this issue since this is general discussion rather than potential bugs (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