AttributeError: `FewShotGptPolicy` object has no attribute `reset_last_action`

[jogobeny]

Hi,

I am experimenting with running COPRA on Llama 3.1. I have added my own config and updated the chat format to match Llama 3.1.

When I run simple_benchmark_lean4, it sometimes completes successfully, but occasionally I get the following exception:

2025-09-24 23:31:50,315 - __main__ - ERROR - Exception occurred while proving lemma: test in file data/test/lean4_proj/Lean4Proj/Temp.lean: 'FewShotGptPolicy' object has no attribute 'reset_last_action'
Traceback (most recent call last):
  File "/home/.../.../copra/src/copra/main/eval_benchmark.py", line 405, in _run_prover
    agent.run_episodes_till_stop(
  File "/home/.../.../copra/src/copra/agent/simple_proof_agent.py", line 55, in run_episodes_till_stop
    self._run_episode_as_per_policy(env, stop_policy, policy_info_message, render)
  File "/home/.../.../copra/src/copra/agent/simple_proof_agent.py", line 88, in _run_episode_as_per_policy
    self._policy.reset_last_action(modified_action)
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
AttributeError: 'FewShotGptPolicy' object has no attribute 'reset_last_action'

I’ve attached the full eval.log for reference: eval.log (n_4_few_llama3_1.txt)

Could you help me understand why this is happening and how to fix it?

Thank you.

[amit9oct]

Thank you for raising this issue. I will look into it.

[amit9oct]

I have significantly changed the workflow to support parallel execution; hopefully, some of it will help alleviate some issues. However, in the future, we will support vLLM for all open-source models. And this will be addressed as part of the vLLM migration.

[amit9oct]

@jogobeny Please retry again with the latest fixes. Now I have added vllm so you no longer need to format etc. It should work by just adding the config. Please let me know, if you have any question.

[jogobeny]

@amit9oct Hi. I have a few notices:

# miniF2F_lean4_few_shot_kimina_no_re_rank.yaml

defaults:
  - env_settings: no_re_rank
  - benchmark: miniF2F_lean4_test
  - eval_settings: n_4_few_kimina
  - prompt_settings: lean4_few_shot
  - override hydra/job_logging: 'disabled'

eval_settings:
 timeout_in_secs: 200
 proof_retries: 4
 temperature: 0.7

• When I run python src/copra/main/run.py --config-name miniF2F_lean4_few_shot_kimina_no_re_rank, it creates .log folder and inside it the datetime folder with {eval, vllm_server, eval_thm_X} logs. After killing the process and rerunning it, it creates a new datetime folder (with {eval, vllm_server}.log), but no eval_thm_X logs, it actually appends new lines to the old eval_thm_X logs in the previous datetime folder.
• Calling this skipping method takes like 5 minutes; this certainly didn't take that long on my previous version (1.1.11).

self.logger.info(f"before skipping {type(self._dynamic_proof_executor)}")
self._dynamic_proof_executor.skip_to_theorem(self.lemma_name)
self.logger.info("after skipping")
lemma_found = True

# 2025-10-24 03:18:56,459 - copra.main.proof_execution.thm_0 - INFO - before skipping <class 'itp_interface.tools.dynamic_lean4_proof_exec.DynamicProofExecutor'>
# 2025-10-24 03:23:52,134 - copra.main.proof_execution.thm_0 - INFO - after skipping

• I also called logging inside the lean4_sync_executor.Lean4SyncExecutor._skip_to_theorem, hoping I could debug why it takes so long, but no logs were printed anywhere.

self.logger.info(f"before parse_thm_name")
thm_namespace, given_theorem_name = parse_thm_name(theorem)
self.logger.info(f"after parse_thm_name")

When I run with the miniF2F-lean4 benchmark, do I have to let COPRA build it, or is it okay to build it manually beforehand via lake build?

Also, have you tried the Kimina model? Because it doesn't follow the instructions on how to respond at all.

Part of the log: eval_thm_0.log

Thanks a lot.

[amit9oct]

@jogobeny
3. The logging happens in previous log folder probably because of checkpoint resuming on rerun. If you delete .log/checkpoints then probably it will start fresh.
4. Have you rerun install-lean-repl and install-itp-interface with correct export LEAN_VERSION (make sure it is the same Lean version as your miniF2F). If yes then I can debug more.
5. You should prebuild the miniF2F repo before running evala.
6. Kimina model is bad at following instructions and doesn't work well with COPRA, and even few shot is pretty hard with it. Will have to probably edit the system prompt and parser to make it work. At that point think it is better to use a formatting model along with Kimina to make any agent use results from Kimina.

[jogobeny]

@amit9oct Yes, I have done a fresh install (removing venv folder, creating new with Python 3.11.5, sourcing, pip install -e .[os-models], exporting LEAN_VERSION to 4.17.0 (I can also try 4.15.0 or newer, if it helps), then install-lean-repl and install-itp-interface. I haven't built miniF2F again since I am still using the same version as before ('before' I mean the previous COPRA commits, where it didn't take that long as mentioned above).

[amit9oct]

@jogobeny
I think there is probably some build error or version mismatch. I was able to run it. I could not reproduce the error you mentioned. Probably just clean .lake file and force pip install the copra package again, and re-run the install commands with correct lean version.

Also, for the open-source model, try openai/gpt-oss-20b, which works the best (I'm going to push the settings file for the same soon). I'm quite surprised by the results. There are some parsing errors; but in general it works quite well with gpt-oss. I have also updated the miniF2F to 4.21 (latest)

[amit9oct]

@jogobeny I have updated to copra repo to 1.1.16 and it should work well with gpt-oss-20b. Please try that. I'm attaching my run log here:

eval.log

As you would notice that there are some successes, there are some failures too (and that is because sometimes gpt-oss doesn't follow the instruction response correctly, or the prompt gets too large). But by far this is the best open source model.

Let me know if any issues still persist. Thank you so much for trying COPRA and reporting issues 👍.

[jogobeny]

@amit9oct I have updated and used gpt-oss-20b, and it doesn't seem to take as long as before. I am not sure where the problem was, but it appears to be resolved now.

By the way, could you provide me with more info about some properties from the config files? E.g., difference between proof_retries and max_steps_per_episode? What about use_hammer, max_history_messages, use_example_retrieval, always_use_useful_theorem_retrieval, and num_goal_per_prompt? Sorry if it is somewhere described, I might have missed it.

PS1 What hardware do you use? How many calls to the model do you make per one theorem within the timeout limit? I assume you have used miniF2F_lean4_easy_to_hard + n_60_dfs_gpt_oss_20b_no_retrieve_no_ex.

PS2 I have noticed that I get so many (almost on every prompt call)

2025-11-03 22:36:36,443 - copra.main.proof_execution.thm_1 - INFO - Incomplete Response messages: 
[{'role': 'assistant', 'content': None, 'finish_reason': 'length'}]

So almost every proof is

2025-11-03 22:33:33,683 - __main__ - INFO - Dumping proof search result:
Proof FAILED (Timeout) for lemma: aime_1983_p2

And sometimes even

2025-11-03 22:39:02,486 - copra.main.proof_execution.thm_1 - ERROR - Max token per prompt must be greater than 0, please decrease max_tokens_per_action
Traceback (most recent call last):
  File "/home/.../copra/src/copra/agent/dfs_policy_prompter.py", line 314, in run_prompt
    prompt_message, prompt_token_count, custom_system_msg, custom_system_msg_cnt = self._get_prompt_message(request, max_token_per_prompt) # Re-generate the prompt message within new token limit
                                                                                   ~~~~~~~~~~~~~~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/.../copra/src/copra/agent/dfs_policy_prompter.py", line 112, in _get_prompt_message
    assert max_tokens_in_prompt > 0, "Max token per prompt must be greater than 0, please decrease max_tokens_per_action"
           ^^^^^^^^^^^^^^^^^^^^^^^^
AssertionError: Max token per prompt must be greater than 0, please decrease max_tokens_per_action

I have used the same config.

If your proof failed, it never is IsTimeout: true:

ProofFile: None
LemmaName: theorem mathd_algebra_388
  (x y z : ℝ)
  (h₀ : 3 * x + 4 * y - 12 * z = 10)
  (h₁ : -2 * x - 3 * y + 9 * z = -4) :
  x = 14  :=
SearchResult: [FAILED]
IsInferenceExhausted: False
IsTimeout: False  # <-------
LongestSuccessPath: -1 
StepsUsed: 3
SearchTimeInSecs: 76.71054267883301
NumberOfBacktracks: -1
PossibleFailedPaths: -1
AdditionalInfo: {'queries': 5, 'attempt_idx': 1, 'total_queries': 5}

But if my proof failed, it is always is_timeout: true.

"data/test/miniF2F-lean4/MiniF2F/Test.lean": {
    "aime_1983_p2": {
        "proof_file": null,
        "proof_found": false,
        "lemma_name": "aime_1983_p2",
        "proof_steps": [],
        "proof_time_in_secs": 600.123838186264,
        "inferences_taken": -1,
        "possible_failed_paths": -1,
        "num_of_backtracks": -1,
        "is_timeout": true,  # <-------
        "is_inference_exhausted": false,
        "longest_success_path": -1,
        "additional_info": {
            "attempt_idx": 0,
            "total_queries": 0
        },
        "language": "LEAN4"
    },

[jogobeny]

@amit9oct I have also tested another model (vllm: Llama 3.1), which worked better for me (but I am still not sure about the timeouts I got from gpt-oss-20b). One thing that confuses me is that I run miniF2F_lean4_test_easy_to_hard with different eval_settings (just changing max_proof_depth and gpt_model_name), and it only tried to prove 18 theorems. I thought that it only attempted to prove the remaining theorems after the gpt-oss-20b was timed out (by my cluster limit, gpt-oss-20b managed to go through only 144 theorems), so I tried to rename the whole .log folder to .log2 and rerun it, but it still proves 18 theorems.

Here are my logs from the Llama 3.1 run:

proof_results.json
data_test_miniF2F-lean4_MiniF2F_Test.lean.txt
benchmark_proof_results.txt
checkpoint_info.json
vllm_server.log
eval.log

[amit9oct]

@jogobeny The logs are interesting. I also see some problems with the have proofs. I'm working on a fix. Let me do that and get back to you in a day or two. With gpt-oss, I was able to do more than 58 theorems (including one induction proof) with pass@1

[amit9oct]

There are some incorrectly accepted proofs, especially because of the have bug. I have changed the itp-interface to work better with have proofs. I have also added a validation mechanism that checks for proof at the end.

[amit9oct]

@jogobeny For the gpt-oss returning None for responses, it seems to be an issue with the vllm: vllm-project/vllm#26480 , something with the flash-attention library, and can change based on which GPU one is using.