question about reproducing results from paper

[maverick-harmonic]

Hello,
My goal was to reproduce the results of tactic generation without retrieval on the novel premises split. Here is what I did:

1. I ran one step of training with ReProver/generator/confs/cli_novel_premises.yaml [1] to create a checkpoint that I can use with the evaluation script [2]
2. I ran the evaluation script like so: PYTHONPATH=$PYTHONPATH:~/w/lean-dojo/LeanDojo/src python prover/evaluate.py --data-path data/leandojo_benchmark/novel_premises/ --ckpt_path lightning_checkpoints/last.ckpt/ --split test --num-cpus 4 --with-gpus --timeout 60
3. I loaded the results and ran [3] to get a 0.29 pass rate. This is significantly higher than the 0.229 pass rate described in the paper.

Any ideas/tips on what I'm doing wrong?

[1] Here's the diff I used against commit 762c32fc6e8c6e29fa446dada8aac27f678fe4c8.

git diff generator/confs/cli_novel_premises.yaml
diff --git a/generator/confs/cli_novel_premises.yaml b/generator/confs/cli_novel_premises.yaml
index 7bc4ec4..47139bc 100644
--- a/generator/confs/cli_novel_premises.yaml
+++ b/generator/confs/cli_novel_premises.yaml
@@ -10,7 +10,8 @@ trainer:
       offload_optimizer: false
       cpu_checkpointing: false
   gradient_clip_val: 1.0
-  max_steps: 500000
+  #max_steps: 500000
+  max_steps: 1
   check_val_every_n_epoch: 2
   num_sanity_val_steps: 0
   callbacks:
@@ -19,9 +20,11 @@ trainer:
         logging_interval: step
     - class_path: pytorch_lightning.callbacks.ModelCheckpoint
       init_args:
+        dirpath: lightning_checkpoints/
         verbose: true
         save_top_k: 1
         save_last: true
+        every_n_train_steps: 1
         monitor: Pass@1_val
         mode: max
     - class_path: pytorch_lightning.callbacks.EarlyStopping
@@ -32,7 +35,8 @@ trainer:
         verbose: true

 model:
-  model_name: google/byt5-small
+  #model_name: google/byt5-small
+  model_name: kaiyuy/leandojo-lean3-tacgen-byt5-small
   lr: 5e-4
   warmup_steps: 2000
   num_beams: 1
@@ -47,7 +51,7 @@ data:
   corpus_path: data/leandojo_benchmark/corpus.jsonl
   keep_marks: true
   preds_path: null
-  batch_size: 8
+  batch_size: 2
   eval_batch_size: 64
   max_seq_len: 2300
   p_drop: 0.5

[2] See below:

lean-dojo/ReProver (main) $ find lightning_checkpoints/
lightning_checkpoints/
lightning_checkpoints/last.ckpt
lightning_checkpoints/last.ckpt/zero_to_fp32.py
lightning_checkpoints/last.ckpt/checkpoint
lightning_checkpoints/last.ckpt/checkpoint/bf16_zero_pp_rank_0_mp_rank_00_optim_states.pt
lightning_checkpoints/last.ckpt/checkpoint/mp_rank_00_model_states.pt
lightning_checkpoints/last.ckpt/latest

[3]

In [4]: with open('ede1e960-b1cf-4689-a1f4-fda472963978_results.pickle', 'rb') as f: results = pickle.load(f)

In [5]:     # Calculate the result statistics.
   ...:     num_proved = num_failed = num_discarded = 0
   ...:     for r in results:
   ...:         if r is None:
   ...:             num_discarded += 1
   ...:         elif r.status == Status.PROVED:
   ...:             num_proved += 1
   ...:         else:
   ...:             num_failed += 1
   ...:

In [6]: print(f"Pass@1: {num_proved / (num_proved + num_failed)}")
Pass@1: 0.29464732366183094

[yangky11]

Hi,

If I'm understanding correctly, the model is trained for only one step, so it's essentially not different from the pretrained ByT5?

Can you run evaluate.py in debug mode (environment variable VERBOSE=1) and share the logs?

[maverick-harmonic]

Hi @yangky11 , before running it for one step I changed the configuration to load weights from the pretrained model on huggingface:

I can run evaluate.py in debug mode but it produces a ton of log output. Is there specific output you'd like to see?

[yangky11]

Oh, OK. That's because kaiyuy/leandojo-lean3-tac-gen-byt5-small was trained using the random split. So it has probably seen the testing data in the novel_premises split.

[maverick-harmonic]

Great, that makes sense. It's a good datapoint to have that delta as well.

Any chance you could upload the model trained on the novel_premises split? I would love to just baseline everything before going deeper into trainings.

[yangky11]

I just uploaded the checkpoints in PyTorch Lightning format so that you no longer need the 1-step training trick. https://huggingface.co/kaiyuy/leandojo-pl-ckpts/tree/main

[maverick-harmonic]

That’s fantastic. Thanks!

…

On Thu, Jul 27, 2023 at 4:09 PM Kaiyu Yang ***@***.***> wrote: I just uploaded the checkpoints in PyTorch Lightning format so that you no longer need the 1-step training trick. https://huggingface.co/kaiyuy/leandojo-pl-ckpts/tree/main — Reply to this email directly, view it on GitHub <#22 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/BBRKDHPAI35FN6RQNOYIMGTXSLYMBANCNFSM6AAAAAA22VTMQ4> . You are receiving this because you authored the thread.Message ID: ***@***.***>