How to reproduce the results from paper

[monkeytim19]

Hi, I've been trying to reproduce the results that were given in the LeanDojo: Theorem Proving with Retrieval-Augmented Language Models paper, specifically the results stated in Appendix D, Table C.

However, I am slightly confused about the instructions given in the repo. In particular, under the Theorem Proving Evaluation on LeanDojo Benchmark section, when trying to use the pre-trained retriever to index the entire LeanDojo Benchmark corpus, the code states:

python retrieval/index.py --ckpt_path PATH_TO_RETRIEVER_CHECKPOINT --corpus-path data/leandojo_benchmark_4/corpus.jsonl --output-path PATH_TO_INDEXED_CORPUS
# Do it separately for two data splits. 

Could you please clarify why it's necessary to run this process separately for the random and novel_premises data splits? Since the retriever should have been pre-trained on the entire LeanDojo Benchmark, I don't understand why different data splits would generate different indexed corpora.

Perhaps I made a mistake interpreting the instructions, but It would be nice if a clarification could be made on this, thanks very much!

[yangky11]

The retriever is trained on only the training data not the entire LeanDojo Benchmark. At this point, you should have two different PATH_TO_RETRIEVER_CHECKPOINT: one for random and one for novel_premises.

[monkeytim19]

Thanks and I appreciate the swift reply.

Just to follow up, since the trained models from Hugging Face (e.g. kaiyuy/leandojo-lean4-tacgen-byt5-small) do not specify which data split it was trained using, does it mean that to replicate the results from the paper, it is necessary to train all the models from scratch with the respective data split (random and novel_premises)?

Many thanks.

[yangky11]

The most recent model checkpoints are here: https://huggingface.co/kaiyuy/leandojo-pl-ckpts

[yangky11]

Update: The new evaluation script takes Hugging Face (instead of PyTorch Ligthning) checkpoints as input. You can directly use models such as leandojo-lean4-tacgen-byt5-small. Please see the updated README for details. As a result, https://huggingface.co/kaiyuy/leandojo-pl-ckpts has been deleted.

[1854039]

Hello, I trained the latest huggingface model on random and novel with 0 learning rate as README said. The results are much better than those in the paper, have you improved the retrieval model? Or what data set is the model file on HF trained in? Thank you so much!

[yangky11]

@1854039 What were the results and under what experimental setup?

Sine the paper was published, various bug fixes and improvements have been incorporated into LeanDojo and Lean itself. The models on HF were trained on the latest version https://zenodo.org/records/12740403, which was extracted in July 2024 from mathlib4. Main results in the table used Lean 3 (https://zenodo.org/records/10114157), which has retired and is no longer supported by LeanDojo. The paper's appendix also has results on Lean 4, though with an older dataset version (probably v3).