Bootstrapping Hierarchical Autoregressive Formal Reasoner with Chain-of-Proxy-Autoformalization

We greatly appreciate your detailed reviews, as well as your constructive comments:) We plan to update (U) the following points in the camera-ready version:

• U1. Add a footnote in line 30 "backtracking," to avoid misunderstanding.
• U2. Temporarily rewrite line 297-298 as "demonstrates marginal differences".
• U3. Re-run main experiments and solution pruning experiments twice to report Avg and StDev.
• U4. Visualize solving rate - budget curve Sec. 5.2.
• U5. Add discussion [R4] in Sec. 5.1.
• U6. Replace the claim "consistent scalability" with "scalability".
• U7. Add PutnamBench-Solving results in Table 2.

We sincerely hope them to improve the paper quality and satisfactorily respond to your comments. Our detailed responses (R) are as follows.

W1, Q1. Refining the definition of "backtracking".

R1. Thank you for this suggestion. In this paper, "backtracking" refers to the global proof-search backtracking. We will add a footnote at its first occurrence (line 30) to avoid readers' confusion.

W2, Q2. Improper claim of "no statistically significant difference".

R2. We will temporarily rewrite our claim (line 297-298) as "demonstrates marginal differences" and schedule two repeated runs on solution pruning experiments (Table 4) and main experiments (Table 2. Cycle 1: BFS, WG, AR, H-BFS, H-AR; Cycle 2: H-AR). Due to the limited response time and computing resources, we have not finished all re-runs yet. We promise to update Table 2, Table 4, and line 297-298 in the camera-ready version.

Some of them are finished and show strong statistical significance.

W3, Q3. Explanation of Table 2 (budgets of H-WG and HAR)

R3. We have visualized the solving rate - budget curve of SFT-based experiments in Table 2, which demonstrates that HAR is nearly Pareto-optimal (except for extremely low budget scenarios). Due to the response policy, we provide an interpolated table here. The visualization will be added to Sec. 5.1 in the camera-ready version.

Moreover, we count the budget distribution of 4 types of problems: Both Succeeded (both HAR and H-WG successfully solve the problem), One Succeeded (only one of them successfully solves), and Both Failed (both of them fail to solve). The budget consumption of each type is as below:

As in Appendix F.1, we set the number of expansion attempts as $K=80$ for BFS&AR, and the number of generation attempts as $K=8$ for WG. This is because in the dataset constructed by CoPA, each formal solution contains 9.7 steps on average (line 708).

In "Both Failed": H-WG generates 8.12 steps per attempt, i.e., 64.95 steps per problem. HAR explores at most 80 steps per problem. Therefore, the budget consumption of HAR seems to be higher than H-WG.

W4, Q4. Explanation of the comparison between HAR and H-SA.

R4. H-SA is an augmented version of H-WG. H-WG generates a solution sketch given the initial solution state, and then fills the proof gaps; H-SA generates a solution sketch given both the formal statement (can be viewed as initial solution state + ground-truth formal answer) and the ground-truth informal solution, then fills the proof gaps.

In this view, H-SA sets an (intuitive, not rigorous) upper bound of H-WG. Now that HAR outperforms H-SA, we have a better chance of believing that HAR consistently outperforms H-WG.

We will add the above explanation of the indent behind, including H-SA for comparison in Sec. 5.1.

W5. Explanation of CoPA's scalability in Table 1.

R5. We agree with your insight that scaling up all components of CoPA faces a challenge. The informal dataset is fixed as Numina-1.5. Therefore, as CoPA iterates from formalizing samples and removing successful ones from future iterations, the remaining data will be more and more difficult, until 1) CoPA fails on all of them, or 2) CoPA succeeds on all of them. However, as stated in Appendix B, we need more expert iterations to determine CoPA's "consistent scalability" or "inscalability".

Thank you for this comment. We will remove the claim of "consistent scalability" in the abstract.

W6, Q5. More evaluation.

