TheoremLlama

This is the official repository for all the code of TheoremLlama for uploading the training and inference code of the paper. The code will be available soon. You can now try our model checkpoints and dataset at:

• TheoremLlama model at: https://huggingface.co/RickyDeSkywalker/TheoremLlama
• Open Bootstrapped Theorem (OBT) dataset at: https://huggingface.co/datasets/RickyDeSkywalker/OpenBootstrappedTheorem

[ArXiv]

Updates:

• 10th Oct 2024: update MiniF2F evaluation code

Test on MiniF2F dataset

Setup the environment:

pip install -r requirements.txt

Setup the env variable in eval_MiniF2F.py. Default settings are:

CUDA_DEVICE_ID=1
BATCH_SIZE=4
PROOF_NUM_PER_THEOREM=32
MODEL_ID = "RickyDeSkywalker/TheoremLlama"
CKPT_PATH = "./Generated_proof_ckpts/MiniF2F_Valid/test_output"
SAVE_PATH = './Generated_proof/MiniF2F_Valid/test_output'
dataset_split = "test"

Run the evaluation code:

python eval_MiniF2F.py

You can find the generated proof in SAVE_PATH and the ckpts for the proof in CKPT_PATH.

Citation:

@misc{wang2024theoremllamatransforminggeneralpurposellms,
      title={TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts}, 
      author={Ruida Wang and Jipeng Zhang and Yizhen Jia and Rui Pan and Shizhe Diao and Renjie Pi and Tong Zhang},
      year={2024},
      eprint={2407.03203},
      archivePrefix={arXiv},
      primaryClass={cs.FL},
      url={https://arxiv.org/abs/2407.03203}, 
}