From 060e67d235bbe2877e0eedd582815a48adb67fb6 Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Fri, 19 Apr 2024 17:23:58 +0000 Subject: [PATCH] update --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index bdbbfe2..cb93bf0 100644 --- a/README.md +++ b/README.md @@ -306,8 +306,8 @@ After the tactic generator is trained, we combine it with best-first search to p For models without retrieval, run: ```bash -python prover/evaluate.py --data-path data/leandojo_benchmark_4/random/ --ckpt_path PATH_TO_MODEL_CHECKPOINT --split test --num-workers 10 --num-gpus 1 -python prover/evaluate.py --data-path data/leandojo_benchmark_4/novel_premises/ --ckpt_path PATH_TO_MODEL_CHECKPOINT --split test --num-workers 10 --num-gpus 1 +python prover/evaluate.py --data-path data/leandojo_benchmark_4/random/ --ckpt_path PATH_TO_MODEL_CHECKPOINT --split test --num-workers 5 --num-gpus 1 +python prover/evaluate.py --data-path data/leandojo_benchmark_4/novel_premises/ --ckpt_path PATH_TO_MODEL_CHECKPOINT --split test --num-workers 5 --num-gpus 1 ``` For models with retrieval, first use the retriever to index the corpus (pre-computing the embeddings of all premises):