R6. We have evaluated methods in Table 2 (excluding H-SA due to the absence of ground-truth informal solution) on the PutnamBench-Solving[1,2], which consists of 324 problems from undergraduate-level competitions. The results are as follows.

Although AR / HAR demonstrates superiority over baselines, all methods almost fail on this benchmark because of its out-of-distribution (OOD). As stated in Appendix B. "Limitation", CoPA formalizes Numina-CoT and Numina-1.5, which focuses on "Chinese high school math exercises to US and international mathematics olympiad competition problems". PutnamBench-Solving focuses on undergrad-level competitions and is totally OOD from the training set. The OOD curse in formal reasoning is more challenging since each formal step should be not only semantically but syntactically correct. LLM usually fails to call functions or apply theorems without prior knowledge. As mentioned in line 599-601, we admit current data domain is not enough and encourage future work on this.

Other benchmarks, such as MathOdyssey, ISARSTEP, are not suitable for our evaluation. This project focuses on Lean 4 language, proposing CoPA that translates informal problem-solution pairs into formal ones, and HAR that searches for a formal solution given a formal problem. They are unsuitable for informal math QA (MathOdyssey), filling in a missing intermediate proposition given surrounding proofs (ISARSTEP), natural language inference (FOLIO, ProofWriter, PrOntoQA), and natural language QA (AR-LSAT).

Among them, HAR can be indirectly evaluated on MathOdyssey by 1) autoformalizing the informal problems and answers; 2) conducting D-FPS using HAR. However, this evaluation will be greatly affected by the accuracy of autoformalization. If you feel it necessary to conduct such an evaluation, we will do it ASAP.

L1. Limitation on computing cost

R7. CoPA's data flow (problem autoformalization, solution drafting, gap filling) does not result in a higher-order computational complexity compared with autoformalization-based approaches in theorem proving (statement autoformalization, proof search). Moreover, CoPA differs from [3] by:

1. Problem/Statement Autoformalization: CoPA uses heuristic filtering instead of LLM grader (Appendix C), therefore requires fewer LLM calls while having higher accuracy.
2. Solution/Proof Generation: CoPA uses H-SA, which demonstrates a significantly higher success rate and lower budget cost than WG, as demonstrated in Table 2.

HAR shows superior efficiency compared to baseline methods (R3). Therefore, the theoretical computational resource requirement is not higher than other methods.

The seemingly high compute cost in Sec. J is because this project is conducted on specific hardware platforms that often lack open-source support and in-depth optimization. We believe researchers equipped with A100s, H100s, or even B100s can reproduce the pipeline with much lower resources.

[1] Liu, Qi, et al. "Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving." arXiv preprint arXiv:2505.04528 (2025).

[2] Tsoukalas, George, et al. "Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition." Advances in Neural Information Processing Systems 37 (2024): 11545-11569.

[3] Lin, Yong, et al. "Goedel-prover: A frontier model for open-source automated theorem proving." arXiv preprint arXiv:2502.07640 (2025).

We have now completed three independent runs and will update Tables 2 & 4 with means ± standard deviations.

Table 2 (Main Results) confirms the robustness of our findings:

Table 4 (Solution Pruning) shows a more interesting pattern.

FormalMath500: There is no significant change in solving rates across pruning recursions, and average solution lengths decrease monotonically.

MiniF2F-Solving: For $R=0,1,2$, solving rates remain relatively stable and average solution lengths decrease monotonically. For $R=3, \infty$, solving rates improve and the average solution lengths fluctuate.

We hypothesize this is due to limited context length (as discussed in [R1] to Reviewer pJF9) on complicated problems. Deeper pruning improves reasoning efficiency, preventing models from exceeding the context window (4096 tokens).

