[QUESTION, BUG] all theorem are discarded when using miniF2F

[irene622]

related issue : https://github.com/lean-dojo/ReProver/issues/23

I run the following code to evaluate the ReProver model on miniF2F dataset.

1. Extracting the datasets using the below code of here
2. Run prover/evaluate.py

   python prover/evaluate.py --data-path <path>/leandojo_minif2f/default  --ckpt_path <path>/ReProver/lightning_logs/version_232973/checkpoints/last.ckpt --split val --num-cpus 16

Then, I have results as the attached file mini13-238259.err.txt

My results looks strange, because it print

INFO     | __main__:main:166 - Evaluation done! 0 theorems proved, 0 theorems failed, 244 non-theorems     discarded

And results show many EOFwarnings like

WARNING  | prover.proof_search:search:142 - EOF

Is it right result? What is wrong part, extracting datasets or evaluate.py? and How to fix it..?

My environment is CONTAINER="native" and no GPU.

[yangky11]

Hi,

It would be great if you could send me your leandojo_minif2f and lightning_logs/version_232973/checkpoints. I'll take a look and try to reproduce the problem

[irene622]

I leave the link to download the folders lightning_logs/version_232973. It is almost 1GB.

Additionally, my Lean version is

Lean (version 3.51.1, commit cce7990ea86a, Release)

and, lean-dojo version is

lean-dojo                 1.2.4

[yangky11]

I would also need the leandojo_minif2f

[irene622]

leandojo_minif2f.zip Oh, I miss it... I am confused why I have EOF error...

[yangky11]

Just an update: I've been swamped recently and will be able to take a look next week.

[yangky11]

I leave the link to download the folders lightning_logs/version_232973. It is almost 1GB.

Additionally, my Lean version is

Lean (version 3.51.1, commit cce7990ea86a, Release)

and, lean-dojo version is

lean-dojo                 1.2.4

@irene622 The model checkpoint directory is empty.

[irene622]

I don't know why... HERE is the downloading link. I upload again the folder instead of a zip file.

[irene622]

I think my problem is solved by using server which is available Docker.

Close the issue.