search

lean-dojo / ReProver

Retrieval-Augmented Theorem Provers for Lean
https://leandojo.org
MIT License
229 stars 53 forks source link

The evaluation result on the dataset Minif2f and ProofNet, indexed-corpus-path option #31

Closed irene622 closed 1 year ago

irene622 commented 1 year ago

Hi, at first, thanks for add results of evaluation on the two dataset, Minif2f and the ProofNet. I am currently running the following on the Minif2f!

I have two questions.

  1. The difference between the below two commands is indexed-corpus-path option.

    python prover/evaluate.py --data-path data/leandojo_minif2f/default/  --ckpt_path PATH_TO_MODEL_CHECKPOINT --split test --num-cpus 8 --with-gpus

    and 

    python prover/evaluate.py --data-path data/leandojo_minif2f/default/  --ckpt_path PATH_TO_REPROVER_CHECKPOINT --indexed-corpus-path PATH_TO_INDEXED_CORPUS --split test --num-cpus 8 --with-gpus

    What is the role of indexed-corpus-path option?

  2. I want to confirm your result which can get the result after prover/evaluate.py on the Minif2f dataset. Before, the result can be showed, but now it is hard to find the result... ;) How can I see the evaluation result on the Minif2f and ProofNet??

yangky11 commented 1 year ago

The difference is whether you want to evaluate the model w/ or w/o retrieval, see https://github.com/lean-dojo/ReProver#theorem-proving-evaluation-on-leandojo-benchmark-lean-3-and-lean-4.

evaluate.py prints the result of each theorem to stdout. You can use scripts/stats.py to calculate the metrics, or you can write a simple script by yourself.

irene622 commented 1 year ago

Thank you!

However, I would like to see the results of your evaluation with Minif2f dataset. I think you posted the results on GibHub before, but I can't find it now. Where can I check your results??

yangky11 commented 1 year ago

I don't think it was public before, but I just re-run the model. See https://github.com/lean-dojo/ReProver/discussions/32. Let me know if you also need the result on ProofNet.