Let $S_0, S_\infty$ denote problems solved in $R=0, \infty$ experiments, respectively. The mean solution length of $S_0 \backslash S_\infty$ is $9.82$, while that of $S_\infty \backslash S_0$ is $11.85$. The longest solution in $S_0 \backslash S_\infty$ has 17 steps, while $S_\infty \backslash S_0$ contains three solutions longer than 17 steps (19, 24, 29).

This further supports the benefits of solution pruning: training efficiency (Train Size $\downarrow$) and reasoning efficiency (Avg. Len. $\downarrow$, Solved $\uparrow$).

We will also add the above analysis in Appendix G.

Q5. The current evaluation is minimal. It should include other math benchmarks such as PutnamBench, MathOdyssey, ISARSTEP, etc. It should also be expanded to include other reasoning datasets such as Folio, Proofwriter, PrOntoQA, AR-LSAT, etc. Will this also work with other open weight models or is it targeted only for one model? Some evaluation here would also be desirable.

R9. We appreciate your suggestions and have respectfully done in [R10, R11]. Due to time and resource constraints, some evaluations have not been completed yet. We will continue and update in the camera-ready.

We respectfully note that, for D-FPS, the current evaluation covers all publicly available benchmarks (FormalMath500, MiniF2F-Solving, and PutnamBench-Solving). Sec. 4.2.4 proposes dataset denoising, which expands to improving data quality of informal math reasoning. Further expansions are valuable but lie outside this paper’s focus.

Including informal math benchmarks MathOdyssey.

R10. Expanding to informal benchmarks such as MathOdyssey implies a novel task: end-to-end formal problem-solving (E2E-FPS) (like [1]) that chains (i) autoformalizing a natural language problem, and (ii) generating a formal solution. This has sparked a long discussion among authors.

We provide a pilot study using CoPA Autoformalizer to formalize 288 problems with non-empty labels in MathOdessy, resulting in 269 successfully formalized problems. Models are evaluated with environmental & hyperparameter settings identical to Appendices D & F. We also evaluated AR/HAR with $K_S = 40$ for fair comparison with WG/H-WG $K_W=8$ (WG/H-WG $K_W=16$ takes longer time).

Comparison between AR/HAR ($K_S=40$) and baselines validate AR/HAR's superiority over BFS/H-BFS and WG/H-WG. We will continue $K_W=16$ experiments and incorporate the discussions into a new appendix.

Effectiveness on other open weight models.

R11. Sincere apologies for the late response, as these experiments are expensive and time-consuming. Honestly, we too have wondered whether the impressive effectiveness is a flash in the pan on Qwen series models (as recent pushback on the unreasonable effectiveness of Qwen-based RL[2]).

We have SFTed Phi-4-mini-instruct with identical recipes in the main experiments (Cycle 1 data; Appendices E & K). We also evaluated AR/HAR with $K_S = 40$ for fair comparison with WG/H-WG $K_W=8$ (WG/H-WG $K_W=16$ takes longer time). Early results are shown below.

Results demonstrate similar pattern to Qwen2.5-Math-7B (Table 2; Updated [R2]; [R6]) and align well with our main claims. On all 4 benchmarks, AR ($K_S=40$) demonstrates consistent pareto-optimality over BFS and WG. On FormalMath500, HAR ($K_S=40$) demonstrates similar superiority over H-BFS and H-WG.

We will incorporate all new results and discussion in the camera-ready.

Thank you again for your constructive suggestions, which have made our work more complete :)

[1] Mathesis: Towards Formal Theorem Proving from Natural Languages

[2] Spurious Rewards: Rethinking Training Signals in RLVR

We appreciate the opportunity for further clarification :)

Explanation for Q3 is also not convincing.

R8. Thank you for this insightful comment. We have re-examined the code, data, and experiment results, and discovered a bug in WG's step-counting script: it double-counted every proof step that belonged to a solution step.

After correcting it, we reran WG and H-WG using 16 generation attempts ($K_W=16$). The updated Table 2 is shown below.

Comparisons of (BFS, WG ($K_W=16$), AR) and (H-BFS, H-WG ($K_W=16$), HAR) demonstrate the superiority of AR/HAR.

