ReProver fine-tuning

[darabos]

Hi,
We're experimenting with fine-tuning ReProver on a slightly modified Mathlib dataset. We just used the training code in this repo with ReProver instead of ByT5 as the base model. It works, but I'm wondering if this is the right way. It perhaps results in a high initial learning rate and causes the model to forget too much in the first epochs.

Do you think it would be better to continue from ReProver's training checkpoint? Or should we just use a lower learning rate?
Thanks for any tips!

[yangky11]

We tried further finetune the ReProver checkpoint, though the results were not promising. I believe it may have something to do with lean-dojo/LeanDojo#5.