Converting Hugging Face Safetensor to Checkpoint

[Bojun-Feng]

Hello, I've been trying to reproduce the results of the paper through evaluating the hugging face model on the benchmark (without indexing).

However, I am having some trouble applying the hugging face safetensors to compatible torch lightning check points for evaluation. Currently I am using torch to change the safe tensor to a binary checkpoint:

# ... download model from https://huggingface.co/kaiyuy/leandojo-lean4-tacgen-byt5-small
ckpt = load_file('model.safetensors')
torch.save(ckpt, '/content/model.bin')

Then, I run command according to the instructions:

python prover/evaluate.py 
  --data-path data/leandojo_benchmark_4/random/
  --ckpt_path /content/model.bin
  --split test
  --num-workers 5
  --num-gpus 1

However, it seems that dictionary keys are missing in the resulting checkpoint, I get a dictionary error for 'pytorch_lightning_version'.

I first manually added the pytorch lightning version, but am not sure what the parameter should be for other missing parameters such as 'max_inp_seq_len', and 'max_oup_seq_len'. Is there a conveinent way I can load the model from the safetensors or gain access to the original model checkpoints? I looked online but found no relevant information.

I am new to the repo and lean in general so this might be a stupid question. Would appreaciate any useful information or suggestions.

[yangky11]

You probably want to use the PyTorch Lightning checkpoints here: https://huggingface.co/kaiyuy/leandojo-pl-ckpts

[Bojun-Feng]

Thanks for the response @yangky11! I tried out your suggestion and am facing the same issues as @xiaoxin-yin.

Additionally, there are quite a few different models in the checkpoint, and I am not sure what they represent. What model should I use for benching without indexed data? Also, the checkpoints does not seem to align with the hugging face models and seem to be correlated with different datasets. Is it because the checkpoints already contain the premises?

I'm new to leandojo and lean so I'm sorry if my questions are silly. After I figure out how to benchmark with the checkpoints, I would be happy to write up some documentation and a demo colab notebook for future users!

[yangky11]

It looks like the error is because the ReProver's checkpoint contains a path to the retriever checkpoint, which points to the path when I trained the retriever (lightning_logs/retriever_novel_premises/checkpoints/epoch=3-step=172908.ckpt). Could you please try renaming the reprover_novel_premises.ckpt folder in https://huggingface.co/kaiyuy/leandojo-pl-ckpts to lightning_logs/retriever_novel_premises/checkpoints/epoch=3-step=172908.ckpt?

[yangky11]

@Bojun-Feng

• generator_novel_premises.ckpt: Tactic generator (without retrieval) trained on the novel_premises split of LeanDojo Benchmark.
• generator_random.ckpt: Tactic generator (without retrieval) trained on the random split of LeanDojo Benchmark.
• retriever_random.ckpt: Retriever trained on the random split.
• retriver_novel_premises.ckpt: Retriever trained on the novel_premises split.
• reprover_novel_premises.ckpt: Retrieval-augmented tactic generator trained on novel_premises.
• reprover_random.ckpt: Retrieval-augmented tactic generator trained on random.

[xiaoxin-yin]

Thank you, @yangky11 ! It works after I rename the checkpoint to lightning_logs/retriever_novel_premises/checkpoints/epoch=3-step=172908.ckpt. However, I found that checkpoints like "kaiyuy/leandojo-lean4-retriever-tacgen-byt5-small" work better than those in https://huggingface.co/kaiyuy/leandojo-pl-ckpts. Just wondering if it is expected.

[yangky11]

I expect them to be the same models, only in different formats.

[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.