To understand the remaining budget gap on FormalMath500, we broke down the budget consumption of H-WG ($K_W=8$) and HAR, where "Both Failed" denotes problems that both methods fail to solve, and "Others" denotes problems that any method solves.

For the 209 "Both Failed" problems in FormalMath500, H-WG generates 65 steps (8.1 steps per solution), while HAR exhausted its full budget of 80 steps. On MiniF2F-Solving, H-WG's step count (9.2 steps per solution) is closer to CoPA's dataset average of 9.7 (line 708), so the gap is smaller.

Overall, as demonstrated by the visualizations of solving rate - budget curve [R3], AR/HAR remains more efficient than WG/H-WG when both are given comparable generation limits.

We will include the corrected numbers and the new visualization in the camera-ready. Thank you for this constructive comment, which really helps us to improve this work :)

Thank you for the appreciation of our work and the inspiring suggestions. We sincerely hope the planned paper updates (U) and responses $R$ can help resolve your concerns.

U1. Add test-time scaling experiments and discussions[R1] as a new Appendix.

U2. Polish Sec. 2 and add discussions[R2]

U3. Polish caption of Fig. 1 to reflect discussion[R3]

W1. Impact of backtracking on test-time scaling capabilities.

R1. We set the max step limit $K=320$ to evaluate the test-time scalability of Cycle 2 H-BFS and HAR on the FormalMath500 benchmark. HAR solves 47.88% problems with 64727 search steps, while H-BFS solves 32.54% with 90533 steps. The following table compares the two methods with interpolated solving rates.

H-BFS shows consistent scalability and plateaus after ~70000 steps. The solving rate of HAR rapidly increases and is saturated after ~20000 steps. The saturated solving rate of HAR (47.88%) is significantly higher than that of H-BFS (32.54%).

We find that HAR plateaus because of limited context length. All models are SFTed from Qwen2.5-Math-7B, whose maximum context length is 4096 tokens. Complicated problems require longer CoTs, which require the model to have a larger context length to cover the solution state (more and more conclusions along reasoning) and next-step draft.

HAR experiment encounters 953 times of context length exceeding (experiment restarts upon an exception occurs), while H-BFS encounters 413 times. This corresponds to our observation (line 286) that BFS with accumulated log-prob as value function tends to collapse to breadth-first search.

We will add the above discussions as a new Appendix.

Moreover, we have visualized the solving rate - budget curve of SFT-based experiments, which demonstrates that HAR is nearly pareto-optimal (except extreme low budget scenarios). Due to the response policy, we provide an interpolated table here. The visualization will be added to Sec.5.1 in the camera-ready version.

W2. More comparison and discussion with respect to related work.

R2. For HAR, Sec.5.1. "Baseline Methods" covers most existing methods, to name a few:

• WG: DeepSeekProver-V1, DeepSeekProver-V1.5, DeepSeekProver-V2 (w/o Subgoal Decomposition), Goedel Prover, etc. belong to this category. They directly sample a whole proof given the formal statement.
• H-WG: DeepSeekProver-V2 (w Subgoal Decomposition) belongs to this category. It firstly generates a formal proof sketch containing sorry placeholders, and generates proofs to fill these subgoals.
• BFS: A wide spectrum of works following LeanDojo belongs to this category. They model the construction of proofs as a best-first search on a tree consisting of proof states and proof steps.
• H-BFS: POETRY belongs to this category. It conducts best-first search while allowing the model to generate sorry placeholder and recursively search proofs for subgoals.

HAR differs from existing methods by:

• WG/H-WG: Splits the generation of formal solutions into many smaller rejective sampling steps to avoid error propagation.
• BFS/H-BFS: Removing backtracking for more efficient D-FPS.
• WG/BFS: Decoupling one formal step into an informal-aligned drafting and finer-grained gap filling.

As for CoPA, it differs from [1] by:

