search

lean-dojo / ReProver

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

How to apply the dataset, miniF2F to ReProver? #23

Closed irene622 closed 12 months ago

irene622 commented 1 year ago

Hi, I read your paper, and ReProver can be experienced for miniF2F dataset. I try to apply lean data of miniF2F, but I have few ambiguous about the experiment..

  1. The lean file in miniF2F are different from your benchmark dataset. Then, do I have to change miniF2F to the benchmark data format such as e.g, transfer to json format and {"link", "commit"...}? If yes, what is a proper input per keys in json?

  2. The experiment for miniF2F is done without retriever? or not? For only test, applying miniF2F is runned on theorem proving without retriever??

Thank you for time!

yangky11 commented 1 year ago

Hi,

You can use LeanDojo to extract data from miniF2F, as shown at the end of this Jupyter notebook.

Then you can use prover/evaluate.py to evaluate the model (trained on mathlib) on miniF2F.

The miniF2F numbers we reported were w/ retrieval, though w/o retrieval should also be close. Theorems in miniF2F usually do not rely on obsolete premises.