ReProver

ReProver copied to clipboard

RuntimeError: CUDA error: unspecified launch failure

1

Hi, Thanks for your work. I want to reproduce the training process of the Premise Retriever. There are no issues during training, but there is a bug during testing. I...

yifan123

Speed up

1

Solved the problem of low GPU usage

huolongguo1O

Supplementary dependent library

1

Supplementary dependent library

huolongguo1O

Evaluation on multiple GPUs

1

Hi there! I am trying to run evaluation with multiple GPUs. I have ran everything in './scripts/minimal_example.sh'. Running on 1 GPU works perfectly, however when I pass in more than...

ezhang7423

Question about released checkpoint split strategy

1

Hi, thanks for the great work on LeanDojo! Could you clarify what data split was used to train the released checkpoint(tactic generator and premise retriever) on huggingface? Was it trained...

mikeljl

Many missing premises while training premise selector.

4

Hello, I was trying to train the premise selector (specifically, this command: `python retrieval/main.py fit --config retrieval/confs/cli_lean4_random.yaml --trainer.logger.name train_retriever_random --trainer.logger.save_dir logs/train_retriever_random`) and after wandb sets itself up, I get a...

ketchupfan