1. Problem/Statement Autoformalization: CoPA uses heuristic filtering instead of LLM grader (Appendix C), therefore requires fewer LLM calls while having higher accuracy.
2. Solution/Proof Generation: CoPA uses H-SA, which demonstrates a significantly higher success rate and lower budget cost than WG, as demonstrated in Table 2.

CoPA differs from [2] by:

1. Motivation. D-FPS faces extreme scarcity of formal problem-solution data. Therefore, CoPA targets to construct initial data for model training. Formal Theorem Proving (FTP) has abundant data (LeanWorkbook, Mathlib4), thus STP[2] is initialized by SFT on them (Sec.3.1 in [2]) and targets to generate more high-quality data.
2. Data: CoPA transforms informal problem-solution pairs into formal ones, while STP[2] generates new conjectures and their proofs.
3. Incorporation of informal language. CoPA aims at generating informal-formal aligned problems and solution drafts, thus integrating novel techniques including proxy autoformalization and hierarchical reasoning. STP[2] focuses on FTP and only works on formal language.

Q1. HAR's sampling strategy.

R3. In the current design, for each state, HAR only samples one path. As shown in Fig. 1 and illustrated in line 131-137, given a solution state (i.e., proof state), HAR generates an informal thought, then a formal step draft, executes it, and attempts to fill the sorry gap with a low-level prover. This counts as 1 step in the budget computation. If the execution of gap filling fails, HAR generates another action until the budget is exhausted or the step is successfully executed and filled.

[1] Lin, Yong, et al. "Goedel-prover: A frontier model for open-source automated theorem proving." arXiv preprint arXiv:2502.07640 (2025).

[2] Dong, Kefan, and Tengyu Ma. "Stp: Self-play llm theorem provers with iterative conjecturing and proving." arXiv preprint arXiv:2502.00212 (2025).

Thank you for the positive feedback! We're glad that our comprehensive pipeline and strong empirical gains resonated with you. We'll polish Sec. 2 "Related Works" and incorporate the comparisons in [R2].

Thank you for this insightful review and constructive comments. In summary, we will update the following points in the camera-ready version:

• U1. Add discussions[R2] into Appendix H.
• U2. Visualize solving rate - budget curve Sec. 5.2.
• U3. Polish Sec.2 and add discussions[R3] (line 73)
• U4. Polish Appendix B and add discussions [R4](line 598-599).

Hope them can improve paper quality and help future readers. Our detailed responses (R ) are as follows.

W1. High compute resource requirement.

R1. CoPA's data flow (problem autoformalization, solution drafting, gap filling) does not results in a higher-order computational complexity compared with autoformalization-based approaches in theorem proving (statement autoformalization, proof search). HAR show superior efficiency compared to baseline methods in Table 2. Therefore, the theoretical compute resource requirement is not higher than other methods.

The seemingly high compute cost in Sec. J is because this project is conducted on specific hardware platforms that often lacks open-source support and in-depth optimization. We believe researchers equipped with A100s, H100s, or even B100s can reproduce the pipeline with much lower resource.

As mentioned in NeurIPS Paper Checklist 5. We will open-source our code and model to facilitate future research.

W2. Dataset denoising's negative impact on specific datasets.

R2. Dataset denoising falls behind on SVAMP, OlympiadBench, SAT-Math, MMLU-STEM, Gaokao-Math-QA, and AIME24, which may be due to:

