Thank you for your comment. We would like to address your concerns as follows:
**Comment:** “Standard practice for self-improvement that leads to lack of novelty.”
**Response:** We go beyond just including the error response. The error message is incorporated with a stateful backtracking search. Statefulness helps avoid repeating similar mistakes and helps prune the search space further. Apart from the error message on the last step, the proof steps that were incorrect for the particular state are shown in the prompt, this reduces the search space dramatically, and triggers backtracking if the LLM chooses to repeat the same incorrect step. The stateful tracking of errors allows us to identify proof steps that eventually fail even while executing immediately which further helps in backtracking early and changing the direction of proof. We have included an example of this in the response to your next comment.
**Comment:** “ReProver uses DPR why BM25 works better in COPRA than ReProver”
**Response:** Retrieval helps get the useful lemmas needed to complete a proof, but the tactic prediction model needs to know the right way of using them. The model may fail to predict the right arguments for the lemma, and the proof search may fail despite the retrieval being correct. The ReProver paper doesn’t perform an ablation on how the quality of the retriever impacts its ability to do proofs. It studies the quality of the DPR vs BM25 retriever in terms of MRR but doesn’t have any ablations where ReProver uses BM25 instead of DPR for proof search, so it is hard to know the impact of the quality of retrieved results on the overall proof search.
For the example in Fig. 6, we had the following prompt just before GPT correctly predicted the next proof step:
```
[GOALS]
[GOAL] 1
n = 70 # The goal we want to prove (or proof state)
[HYPOTHESES] 1 # Assumptions about the goal
[HYPOTHESIS] n : ℕ
[HYPOTHESIS] h₀ : 0 < n
[HYPOTHESIS] h₁ : n.gcd 40 = 10
[HYPOTHESIS] h₂ : n.lcm 40 = 280
[THEOREMS] 1 # The retrieved lemmas from BM25 which can help prove goal
[THEOREM] pnat.gcd_mul_lcm : (n m : ℕ+) : (gcd n m) * (lcm n m) = n * m
[THEOREM] tactic.is_prime_helper : (n : ℕ) (h₁ : 1 < n) (h₂ : nat.min_fac n = n) : nat.prime n
[THEOREM] pnat.lcm_coe : (n m : ℕ+) ....
[INCORRECT STEPS] # Previous mistakes on the given proof state
# Each mistake is listed with the ‘STEP’ keyword.
[STEP] apply nat.eq_of_mul_eq_mul_left (by norm_num : 0 < 40),
rw ←pnat.gcd_mul_lcm,
repeat { rw pnat.gcd_coe },
repeat { rw pnat.lcm_coe },
norm_num,
.... .... ....
[STEP] have h₃ : n * 40 = nat.gcd n 40 * nat.lcm n 40, from pnat.gcd_mul_lcm (⟨n, h₀⟩) ⟨40, dec_trivial⟩,
[STEP] rw nat.gcd_mul_lcm,
[STEP] rw pnat.gcd_mul_lcm at h₁,
[LAST STEP] # Last prediction
have h₃ : n * 40 = 10 * 280, from pnat.gcd_mul_lcm (subtype.mk n h₀) (subtype.mk 40 dec_trivial),
linarith,
[ERROR MESSAGE] # Error message on the last step
Got error in 'have h₃ : n * 40 = 10 * 2...':
error: invalid type ascription, term has type
pnat.gcd ⟨n, h₀⟩ ⟨40, _⟩ * pnat.lcm ⟨n, h₀⟩ ⟨40, _⟩ = ⟨n, h₀⟩ * ⟨40, _⟩ ...
[END]
```
```
# Prediction by GPT-4
[RUN TACTIC]
have h₃ : n * 40 = 10 * 280, by rw [←nat.gcd_mul_lcm n 40, h₁, h₂],
linarith,
[END]
```
It is easy to see that to be able to capitalize the well-retrieved lemmas, the models need to learn how to use those lemmas as well. In our case, BM25 does a very good job of retrieving the best lemmas, however, GPT-4 could not use it correctly in the first couple of tries. It was only because of our **novel stateful backtracking** approach that we could capture the previous mistakes along with the last error message all in the same prompt which dissuaded the GPT-4 from making repeated mistakes and getting to the right prediction. It is also important to note that we could not solve this problem without retrieval, but once we know the list of relevant lemmas, knowing how to use them becomes extremely important. Given this example, it should not be surprising that even when DPR performs better than BM25, COPRA has an edge because it can act as per the rich feedback it gets from the environment. Another interesting idea one can try is to let COPRA create a search query to control the retrieved lemma, which can make a simple BM25 search more effective than DPR.