Running premise selection using pretrained model/embeddings

[jrr6]

Hi, I'm attempting to run the pretrained model using the demo code in the README, but using the precomputed embeddings published on Huggingface in kaiyuy/premise-embeddings-leandojo-lean4-retriever-byt5-small rather than a small in-file premise array. I had simply taken the demo code and substituted

premise_dict = json.load(open('embeddings/dictionary.json', 'r'))
premises = {int(k): premise_dict[k] for k in premise_dict}

in place of premises and

premise_embs = torch.from_numpy(np.load('embeddings/embeddings.npy')).float()

as a global constant in place of premise_embs, where the embeddings directory contains the Huggingface repo.

However, the output I get does not match the LeanCopilot output: in particular, the embeddings I get from the encoder are dramatically different from those produced by the LeanCopilot FFI. Have I misunderstood how the demo works? Or are the precomputed embeddings intended for use with a different model than kaiyuy/leandojo-lean4-retriever-byt5-small?

Thanks for any guidance.

[yangky11]

It's likely that the precomputed embeddings are out of sync with kaiyuy/leandojo-lean4-retriever-byt5-small. I'll try to update both, and please try again in one or two days.