1. Multiple-choice Questions (MCQs) and True-false Problems (TFPs) [SAT-Math, MMLU-STEM, Gaokao-Math-QA]. CoPA focuses on free-response problems (FRP), and therefore rewrites TFPs/MCQs into FRPs in Numina-CoT, Cycle 0, and filters out MCQs in Numina-1.5, Cycle n (line 197). This distribution shift might leave these problems out-of-distribution, thus negatively impacting the SFTed models' performance on benchmarks of MCQs, including SAT-Math, MMLU-STEM, and Gaokao-Math-QA.
2. Simple math word problems (SMWPs). SVAMP focuses on SMWPs about simple arithmetic taught in grades four and lower. Highly automated tactics like norm_num and linarith can directly solve them, thus their formalization might collapse to the "guess-and-verify" pattern, or even only a simple norm_num. Then, the informalization might contain a less detailed CoT compared to the original solution.
3. Out-of-distribution (OOD). STEM problems such as physics, biology, and astronomy are hard to formalize and OOD to Numina-1.5. For problems in geometry, probability, and combinatorics, their difficulty mainly lies in understanding the mathematical abstract and finding the expressions. Once formalized, most of them may collapse to simple arithmetics. This work focuses on problem-solving, therefore, theorem-proving ones are filtered out (line 183). Since MMLU-STEM consists of MCQs of STEM, OlympiadBench contains 25%+ physics problems and 21% about theorem-proving, which are relatively OOD to the SFT dataset and suffer from unstable performance. These limitations are included in Sec.B "Extension to Theorem Proving" and "Data Domain".
4. Benchmark size. AIME24 only contains 30 problems, and the evaluation pipeline (Qwen2.5-Math's official repo) uses greedy decoding with temperature $T=0$, sample number $n=1$. This setting is prone to randomness in small benchmarks like AIME24; one sample can result in 3.3% performance variation.

The above analysis will be added to Appendix H in the camera-ready version.

Q1. Comparing computational efficiency with baselines.

R3.

• CoPA: To the best of our knowledge, this paper is the first to fully open all details about the computational cost. It is not easy to directly compare the computational cost of all components. Here we compare with [1] from a data flow perspective:

  1. Problem/Statement Autoformalization: CoPA uses heuristic filtering instead of LLM grader (Appendix C), therefore requires fewer LLM calls while having higher accuracy.
  2. Solution/Proof Generation: CoPA uses H-SA, which demonstrates a significantly higher success rate and lower budget cost than WG, as demonstrated in Table 2.

  Therefore, CoPA demonstrates higher computational effciency. We will polish Sec.2. "Autoformalization" and integrate the above comparison in it.

• HAR: Table 2 shows that HAR outperforms all baselines. Moreover, we have visualized the solving rate - budget curve of SFT-based experiments, which demonstrates that HAR is nearly pareto-optimal (except extreme low budget scenarios). Due to the response policy, we provide an interpolated table here. The visualization will be added to Sec.5.1 in the camera-ready version.

Q2. CoPA's generalizability to highly challenging or competition-level problems?

R4. Yes. We believe that CoPA can better generalize to competition-level problems. Existing methods directly generates proofs, which may suffer from extreme sparsity on difficult problems. In contrast, CoPA conducts H-SA to utilize priors in natural language ground-truth and align reasoning granularity with informal reasoning.

However, the current formalization system supports problems in disciplines including physics and combinatorics are not satisfactory. Recent progress in PhysLean[2] and CombiBench[3] can help future works to mitigate the gap.

We will polish Appendix B (line 598-599) to integrate this discussion.

[1] Lin, Yong, et al. "Goedel-prover: A frontier model for open-source automated theorem proving." arXiv preprint arXiv:2502.07640 (2025).

[2] PhysLean: Digitalizing Physics in Lean 4

[3] Liu, Junqi, et al. "CombiBench: Benchmarking LLM capability for combinatorial mathematics." arXiv preprint arXiv:2505.03171 (2025).

We greatly appreciate your time and efforts in this detailed and invaluable review :) In the camera-ready version, we will update (U) each point:

• U1. Rewrite Sec. 3 and Appendix A with example in Fig. 1 to explain FTP and D-FPS.
• U2. Add discussions in R2 into Appendix H.
• U3. Add discussions in R3 into Appendix L.
• U4. Add more explanations in line 728.
• U5. Add discussions in R5 into Appendix I.
• U6. Update Table 2 with 3-run Avg and StDev.
• U7. Polish Sec. 2 "Formal Reasoning".

Hopefully, these updates can help improve the paper and satisfactorily respond to your comments. Our detailed responses (R) are as follows.

W1.1. Add intuitive explanations or examples for D-FPS.

R1. We will further explain the mathematical notations for D-FPS and FTP in Sec. 3 and Appendix A (line 561-567) using the Fig. 1 example. Appendix A will be renamed as "More Discussions on D-FPS".

W1.2, Q5. Add more discussions of dataset denoising's negative impact on specific datasets.

R2. Compared with Direct SFT, Denoised SFT falls behind on SVAMP, OlympiadBench, SAT-Math, MMLU-STEM, Gaokao-Math-QA, and AIME24. The causes might be:

1. Multiple-choice Questions (MCQs) and True-false Problems (TFPs). CoPA focuses on free-response problems (FRP), and therefore rewrites TFPs/MCQs into FRPs in Numina-CoT, Cycle 0, and filters out MCQs in Numina-1.5, Cycle n (line 197). This distribution shift might leave these problems out-of-distribution, thus negatively impacting the SFTed models' performance on benchmarks of MCQs, including SAT-Math, MMLU-STEM, and Gaokao-Math-QA.
2. Simple math word problems (SMWPs). SVAMP focuses on SMWPs about simple arithmetic taught in grades four and lower[1]. Highly automated tactics like norm_num and linarith can directly solve them, thus their formalization might collapse to the "guess-and-verify" pattern, or even only a simple norm_num. Then, the informalization might contain a less detailed CoT compared to the original solution.
3. Out-of-distribution (OOD). STEM problems, such as physics, biology, and astronomy, are hard to formalize and OOD to Numina-1.5. For problems in geometry, probability, and combinatorics, their difficulty mainly lies in understanding the mathematical abstract and finding the expressions. Once formalized, most of them may collapse to simple arithmetic. This work focuses on problem-solving, therefore, theorem-proving ones are filtered out (line 183). Since MMLU-STEM consists of MCQs of STEM, OlympiadBench contains 25%+ physics problems and 21% about theorem-proving, which are relatively OOD to the SFT dataset and suffer from unstable performance. These limitations are included in Sec. B "Extension to Theorem Proving" and "Data Domain".
4. Benchmark Size. AIME24 only contains 30 problems, and the evaluation pipeline (Qwen2.5-Math's official repo) uses greedy decoding with temperature $T=0$, sample number $n=1$. This setting is prone to randomness in small benchmarks like AIME24; one sample can result in 3.3% performance variation.

W2.1, Q3. Discussions about potential negative implications.

R3. Thank you for this kind suggestion. We have explored more potential risks and mitigation strategies and will add them into Appenix L.

1. Over-reliance on formal verification. The "verified" refers to "theoretically verified". However, the implementation of formal verifiers themselves is the heel of Achilles. Current expert systems are fragile to misimplementation, e.g. Alphageometry contains wrong rules[2], code contributions to Mathlib are not allowed to use native_decide due to its trust on the Lean compiler. Therefore, merely depend on automated reasoning is not sufficient. Future works may mitigate this by cross-check the same reasoning process with two independent proof assistants (e.g. Lean and Coq).
2. Over-reliance on automated reasoning. Heavy use of automated reasoners offload users' covnitivity. Formal proofs / solutions are not easy to understand. If they accept results without understanding the idea behind, their own intuition and intelligence may degenerate. Future works about faithful informalization (translating formal reasoning results into natural language) can help alleviate this.

W2.2 Solution pruning degrade CoT for simple problems.

R4. We acknowledge this comment and will add a suggestion in line 728 that encourage readers to apply solution pruning on difficult problems.

Q1. Deeper analysis of failure modes.

R5. We have analyzed more examples and the distribution of our datasets, the results are as follows (and will be added into Appendix I).

• Extraneous Answer: Only 0.65% of the formalized data have multiple valid answers, and only 0.09% have more than two. Formal solutions are autoformalized from informal solutions, which are merely solutions without original thinking process, as Gauss said, "no self-respecting architect leaves the scaffolding in place after completing the building". Therefore, merely SFT on such data might be insufficient for the model to learn to filter out extraneous answers. After bootstrapping data with CoPA, future works with reinforcement learning can help mitigate this issue.
• Unsimplified Answer: 14% of the problems have answers longer than 10 characters, 6% of them have answers longer than 20 characters, and the longest answer contains 385 characters. Many of these long answers are polynomials (e.g. Polynomial.C 1 * Polynomial.X^10 + ...) and complex trigonometric functions (e.g. Real.sqrt ((10 * Real.cos (Real.pi / 3) ...). Therefore, the model falls short on learning the definition of "simplified". Future works may train a preference model based on existing problem-answer pairs to filter out unsimplified submissions by the reasoning model.
• Irrelevant Answer: We have carefully examined the training data and find that no final answer corresponds to this failure mode. Therefore, this failure might be occasional. Future works can also use a preference model to filter out these irrelevant submissions.

Q2. Statistical evidence to support the reliability of solving rates.

R6. We will re-run main experiments (Table 2. Cycle 1: BFS, WG, AR, H-BFS, H-AR; Cycle 2: H-AR) for two more times, and report the average and standard deviation of total 3-runs. Due to the limited response time and compute resource, we have not finished all re-runs yet. We promise to update Table 2 in the camera-ready version. However, preliminary results below show strong statistical significance.

Q4. Comparison between HAR and existing methods.

R7. To respectively clarify, Sec.5.1. "Baseline Methods" covers most existing methods, to name a few:

• WG: DeepSeekProver-V1[3], DeepSeekProver-V1.5[4], DeepSeekProver-V2[5] (w/o Subgoal Decomposition), Goedel Prover[6], etc. belongs to this category. They directly sample a whole proof given the formal statement.
• H-WG: DeepSeekProver-V2[5] (Subgoal Decomposition) belongs to this category. It firstly generates a formal proof sketch containing sorry placeholders, and generates proofs to fill these subgoals.
• BFS: A wide spectrum of works following LeanDojo belongs to this category. They model the construction of proofs as a best-first search on a tree consisting of proof states and proof steps.
• H-BFS: POETRY belongs to this category. It conducts best-first search while allowing the model to generate sorry placeholder and recursively search proofs for subgoals.

HAR differs from existing methods by

• WG/H-WG: Splits the generation of formal solutions into many smaller rejective sampling steps to avoid error propagation.
• BFS/H-BFS: Removing backtracking for more efficient D-FPS.
• WG/BFS: Decoupling one formal step into an informal-aligned drafting and finer-grained gap filling.

We will polish Sec.2 "Formal Reasoning" to differentiate HAR with existing methods.

[1] Patel, Arkil, Satwik Bhattamishra, and Navin Goyal. "Are NLP models really able to solve simple math word problems?." arXiv preprint arXiv:2103.07191 (2021).

[2] Lean Zulip Chat. "AlphaGeometry doesn't have a secure foundation"

[3] Xin, Huajian, et al. "Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data." arXiv preprint arXiv:2405.14333 (2024).

[4] Xin, Huajian, et al. "Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search." arXiv preprint arXiv:2408.08152 (2024).

[5] Ren, Z. Z., et al. "Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition." arXiv preprint arXiv:2504.21801 (2025).

[6] Lin, Yong, et al. "Goedel-prover: A frontier model for open-source automated theorem proving." arXiv preprint arXiv:2502.07640 (2025).

We have now completed three independent runs and will update Table 2 (and Table 4 for [R2] to Reviewer ZCQb) with the mean and standard deviation across runs. The results confirm the robustness of our findings:

We appreciate the opportunity to strengthen the statistical grounding of our results :)