HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving

ArXiv: 2412.20735

🎯 Pitch

A 7B model surpasses GPT-4o and all prior systems on miniF2F by predicting how many steps remain—not just which move to make—using a novel distance critic trained on coarse-to-fine tuple targets like (2,3,6). This single critic, combined with iterative data scaling from autoformalized problems, unlocks 68.4% accuracy on the benchmark with far less search than prior methods.

1. Executive Summary

This paper introduces HUNYUANPROVER, a 7B-parameter LLM fine-tuned from HUNYUAN 7B for interactive automatic theorem proving in LEAN4, built around a scalable data synthesis framework that generates over 20 million tactic-level training examples through iterative autoformalization and rejection finetuning from open-source and internal math corpora. At inference, the system deploys guided tree search algorithms — best-first search and an adapted ηMCTS — steered by learned critic models that include a policy confidence baseline, a process reward model predicting state-level provability, and a novel distance critic that estimates remaining proof steps through a coarse-to-fine balanced binary tree representation (predicting hierarchical ranges as tuples like (2,3,6) rather than raw integers to mitigate data sparsity). On the miniF2F-test benchmark, HUNYUANPROVER with distance-critic-guided best-first search achieves 68.4% accuracy, surpassing the prior state-of-the-art by 2.5 points while using a smaller search budget. Ablation results demonstrate that critic guidance — particularly the distance critic — and iterative data curation (removing easy statements after v12 to push performance further) are the primary drivers of improvement, establishing that automated theorem proving with modest-scale models benefits substantially from learned search heuristics but that data quality selection becomes critical once sufficient scale is reached.

2. Context and Motivation

The Core Problem: Theorem Proving Is Data-Sparse and Search-Intensive

The fundamental challenge this paper addresses is how to build an effective automated theorem prover using a relatively modest 7B-parameter language model when the available training data for formal proof systems is severely limited and the search space for Olympiad-level proofs is astronomically large. This is not simply a matter of training a bigger model on more data — the paper confronts two intertwined bottlenecks that are structural to formal theorem proving itself.

Bottleneck 1: Data scarcity in formal proof systems. As the paper states bluntly in Section 2:

"One major bottleneck for automated theorem proving is the lack of training data. For example, as one of the largest open-source LEAN4 datasets, mathlib4 (Moura & Ullrich, 2021) only contains around 50k theorems (with tactics) for training. This is far from sufficient to train a stronger prover given the difficulty of automatic theorem proving."

Fifty thousand examples is minuscule by modern LLM pretraining standards. For context, models like DeepSeek-Prover and InternLM2.5-StepProver (the prior SOTA systems this paper competes against) rely on substantially more training data. The paper cites no equivalent large-scale formal proof corpus — this is a genuine structural gap: formal mathematics in systems like LEAN is time-consuming to produce, requiring expertise in both mathematics and the formal system's syntax. Human-verified formal proofs in mathlib4 represent thousands of person-hours of labor. Scaling via purely human annotation is fundamentally infeasible for reaching the data volumes (tens of millions of examples) that modern LLMs need.

Bottleneck 2: Massive search space for complex proofs. Even with a capable prover model, automatically finding proofs for Olympiad-level statements requires navigating an enormous combinatorial space of possible tactic sequences. The paper characterizes the challenge as one where:

"language models still encounter substantial challenges in formal theorem proving (e.g., using LEAN or Isabelle) probably due to the massive search space of Olympiad-level theorem proving and limited data in such scenario."

A single incorrect tactic choice at any step can lead to a dead end, and the branching factor — the number of valid tactics the model could apply at a given state — is large. Exhaustive search is impossible for non-trivial theorems. Yet the prior generation of theorem provers (as evidenced by the baselines in Table 1) relied heavily on brute-force sampling: generating many candidate proofs and hoping one succeeds, with only minimal learned guidance to direct the search.

Why This Problem Matters

The significance of automated theorem proving extends well beyond benchmarks. The paper situates itself within a broader vision where LLMs serve as mathematical reasoning assistants capable of producing formally verified proofs — proofs that are machine-checkable and guaranteed correct. This has several concrete implications:

Verification and correctness guarantees. Unlike natural language mathematical reasoning where models can produce plausible-sounding but incorrect arguments, LEAN proofs are mechanically verified. A successful LEAN proof is a certificate of absolute correctness. For applications in formal verification of software, hardware, or cryptographic protocols — where errors have catastrophic consequences — automated theorem proving offers a path toward trustworthy AI reasoning. The paper's emphasis on LEAN4 specifically (rather than informal mathematical reasoning) signals an ambition toward verified, not merely plausible, outputs.

Scaling formal mathematics. mathlib4, with its 50K theorems, represents only a fraction of known mathematics. Automating the formalization and proof of mathematical results could dramatically accelerate the growth of formal mathematical libraries, creating a flywheel effect: more formalized mathematics enables better prover training, which enables faster formalization. The paper's autoformalization pipeline (converting natural language math problems to LEAN statements) directly targets this bottleneck, treating the vast corpus of informal mathematics as raw material for formal system growth.

Olympiad-level reasoning as an AI capability milestone. Proving IMO problems (the paper highlights solving IMO 1960 P2, 1962 P2, 1964 P2, and 1983 P6 in miniF2F-test) represents a recognizable threshold of mathematical reasoning capability. IMO problems are designed to require creative insight, not just routine calculation — they test whether an AI system can perform the kind of non-obvious deductive leaps that characterize human mathematical expertise. Achieving 68.4% on miniF2F-test (a benchmark containing such problems) demonstrates that LLM-based theorem provers are crossing into genuinely difficult mathematical territory.

Where Prior Approaches Fall Short

The paper does not provide an extensive taxonomy of prior work, but it positions itself against two implicit approaches and several explicit competing systems, each with identifiable limitations.

The whole-proof generation paradigm. Systems like DeepSeek-Prover-V1.5 (Xin et al., 2024b) generate entire proofs in one shot rather than interactively. The paper categorizes these as "Whole-Proof Generation Methods" in Table 1. The limitation is straightforward: generating a complete, correct proof for a complex theorem in a single forward pass is extremely difficult because the model has no opportunity to receive feedback from the LEAN environment during generation. If the proof contains an error at step 3, the model cannot course-correct — the entire proof is discarded. DeepSeek-Prover-V1.5 compensates with massive search budgets (16 × 6400 and 32 × 6400 in Table 1), essentially brute-forcing the problem through enormous parallel sampling. This is computationally expensive and scales poorly to harder problems.

Interactive proving without learned search guidance. The interactive step-proving approach — where the model generates one tactic at a time, receives LEAN feedback, and continues — is shared by Lean-STaR (Lin et al., 2024) and InternLM2.5-StepProver (Wu et al., 2024). However, these systems differ in how they allocate the search budget. Lean-STaR, with its "BFS+CG" (best-first search with critic guidance), achieves only 46.3% on miniF2F-test (Table 1) — well below the 65.9% of InternLM2.5-StepProver+BFS+CG. The paper does not analyze why Lean-STaR underperforms, but the large gap (19.6 points) suggests that critic model quality, training data scale, or search algorithm implementation details matter enormously. InternLM2.5-StepProver achieves strong results (65.9%) but uses a massive search budget: $256 \times 32 \times 600$ — interpreting the Table 1 notation, this means 256 passes, 32 beams, and 600 iterations. This is roughly 4.9 million tactic evaluations per theorem, a cost that limits practical deployment.

The gap in critic model design. The paper identifies a specific shortcoming in how prior systems guide search. Most prior work either uses no critic (relying on random sampling or simple policy confidence as in early versions of the paper's own system) or uses relatively simple critic models. The paper's introduction of the distance critic — predicting the number of remaining proof steps in a coarse-to-fine binary tree representation — represents a novel critic architecture that the paper argues is specifically designed to address data sparsity in critic training. Prior PRM-based approaches (e.g., Wang et al., 2024c, which the paper cites as inspiration) use binary success/failure labels to train value functions. These work, but the distance critic provides richer signal: two states can both be "successful eventually" yet differ substantially in how many steps remain, and this information can help the search algorithm prioritize more promising branches.

The data scaling gap. While DeepSeek-Prover and InternLM2.5-StepProver both use synthetic data generation, the paper argues that the scale matters critically and that prior systems may not have pushed data scaling far enough. Section 2 describes generating over 20 million tactic-level training examples through more than 10 rounds of iterative improvement — expanding the initial mathlib4 dataset (50K theorems) by roughly 400×. This is not merely "more data"; the iterative framework is designed so that each round generates proofs for progressively harder statements, creating a curriculum where the model bootstraps its own capability.

How This Paper Positions Itself

The paper does not claim to invent interactive theorem proving, synthetic data generation, or tree search with critic guidance. Rather, it positions itself as systematically engineering the combination of data scaling and critic-guided search to achieve SOTA with a modest model size. The positioning has several key aspects:

Data scaling as a first-class design choice, not an afterthought. The iterative tactic generation pipeline (Section 2.2) is not described as a one-time preprocessing step but as the central mechanism enabling the prover's performance. The paper explicitly frames the problem as one of insufficient data and then constructs a self-improving data flywheel: the autoformalizer converts 30M internal math problems to LEAN statements, the prover attempts to solve them via tree search, successful trajectories become new training data for the next prover iteration, and unsolved statements remain in the pool for future iterations. This is analogous in spirit to expert iteration / STaR approaches (Zelikman et al., 2022) but scaled to the formal theorem proving domain with the specific challenge of autoformalization.

Critic models as the key differentiator in search. While best-first search and MCTS are standard algorithms, the paper invests significant design effort in the critic models that guide them. The three-tier critic hierarchy — policy confidence (cold start) → process reward model (success prediction) → distance critic (remaining steps) — represents a progression of increasingly informative guidance signals. The distance critic, with its balanced binary tree representation, is positioned as the paper's primary methodological innovation at inference time. The hierarchical representation (Figure 2) is motivated by a specific problem: predicting raw integer distances suffers from data sparsity (each possible distance value gets few training examples), while the coarse-to-fine tree allows the model to share statistical strength across similar distances (e.g., states 5 steps and 6 steps from completion share the path prefix root → 2/2 → 3/4).

Comparison to prior SOTA as evidence of efficiency, not just accuracy. Table 1 is carefully constructed to highlight not just that HUNYUANPROVER achieves 68.4% (vs. 65.9% for InternLM2.5-StepProver) but that it does so with a smaller search budget: $600 \times 8 \times 400$ versus $256 \times 32 \times 600$. While the cost metrics are not directly comparable across different notation conventions, the paper's framing emphasizes that critic quality can substitute for brute-force search breadth. This is a practical argument: better search guidance means you can spend less compute per proof, which matters for real deployment.

Data curation emerges as an unexpected finding. The paper notes that after iteration v12, when data volume had reached approximately 4.25B tokens, further scaling produced only minor improvements. The key insight from Figure 3 is that removing easy training data from early iterations then unlocked additional gains (v14 and v16). This is described as a finding rather than an a priori design choice:

"We can see the performance boost is achieved by removing these easy data. This highlights the importance of data selection in the iterative improving process."

This positions the paper as contributing not just a method but an empirical finding about the data scaling behavior of iterative prover training: there is a point at which data quality and difficulty composition matter more than raw volume.

Acknowledged but deferred: combining PRM search with revisions, MCTS ablation. The paper is careful to note several limitations that position it as an intermediate step rather than a final system. The MCTS results (Table 2) are only evaluated in combination with PRM, not with the distance critic:

"Due to limitation on time and computation resources, we leave separately examining the effectiveness of MCTS and PRM in future work."

This suggests the paper views MCTS as promising but underexplored in the current experiments — the gains over BFS are modest (62.29% vs. 61.07% at v12, 66.39% vs. 65.57% at v14), and the paper does not claim to have optimized MCTS for this domain.

The Broader Research Context

The paper exists at the intersection of several research threads that it largely takes as given rather than extensively recounting:

• LLMs for formal mathematics (DeepSeek-Prover, Lean-STaR, InternLM2.5-StepProver): the paper treats these as direct competitors, with Table 1 serving as the primary positioning device.
• Process reward models for search guidance (Math-Shepherd, Wang et al., 2024c): the paper adapts the binary-labeled PRM approach from this line of work but extends it with the distance critic architecture.
• Monte Carlo Tree Search for LLM reasoning (ηMCTS from Tian et al., 2024): the paper adopts ηMCTS with minimal modification (removing simulation, increasing the per-node sampling budget to K tactics), treating it as a known algorithm rather than a contribution.
• Expert iteration and self-improvement (RFT, STaR): the iterative data generation framework follows the pattern of using the model's own successful outputs as training data for the next iteration, a now-standard technique that the paper scales to the formal theorem proving domain.

The paper's contribution is best understood not as introducing fundamentally new algorithms but as demonstrating that engineering the right combination of data scaling strategy, critic architecture, and search algorithm yields SOTA results with a 7B model — and that within this combination, the distance critic and data curation are the specific innovations that provide the edge over prior work.

3. Technical Approach

3.1 Reader Orientation

HUNYUANPROVER is a 7B-parameter language model fine-tuned to act as an interactive theorem prover in LEAN4 — it takes a formal mathematical statement and a current proof state as input and outputs the next tactic (proof step) to apply. The system solves the twin problems of data scarcity (too few formal proof examples exist to train a capable prover) and search complexity (finding a valid proof through the enormous space of possible tactic sequences) by combining an iterative self-improving data generation pipeline with guided tree search algorithms that use learned critic models to decide which proof branches are most promising.

3.2 Big-Picture Architecture (Diagram in Words)

The system has six major components arranged in two phases — offline data generation and online proof search:

1. Autoformalization Model — translates natural language math problems into LEAN4 formal statements, producing a pool of 20M statements to prove.
2. Iterative Prover Training Loop — an expert-iteration cycle: a prover model attempts to prove statements from the pool using tree search; successful proof trajectories become new training data; the prover is retrained via rejection finetuning (RFT) on accumulated trajectories; the cycle repeats for 10+ iterations, gradually solving harder statements.
3. Policy Model (the Prover) — a HUNYUAN 7B model fine-tuned on the accumulated tactic data that, given a statement and current proof state, outputs a next tactic to apply.
4. Critic Models — three types of learned guidance functions. Policy Confidence (PC) averages token-level log probabilities of the policy model to score states; Process Reward Model (PRM) predicts whether a given proof state can eventually lead to a successful proof; Distance Critic (DC) predicts the estimated number of remaining proof steps using a coarse-to-fine balanced binary tree representation.
5. Tree Search Algorithms — Best-First Search (BFS) iteratively selects the highest-scoring unexplored node according to the critic, expands it by sampling K tactics from the policy, and feeds valid new tactics to LEAN4 for execution. ηMCTS modifies BFS by allowing nodes to be revisited with a dynamic expansion budget based on importance scores and balancing exploration vs. exploitation via Upper Confidence Bound (UCB) scores.
6. LEAN4 Environment (LeanDojo) — the verification engine that executes each tactic against the current proof state and returns the resulting new state or an error if the tactic is invalid.

Information flow at training time: Natural language math problems → autoformalization model → LEAN statements pool → BFS with current prover + critic → correct proof trajectories → merge into training dataset → RFT on prover → repeat.

Information flow at inference time: Formal statement → BFS or MCTS with policy model proposing tactics and critic model scoring states → LEAN4 execution feedback → repeat until proof is found or budget exhausted.

3.3 Roadmap for the Deep Dive

• First, the autoformalization data pipeline (Section 2.1), because the LEAN statement pool is the raw material from which all prover training data ultimately derives and the scale of this pool (30M problems → 20M statements) determines the entire data scaling story.
• Second, the iterative prover training framework (Section 2.2), because this is the engine that converts the statement pool into tactic-level training data through repeated cycles of attempted proofs and retraining — understanding this self-improvement loop is essential to understanding how the system reaches 20M+ training examples.
• Third, the policy model and its fine-tuning configuration, including the specific hyperparameters and training protocol, because this is the core model whose capabilities are being iteratively improved.
• Fourth, the tree search algorithms (BFS and ηMCTS) as abstract frameworks, covering the selection, expansion, and (for MCTS) backpropagation mechanics, because the critic models are plugged into these algorithms and their effectiveness depends on understanding how the critic scores are used.
• Fifth, the critic models in increasing order of sophistication: Policy Confidence → Process Reward Model → Distance Critic. This order makes sense because PC requires no separate training, PRM adds learned value prediction, and DC further adds fine-grained distance estimation with the hierarchical binary tree representation. Each critic addresses a limitation of the previous one.

3.4 Detailed, Sentence-Based Technical Breakdown

This is fundamentally a systems engineering paper that achieves SOTA through the careful combination of three existing techniques (autoformalization, expert iteration, critic-guided tree search) with two key innovations: the scale of the iterative data generation (20M+ tactic examples) and the distance critic architecture that provides richer search guidance than prior PRM-based approaches.

Autoformalization: Converting Natural Language Math to LEAN Statements

The autoformalization pipeline (Section 2.1) solves a specific bottleneck: while mathlib4 contains only around 50K theorems in LEAN4 format, there exist massive corpora of natural language math problems (the paper cites over 30 million internal problems plus the open-source NuminaMath CoT dataset). The autoformalizer bridges this gap by translating natural language mathematics into formal LEAN4 statements, creating a large pool of statements that the prover can then attempt to prove.

Initial training data for the autoformalizer. The paper starts with 130K high-quality natural-language-to-LEAN-statement pairs drawn from two sources: 50K from Lean Workbook (Ying et al., 2024) and 80K from MMA (Jiang et al., 2024). These are aligned pairs — a natural language problem statement on one side, its LEAN4 formalization on the other — that provide supervised training signal for the autoformalization model.

Data augmentation through translation. To double the size of this initial training set, the paper translates the natural language portion of all 130K pairs into Chinese, producing an additional 130K Chinese-to-LEAN pairs. This is a pragmatic data augmentation decision: Chinese and English express the same mathematical content with different surface forms, so the model learns to be language-agnostic in its formalization — it can produce LEAN statements from both English and Chinese input. The combined 260K pairs are used to train the initial autoformalization model.

At-scale formalization. The trained autoformalization model is then applied to 30 million internal math problems in natural language. For each natural language problem, the model samples 8 outputs using different temperature settings (the specific temperatures are not stated in the paper, but the sampling strategy mirrors the diversity-seeking approach used throughout the system). This produces up to 240 million candidate LEAN statements.

Filtering to valid statements. The paper applies filtering criteria to eliminate candidates that are not well-formed LEAN. The filtered set $D_q$ contains approximately 20 million LEAN statements — a reduction from 240M candidates to 20M valid statements, meaning roughly 8.3% of generated candidates pass the filters. The filtering criteria are described as eliminating statements that "do not conform with LEAN grammar or do not satisfy other rules adopted by previous practices (Ying et al., 2024)" — the specific rules are not enumerated but come from prior work on Lean Workbook.

What the autoformalizer does NOT do. Critically, the autoformalizer only produces statements (theorems to be proved), not proofs (the tactic sequences that establish those theorems). The statement $D_q$ is therefore a pool of unproven LEAN formal statements — the raw material that the iterative prover training loop (Section 2.2) will attempt to solve. The autoformalizer's job is to convert informal mathematical problems into formal conjectures; the prover's job is to find proofs for those conjectures (or determine that they are false, though the paper focuses on true statements).

Design rationale. Using autoformalization rather than purely human-written formal statements is economically necessary — generating 20M formal statements via human experts would be prohibitively expensive and time-consuming. The quality-control mechanism (grammar checking and rule-based filtering) provides a lightweight correctness guarantee: the statements are syntactically valid LEAN4, even if their semantic correctness (whether they faithfully capture the original natural language problem) is not guaranteed. The paper implicitly relies on the fact that a statement's LEAN proof is only possible if the statement is correctly formalized, so the prover's success on a statement provides a form of validation for the autoformalizer's output.

Iterative Prover Training: Self-Improving Data Generation

The iterative training framework (Section 2.2) is the mechanism that converts the pool of unproven LEAN statements $D_q$ into tactic-level training data for the prover. The core insight is that the prover can generate its own training data by attempting to prove statements and collecting the successful trajectories, with each round of retraining enabling the prover to solve harder statements in the next round.

Initial prover (π₀). The base prover $\pi_0$ is trained on publicly available data, including mathlib4 (the ~50K formal proofs with tactics). This provides the prover with fundamental LEAN tactical knowledge — how to apply tactics like rw, induction, nlinarith, etc. — but at a relatively small scale. The paper does not detail the exact training procedure for $\pi_0$, but it serves as the bootstrap model for the iterative loop.

The iteration equation. At each iteration $t$, the system attempts to prove all previously unsolved statements using the current prover $\pi_{t-1}$ guided by best-first search. The training data for iteration $t$ accumulates all successful trajectories found so far:

$D_t = \{(q, \tau) \mid q \in D_q \setminus D_{t-1}, \tau \sim \text{BFS}(q), \tau \neq \text{null}\} \cup D_{t-1}$

where $D_q$ is the pool of autoformalized statements, $D_{t-1}$ is the set of statements already proved in previous iterations, $\tau \sim \text{BFS}(q)$ means running best-first search with prover $\pi_{t-1}$ on statement $q$, and $\tau \neq \text{null}$ indicates that a valid proof was found.

What this equation computes operationally: For each unproven statement $q$, the system runs BFS with the current prover. If BFS finds a valid proof $\tau$ (a sequence of tactics that leads to a verified proof in LEAN), the pair $(q, \tau)$ is added to the training set. Statements that remain unsolved carry forward to the next iteration where a stronger prover will attempt them. The training set $D_t$ grows monotonically — previously discovered proofs are retained, and new proofs are appended.

Why this form: The equation captures expert iteration (also called rejection finetuning or STaR): the model generates its own training data by solving problems, and only successful attempts are used for training. This is a form of curriculum learning because easier statements tend to be solved in early iterations, leaving harder statements for later iterations when the prover is stronger. The monotonic growth of $D_t$ ensures the prover never forgets how to solve previously mastered problems.

Iteration mechanics. The paper reports "more than 10 rounds of iteration" and "more than 20 million tactic-level data is obtained" cumulatively. At each iteration, the prover $\pi_{t-1}$ is used with BFS guided by the critic from the previous iteration to attempt proofs on all unsolved statements. The specific number of iterations is not given, but the version numbering in Figure 3 ("v2" through "v16") suggests approximately 16 iterations, with version numbers approximately corresponding to iteration count.

Post-iteration data curation (the v12 → v14/v16 transition). A critical design choice emerges after iteration v12, when the total training data reaches roughly 4.25B tokens. The paper observes that further data scaling produces only minor improvements, and then deliberately removes easy training data from early iterations (before v8). Figure 3 shows that this data removal — rather than harming performance — produces a noticeable boost (from roughly 62% at v12 to roughly 64.75% at v16 with BFS+PC, and 68.44% with BFS+DC). The paper states:

"Most of the removed training data are relatively easy statements. We can see the performance boost is achieved by removing these easy data. This highlights the importance of data selection in the iterative improving process."

This is an empirical finding rather than an a priori design principle: once sufficient data volume is reached, the difficulty distribution of the training data matters more than raw quantity. Removing easy examples prevents the model from overfitting to simple proof patterns and forces it to focus on the harder problems that are more representative of the benchmark distribution.

Diversity enhancement. The paper introduces two additional methods to increase training data diversity within the iterative framework. First, they "design rules to convert the last state of an unfinished proving trajectory into a new statement" — when BFS exhausts its budget without finding a proof, the final proof state (with its accumulated hypotheses and partial progress) is reformulated as a new LEAN statement. The prover can then attempt to prove this intermediate state as a standalone theorem, potentially generating training data for proving complex subgoals. Second, they "collect data from proving more challenging statements, including those Olympiad-level algebraic inequalities (Wei et al., 2024) and lean workbook (Ying et al., 2024)." This targets the hardest end of the difficulty spectrum, ensuring the training distribution includes problems comparable to the miniF2F benchmark.

Rejection Finetuning (RFT). The actual training process at each iteration uses RFT: the prover $\pi_{t-1}$ is fine-tuned on the accumulated successful trajectories $D_t$. RFT is standard supervised fine-tuning on the model's own successful outputs — the model learns to reproduce the proof steps that led to success, while unsuccessful attempts (rejected by the LEAN environment) are discarded. This is distinct from reinforcement learning approaches (like the RL+MCTS used by DeepSeek-Prover-V1.5 in Table 1) that can learn from negative feedback. The paper's choice of RFT reflects a pragmatic tradeoff: RFT is simpler to implement and more stable than RL, and the iterative structure (each round generating new positive examples from a stronger policy) provides a form of exploration that partially compensates for the lack of negative-signal learning.

Policy Model: Architecture and Fine-Tuning Configuration

The policy model is the central theorem-proving engine — a 7B-parameter HUNYUAN language model fine-tuned to map (statement, proof state) pairs to the next tactic. The paper provides specific hyperparameters for this fine-tuning process.

Base model. The prover starts from the HUNYUAN 7B model. The paper does not detail the base model's pretraining corpus or architecture, treating it as a known quantity. The choice of 7B parameters places HUNYUANPROVER in the same model-size class as its competitors: DeepSeek-Prover-V1.5 (7B) and InternLM2.5-StepProver (7B) — all three leading systems use comparably sized models, making their performance differences attributable to training data, search strategy, and critic design rather than raw model capacity.

Fine-tuning data format. The training data consists of (statement, proof state, next tactic) triples extracted from successful proof trajectories. The prompts for the policy model are structured to include the current tactic state (goals, hypotheses, the statement being proved) followed by a request for the next tactic. An example prompt is provided in Appendix B (the "Policy Prompt" section):

Given the Lean 4 tactic state, suggest a next tactic.
Tactic state:
a b : ℝ
hab : a > 0 ∧ b > 0
h1 : 0 < Real.log 2
h : Real.log (a * b) = Real.log (2 ^ 6)
⊢ a + b ≥ 16
Next tactic:

The model is trained to predict the "Next tactic:" portion — in this example, rw [Real.log_mul] at h — conditioning on the statement context and current state.

Training hyperparameters. The paper specifies:

• Maximum sequence length: 4096 tokens
• Learning rate: $2 \times 10^{-5}$
• Minimum learning rate: $1 \times 10^{-6}$
• Batch size: 256
• Cosine learning rate schedule
• At most 4 epochs of training
• Checkpoint selection based on miniF2F validation set performance

Design rationale for hyperparameter choices. The 4096-token context window accommodates lengthy proof states that can include many hypotheses and complex goal expressions. The learning rate of $2 \times 10^{-5}$ is a standard fine-tuning rate for 7B-scale models — high enough to learn new task-specific behaviors but not so high as to catastrophically forget pretraining knowledge. The cosine schedule with minimum LR of $1 \times 10^{-6}$ provides aggressive early learning that gradually stabilizes. Training for at most 4 epochs with checkpoint selection on the validation set prevents overfitting to the synthetic training data, which may contain patterns that do not generalize to benchmark problems. The batch size of 256 is a standard throughput-constrained choice for 7B-model fine-tuning.

Inference-time sampling configuration. At inference (during both training data generation and benchmark evaluation), the policy model samples $K = 8$ tactics per state. The sampling uses four temperature values — 0.7, 0.8, 1.0, and 1.1 — with 2 tactics sampled at each temperature. This temperature schedule is "empirically decided" (the paper provides no ablation for these values). The multi-temperature sampling serves to balance exploitation (lower temperatures produce more focused, higher-probability tactics) and exploration (higher temperatures produce more diverse tactics that may discover non-obvious proof paths). The total of 8 tactics per expansion step is the branching factor of the search tree.

Tree Search Algorithm: Best-First Search (BFS)

Best-First Search (Section 3.1) is the primary search algorithm used both for generating training data during iterative improvement and for benchmark evaluation. The paper formalizes BFS as an iterative process of selection and expansion operating on a tree of proof states.

State representation. Each node $n_i$ in the search tree corresponds to a LEAN proof state $s_i$ — a snapshot of the goals, hypotheses, and context at a particular point in the proof. The root node $n_0$ corresponds to the initial statement $q$ with no tactics applied. An edge from $n_i$ to $n_j$ represents successfully applying a single tactic at state $s_i$ that transforms the proof state into $s_j$.

The active node set. BFS maintains a set $\mathcal{N}$ of "active" nodes — nodes that have been generated (via expansion) but not yet selected for further expansion. Initially, $\mathcal{N} = \{n_0\}$ (only the root). Nodes are never removed from $\mathcal{N}$ once added; instead, they are selected without replacement, meaning each node is expanded at most once.

Selection step. At each iteration, BFS selects the node $\hat{n}$ with the highest critic score from the active set:

$\hat{n} = \arg\max_{n \in \mathcal{N}} \text{CRITIC}(n)$

where $\text{CRITIC}(\cdot)$ is one of the three critic functions (policy confidence, PRM, or distance critic), $\mathcal{N}$ is the set of active nodes, and $\hat{n}$ is the selected node.

What this computes: Among all unexplored nodes, pick the one that the critic believes is most likely to lead to a complete proof. The critic function maps a proof state to a scalar score — higher scores indicate more promising states. The argmax over $\mathcal{N}$ implements a greedy exploitation strategy: always pursue the most promising-looking branch.

Why this form: This is the defining characteristic of best-first search — it prioritizes depth in promising branches over breadth of exploration. The effectiveness depends entirely on critic quality; if the critic is well-calibrated, BFS efficiently focuses computation on branches likely to succeed. If the critic is noisy or biased, BFS may waste computation on dead ends while neglecting successful paths deeper in the tree.

Expansion step. Once a node $\hat{n}$ is selected, the policy model $\pi$ samples $K = 8$ candidate tactics:

$\hat{\mathcal{C}} = \{\hat{c}_i \mid \hat{c}_i \sim \pi(q, \hat{n}), i \in [0, \ldots, K]\}$

where $\pi(q, \hat{n})$ is the policy's distribution over next tactics given the statement $q$ and the state at node $\hat{n}$, and $\hat{\mathcal{C}}$ is the set of $K$ sampled candidates.

Executing tactics against LEAN. Each candidate tactic $\hat{c}_i$ is executed against the LEAN4 engine. If the tactic is valid under state $s_{\hat{n}}$, LEAN returns a new proof state; the resulting node is added to the active set $\mathcal{N}$. If the tactic is invalid (syntax error, type mismatch, or tactic preconditions not met), it is discarded. This LEAN-mediated filtering ensures that only valid proof steps enter the search tree — the tree contains exclusively states reachable from the root through sequences of valid tactic applications.

Deduplication. Before adding new nodes to $\mathcal{N}$, the system checks for duplicates: if the new proof state is identical (via string matching) to any previously explored node, it is discarded. This prevents the search from cycling or redundantly exploring the same state through different tactic sequences. String matching is a simple but effective deduplication strategy: LEAN states have canonical text representations, so identical states produce identical strings.

Termination conditions. BFS terminates under two conditions: (1) success — a node is reached where the LEAN state has no remaining goals (the proof is complete), in which case the path from root to that node is returned as the proof $\tau$; or (2) budget exhaustion — the maximum number of iterations $T = 800$ is reached without finding a proof, in which case the search fails and returns null. Additionally, a per-step timeout of 60 seconds and a whole-proof timeout of 3600 seconds are enforced for LEAN tactic execution.

Interaction with the critic loop. The critic function is evaluated on each node when it enters $\mathcal{N}$ (either at initialization for the root or after expansion for new nodes). The critic scores determine the selection order for the entire search. Since BFS selects nodes without replacement, each node gets exactly one expansion opportunity with a budget of $K = 8$ candidate tactics. This contrasts with MCTS, which can revisit and re-expand nodes with a dynamically updated budget.

Search cost notation. The paper reports search cost in the format $\#\text{Pass} \times \#\text{Beam} \times \#\text{Iteration}$ for BFS. For HUNYUANPROVER v16+BFS+DC, this is $600 \times 8 \times 400$. Interpreting this notation: 600 passes (independent search attempts per theorem), each maintaining 8 beams (the branching factor $K$), with up to 400 iterations (selection+expansion cycles) per pass. The total tactic evaluations per theorem is therefore up to $600 \times 8 \times 400 = 1,920,000$ in the worst case (though many passes will terminate early upon finding a proof, so the average is lower).

Tree Search Algorithm: ηMCTS (Monte Carlo Tree Search)

ηMCTS (Section 3.1) adapts the algorithm from Tian et al. (2024) to address specific limitations of BFS. The paper identifies two limitations: (1) each node is visited only once with a fixed expansion budget, preventing the algorithm from allocating more computation to promising nodes as more information becomes available; (2) BFS relies purely on the critic score without any exploration mechanism, making it vulnerable to critic bias or misjudgment.

Four-step cycle (modified). The original ηMCTS algorithm cycles through selection, expansion, simulation, and backpropagation. HUNYUANPROVER's adaptation removes the simulation step entirely:

"Here we remove the step of simulation, leaving it for future work."

This means ηMCTS in this paper operates as a three-step cycle: selection, expansion, backpropagation. The removal of simulation (where the model would roll out a complete proof from a node to estimate its value) simplifies the algorithm and reduces computation, but it also means ηMCTS relies entirely on the critic model for value estimates rather than combining critic values with Monte Carlo rollouts — a design choice the paper acknowledges as incomplete.

Multi-visit capability. A fundamental difference from BFS is that ηMCTS can select and expand the same node multiple times. The expansion budget per node is not fixed at $K$; instead, it is dynamically determined by an importance score that evolves as the search tree grows.

Importance score. For any node $n$, the importance score $I(n)$ is defined as the maximum absolute difference between its critic score and the critic scores of all its descendants:

$I(n) = \max_{\hat{n} \in \text{SUCC}(n)} |\text{CRITIC}(\hat{n}) - \text{CRITIC}(n)|$

where $\text{SUCC}(n)$ represents all succeeding (descendant) nodes of node $n$ in the search tree, including both direct children and deeper descendants. $\text{CRITIC}(\cdot)$ is the critic function.

What this computes: $I(n)$ measures how much the critic's assessment changes as the proof progresses from node $n$. A large importance score means that some descendant of $n$ has a substantially different critic score — either much better (the proof is progressing well) or much worse (the branch is headed toward failure). A small importance score means all descendants have similar critic scores, suggesting the node is in a "flat" region where additional exploration is unlikely to change the assessment significantly.

Why this form: The importance score captures information gain potential. Nodes with high importance have proven to lead to states with divergent critic scores — expanding them further may discover even better states (or confirm that the apparent good branches are illusory). Nodes with low importance have consistent scores across descendants — further expansion is unlikely to yield surprising new information. This provides a principled basis for allocating computation: nodes that have demonstrated "interesting" behavior (large score variation) get more expansion budget.

Dynamic expansion budget. The expansion budget for node $n$ is computed from its importance score:

$E(n) = \max(B_{\text{min}}, \min(B_{\text{max}}, \lfloor \alpha I(n) \rfloor + 1))$

where $B_{\text{min}}$ is the minimum expansion budget (a lower bound ensuring every node gets at least some exploration), $B_{\text{max}}$ is the maximum expansion budget (an upper bound preventing any single node from consuming all computation), $\alpha$ is a scaling factor that maps importance scores to budget units, and $\lfloor \cdot \rfloor$ denotes the floor function (rounding down to the nearest integer). The specific values of $B_{\text{min}}$, $B_{\text{max}}$, and $\alpha$ are not stated in the paper.

What this computes: The base budget for a node is 1 (ensuring at least one candidate is sampled). Additional budget is allocated proportionally to importance: $\lfloor \alpha I(n) \rfloor$ additional candidates. The result is clamped to $[B_{\text{min}}, B_{\text{max}}]$. Nodes that have shown large score divergence among their descendants receive more expansion budget; nodes in flat regions receive the minimum.

Why this form: The linear relationship between importance and budget (modulated by $\alpha$ and clamped) is a simple heuristic that operationalizes the principle "explore more where interesting things are happening." The clamps ensure stability — no node starves completely, and no node monopolizes the budget. This is an intuitive but hyperparameter-sensitive design; the paper provides no ablation on $B_{\text{min}}$, $B_{\text{max}}$, or $\alpha$.

Upper Confidence Bound (UCB) selection. Unlike BFS, which selects nodes purely by critic score, ηMCTS uses UCB to balance exploitation and exploration:

$\text{UCB}(n) = \text{CRITIC}(n) + \alpha \times \sqrt{\frac{2 \times \ln \text{CNT}(\text{PRNT}(n))}{\text{CNT}(n)}}$

where $\text{PRNT}(n)$ is the parent node of $n$ in the search tree, $\text{CNT}(n)$ is the number of times node $n$ has been visited (selected for expansion) so far, and $\alpha$ is an exploration-exploitation tradeoff parameter (likely distinct from the $\alpha$ in the expansion budget formula, though the paper uses the same symbol).

What this computes: The UCB score has two terms. The first term $\text{CRITIC}(n)$ is the exploitation component — it favors nodes with high critic-assigned value. The second term $\alpha \times \sqrt{\frac{2 \ln \text{CNT}(\text{PRNT}(n))}{\text{CNT}(n)}}$ is the exploration component — it grows when a node has been visited fewer times than expected given its parent's total visit count. The square-root-log term is the standard UCB1 exploration bonus from the multi-armed bandit literature: it ensures that every child of a frequently-visited parent eventually gets revisited, even if its critic score is low, preventing the search from permanently abandoning potentially fruitful branches due to early noisy critic assessments.

Why this form: The UCB formula addresses BFS's vulnerability to critic bias. If the critic incorrectly assigns a low score to a node that actually leads to a proof, BFS may never expand it (especially if many other nodes have higher scores). UCB ensures that even low-scored nodes get occasional visits — initially because $\text{CNT}(n)$ is small and the exploration term dominates, later because the exploration term decays logarithmically with visits and asymptotically the exploitation term dominates. The exploration bonus is proportional to $\text{CNT}(\text{PRNT}(n))$ — nodes with frequently-visited parents (i.e., nodes in promising regions of the tree) get more exploration pressure than nodes in rarely-visited regions.

Increased per-expansion sampling. Another modification from the original ηMCTS is that expansion samples $K$ candidate tactics (matching BFS) rather than a single tactic as in Tian et al. (2024). This means each visit to a node produces up to $K$ new children (filtered by LEAN validity and deduplication), making ηMCTS more sample-efficient per visit at the cost of potentially generating redundant children.

Backpropagation. After expansion, the critic scores of the newly generated nodes are propagated back up the tree to update the importance scores of ancestor nodes. This is the mechanism by which ηMCTS dynamically reallocates budget: if a newly discovered descendant of node $n$ has a very different critic score from $n$, $I(n)$ increases, and subsequent visits to $n$ will have larger expansion budgets. The paper does not detail the specific backpropagation update rule, but it follows the standard MCTS pattern of updating aggregate statistics (visit counts, value estimates) along the path from the expanded node to the root.

MCTS cost notation. The paper reports MCTS cost as $\#\text{Pass} \times \#\text{Iteration}$ — notably omitting the beam dimension, since beam width is dynamically determined per node rather than fixed. The paper does not provide cost numbers for MCTS in Table 1 (only BFS costs are shown), making direct cost comparisons difficult.

Critic Model 1: Policy Confidence (PC) — The Cold-Start Baseline

Policy confidence (Section 3.2) is the simplest critic — it requires no separate model training and serves as the initial guidance signal before enough search data is accumulated to train learned critics.

Definition. For a tactic $c$ generated under state $n$ while proving statement $q$, the policy confidence $f^{\pi}(c)$ is the token-level average log probability:

$f^{\pi}(c) = \frac{1}{|c|} \sum_{j=1}^{|c|} \log p_{\pi}(c_j \mid q, n, c_{<j})$

where $|c|$ is the number of tokens in tactic $c$, $c_j$ is the $j$-th token of the tactic, $c_{<j}$ represents all preceding tokens, and $p_{\pi}(c_j \mid q, n, c_{<j})$ is the policy model's predicted probability for token $c_j$ given the statement $q$, the current state $n$, and the partial tactic prefix.

What this computes: For each candidate tactic, compute the average log probability across all its tokens. This is the per-token likelihood the policy model assigns to its own generation — essentially, how confident the model is that this tactic is correct. Higher average log probability means the model is more certain; lower means the model is more uncertain or the tactic contains unlikely token choices.

How it is used as a critic score. In BFS or ηMCTS, the critic score for a node is derived from the policy confidence of the tactic that produced it. The paper implies but does not explicitly state whether the node score is the confidence of the single tactic that created it, or some aggregation. Based on standard practice, the score for node $n_j$ (produced by applying tactic $c$ at node $n_i$) would be $f^{\pi}(c)$ — the confidence of the edge, treated as a proxy for the quality of the resulting state.

Design rationale — why PC as a cold start. Policy confidence has zero training cost and is always available because it is derived directly from the policy model's output distribution. It provides a natural warm-start signal: tactics the model is confident about are more likely to be correct (or at least syntactically valid) than tactics the model assigns low probability. The paper states:

"We first leverage policy confidence as guidance for a cold start of guided search due to limited tree-search data for training critic models at the beginning."

This is specifically about the early iterations of the data generation pipeline: before the policy has been strengthened through RFT, and before enough search trees have been generated to train a PRM or distance critic, PC is the only available guidance signal.

Limitations. Policy confidence is a proposal-side signal — it captures how likely the policy thinks the tactic is, not how useful the resulting state actually is for completing the proof. A model can be highly confident about a tactic that leads to a dead end, or uncertain about a tactic that leads to an elegant solution. As the paper demonstrates in Table 2, replacing PC with learned critics (PRM, DC) consistently improves performance — at v14, moving from (BFS, PC) at 62.70% to (BFS, DC) at 65.57% represents a 2.87-point gain, confirming that learned outcome-based critics provide substantially better search guidance than policy confidence alone.

Critic Model 2: Process Reward Model (PRM) — Learned Success Prediction

The Process Reward Model (PRM), denoted $v^{\pi}_{\phi}(q, n)$, is a learned critic that predicts whether a given proof state $n$ can eventually lead to a successful proof of statement $q$ when following policy $\pi$. It is parameterized by $\phi$ and trained on automatically labeled data from previous search trees.

Semantics. The PRM estimates the value of a proof state — the probability that, starting from state $n$, the policy model $\pi$ will eventually produce a complete valid proof of $q$. This is analogous to a value function in reinforcement learning: $v^{\pi}_{\phi}(q, n) \in [0, 1]$ represents the expected success probability from state $n$.

Training data generation. For each statement $q_k$ in a training set $D$ (presumably a subset of the autoformalized statements), the system first generates a search tree by running policy $\pi$ under the guidance of the critic from the previous iteration. The paper notes this uses "the critic from the previous iteration," implying a bootstrapping process: early PRMs are trained on trees generated with PC guidance, later PRMs are trained on trees generated with PRM guidance, and so on.

Labeling nodes. Each node $n^k_i$ in the search tree for statement $q_k$ is assigned a binary label $l^k_i$:

$l^k_i = \begin{cases} +1 & \text{if node } n^k_i \text{ can reach a final state indicating successful proving of } q_k \\ -1 & \text{otherwise} \end{cases}$

What this labeling does: Any node that has a descendant which is a terminal success state (the proof is complete) receives a label of +1. All other nodes receive -1. This is an outcome-based labeling: the label reflects whether the node lies on a path to a discovered proof, not an absolute assessment of the node's provability (there may exist undiscovered proof paths from a node labeled -1).

Why ±1 binary labels rather than soft labels: The paper follows Wang et al. (2024c) in using binary labels rather than Monte Carlo rollout fractions (as in Math-Shepherd or the reference example's PRM training). The binary approach is simpler to implement and was "proven effective in the experiments of Wang et al. (2024c)." However, it discards information: a node from which 9 out of 10 rollouts succeed and a node from which 1 out of 10 rollouts succeed would both receive +1 if at least one path to success was found in the search tree. This coarse labeling potentially makes the PRM less calibrated than soft-label alternatives, but the paper does not compare the two approaches.

Dataset construction. The resulting PRM dataset is:

$D_v = [(q_k, n^k_i, l^k_i), \ldots]$

containing (statement, state, binary label) triples for all nodes across all search trees.

Training objective. The PRM is trained by minimizing mean squared error between its prediction and the binary label:

$v^{\pi}_{\phi} = -\mathbb{E}_{(q_k, n^k_i, l^k_i) \sim D_v} \left(v^{\pi}_{\phi}(q_k, n^k_i) - l^k_i\right)^2$

where $v^{\pi}_{\phi}(q_k, n^k_i)$ is the model's scalar prediction for state $n^k_i$ of statement $q_k$, and $l^k_i \in \{-1, +1\}$ is the binary label.

What this computes: The PRM is optimized to output values close to +1 for states that lead to a discovered proof and close to -1 for states that do not. The squared error penalizes deviations from the label: if a "good" state (label +1) receives a prediction of 0.3, the error is $(0.3 - 1)^2 = 0.49$; if a "bad" state (label -1) receives a prediction of 0.5, the error is $(0.5 - (-1))^2 = 2.25$. The expectation is taken over the empirical distribution of the dataset $D_v$.

Why MSE rather than binary cross-entropy: The paper uses MSE, which treats the prediction as a regression target rather than a probability. This is a design choice following Wang et al. (2024c). MSE with ±1 targets effectively trains the model to output scores centered around +1 for good states and -1 for bad states. Binary cross-entropy with 0/1 targets would instead train the model to output calibrated probabilities. The MSE formulation makes the PRM's output interpretable as a signed quality score rather than a probability, which may be more natural for the argmax selection in BFS (Equation 2) where relative ordering matters more than absolute calibration.

Model architecture. The PRM is "a LLM with an MLP layer on top to output a scalar for each token." The underlying LLM is likely the same HUNYUAN 7B architecture as the policy model, but with the language modeling head replaced or augmented by a multi-layer perceptron that maps the final hidden state to a scalar value. The paper states that "we use the scalar prediction at the last token of each state as the value" — the PRM processes the entire state representation (statement + current goals + hypotheses) as a text sequence, and the scalar output at the final token position is taken as the value for that state. This architecture, following Wang et al. (2024c), leverages the LLM's pretrained understanding of LEAN syntax and mathematical semantics while adding a lightweight regression head for value prediction.

Usage in search. During BFS or ηMCTS, $\text{CRITIC}(n) = v^{\pi}_{\phi}(q, n)$ — the PRM's scalar output for the state at node $n$ is used directly as the critic score. Higher values indicate states that the PRM believes are more likely to lead to a successful proof. In BFS, this score determines selection priority (Equation 2); in ηMCTS, it enters both the UCB exploitation term and the importance score computation (Equation 4).

Limitation that motivates the Distance Critic. The PRM captures whether a proof is likely to be found from a state, but not how close the state is to completion. Two states might both be labeled +1 (proof reachable) but differ substantially in the number of remaining steps: one might need 2 more tactics, another might need 20. The PRM provides no signal to distinguish these cases — both receive similar scores near +1. The distance critic is designed to address this limitation by providing fine-grained distance estimates that help the search algorithm prioritize states closer to completion.

Critic Model 3: Distance Critic (DC) — Coarse-to-Fine Distance Estimation

The distance critic (Section 3.2) is the paper's most novel methodological contribution. It addresses a specific shortcoming of the PRM — the inability to distinguish between states that are close to proof completion versus states that are far away — by predicting the estimated number of remaining proof steps. The key innovation is the hierarchical binary tree representation that mitigates the data sparsity problem inherent in direct integer prediction.

Motivation — the data sparsity problem. Directly training a model to predict the exact number of remaining steps (an integer from 1 to, say, 64) would face severe data sparsity: in a dataset of proof trees, each possible distance value appears relatively few times, and the model has no way to share statistical strength between similar distances. For example, states that are 7 steps from completion and states that are 8 steps from completion are very similar in their characteristics (both are "fairly close"), but a direct regression or classification model would treat them as entirely separate categories, learning independent parameters for each distance value from limited examples. The binary tree representation solves this by introducing a hierarchical structure where predictions at coarser levels are shared across many distance values.

Binary tree structure. The distance critic uses an 8-level balanced binary tree capable of representing numbers from 1 to 64 (since a balanced binary tree with 8 levels can represent $2^8 = 256$ values at the leaves, but the paper states it represents "numbers up to 64"). Each node in the tree is represented by a special token — for example, the node representing "1/2" (the left half of the root split) is tokenized as <|num-1-of-2|>, and "5/8" is tokenized as <|num-5-of-8|>.

Path representation. Any number from 1 to 64 corresponds to a unique path from the root to a leaf in the binary tree. At each level, the path chooses left or right based on whether the number falls in the left or right half of the current range. For example, as illustrated in Figure 2 for a 4-level tree (representing numbers 1-8), the number 6 corresponds to the path:

root → 2/2 → 3/4 → 6/8

This path can be expressed as a tuple of the fractional node labels: (2, 3, 6). Each element represents a finer-grained classification: at level 1, the number is in the right half (2/2); at level 2, it is in the third quarter of the full range (3/4); at level 3, it is exactly 6 out of 8 (6/8). With an 8-level tree, the path would have 8 elements, providing progressive refinement from coarse (which half?) to fine (exactly which number?).

Why a binary tree specifically. The binary tree's hierarchical structure means that two numbers that are close in value share a common prefix in their paths. For instance, numbers 5 and 6 both fall in the right half (2/2) and the third quarter (3/4), diverging only at the leaf level (5/8 vs. 6/8). The model learns to predict the path one level at a time, with predictions at higher levels benefiting from all training examples in that subtree. This coarse-to-fine structure allows the model to first make broad, reliable predictions (which half? which quarter?) before refining to exact numbers, and errors at fine levels are less severe because the coarser prediction is still informative for search guidance.

Training data construction. For each node in the search trees generated during iterative training, the true distance (number of remaining tactics) to a successfully proved terminal state is computed. If the distance exceeds 64, it is clamped to 64:

"If the number of remaining steps exceeds 64, we set it to 64."

This clamping means all states with distance 64 or more are treated as a single "far" category, which is a reasonable simplification since the critic's discrimination power is most important for distinguishing close states (where small differences in remaining steps matter for search prioritization) from far states.

Training format. The distance critic is trained as a language model that, given the LEAN state as input, outputs a structured prediction in a specific format. The Appendix C example shows:

Response
Let me think step by step.
......
So, there is <num_box><num-1-of-2><num-1-of-4><num-1-of-8>
<num-2-of-16><num-4-of-32><num-7-of-64></num_box> more tactic
steps are needed to finish this state.

The special tokens <num-1-of-2>, <num-1-of-4>, etc. represent the path through the binary tree. This example's path corresponds to a specific number (which can be decoded from the binary tree structure). The distance critic is a standard fine-tuned language model that outputs these special tokens in sequence, with the full path enclosed in <num_box>...</num_box> delimiters.

Inference and comparison. During tree search, when the distance critic is used as the critic function, two states are compared by comparing their predicted tuples:

"During the tree-search stage with the distance critic, we compare two states by directly comparing their corresponding tuples. This approach inherently evaluates states in a coarse-to-fine manner."

The comparison is hierarchical: first compare the level-1 prediction (which half?), then level-2 (which quarter?), and so on. This means the distance critic naturally prioritizes states that are closer to completion (lower distance) over states that are farther, with ties at coarse levels being broken by finer levels. The coarse-to-fine comparison also means that if the model makes an error at a fine level (e.g., predicting 7/64 instead of the correct 8/64), the state's ordering relative to states predicted at 20/64 will still be correct because the coarse levels agree.

Integration with BFS. In BFS with distance critic guidance, the $\text{CRITIC}(n)$ in Equation 2 is implicitly the negative distance (or the distance tuple used in a min-comparison) — the search selects the node with the smallest predicted remaining distance. The paper's notation simplifies this; operationally, the argmax over critic scores becomes an argmin over predicted distances. The distance critic provides strictly more information than the PRM because it not only identifies which states can reach a proof but also ranks them by estimated proximity to completion, enabling more fine-grained prioritization.

Empirical impact. Table 2 shows the effect of substituting the distance critic for policy confidence:

• At v14: BFS+PC = 62.70%, BFS+DC = 65.57% (+2.87 points)
• At v16: BFS+PC = 64.75%, BFS+DC = 68.44% (+3.69 points)

These gains are substantial and increase with prover version, suggesting that as the prover becomes more capable (solving harder problems with longer proofs), the distance critic's fine-grained guidance becomes more valuable compared to coarser signals like PC or PRM. Figure 4 further shows that BFS+DC discovers more deep proofs (length >9 steps) compared to BFS+PC, while both methods perform similarly on short proofs (1-3 steps) — the distance critic's advantage is specifically in navigating the longer, more complex proof searches.

CLARIFICATION NEEDED. The paper does not specify how the distance critic score is converted to a single scalar for the argmax in BFS (Equation 2) given that the output is a tuple, not a scalar. The operational procedure (tuple comparison) is described, but the formal mapping from tuple to scalar is left implicit. Additionally, the paper does not state the training objective for the distance critic — it is presumably standard autoregressive language modeling loss on the special token sequence, but this is not specified.

Summary of Design Choices and Their Justifications

• Autoformalization with multi-temperature sampling and rule-based filtering over pure human annotation: economically necessary to scale from 50K to 20M statements; the 8-sample-per-problem strategy with diverse temperatures trades compute for coverage, catching multiple plausible formalizations per problem.
• Iterative RFT over single-pass training or RL: RFT is simpler and more stable than RL; the iterative structure provides exploration through progressive data accumulation (each round's prover can solve harder problems, generating training data that the previous round couldn't); monotonic data growth prevents catastrophic forgetting.
• Post-v12 data curation (removing easy examples) over continued scaling of all data: empirical finding that training on only the harder portion of the data improves benchmark performance, likely because easy examples cause the model to overfit to simple proof patterns that don't transfer to miniF2F difficulty.
• 8-level binary tree for distance prediction over direct integer regression or flat classification: the hierarchical structure mitigates data sparsity by sharing statistical strength at coarse levels; the path representation naturally captures distance similarity (close numbers share prefixes); the coarse-to-fine comparison enables robust state ordering even when fine-level predictions are noisy.
• ηMCTS with removed simulation over full MCTS: acknowledges the theoretical advantage of MCTS exploration (UCB, dynamic budget) while simplifying implementation and reducing computation; leaves simulation (rollout-based value estimation) as future work, relying entirely on the learned critic for node evaluation.
• ±1 binary labels for PRM over soft Monte Carlo labels: follows established practice (Wang et al., 2024c) that was empirically effective; simpler to implement than rollout-based soft targets; the potential loss of calibration information is an acknowledged tradeoff.
• Multi-temperature tactic sampling (0.7, 0.8, 1.0, 1.1, two per temperature) over single-temperature or purely random sampling: the temperature sweep balances focused exploitation (lower temps) with diverse exploration (higher temps), providing the search with both high-probability candidates and creative alternatives; the specific values are empirically determined without formal ablation.

4. Key Insights and Innovations

Innovation 1: Data Quality Filtering as a Second-Stage Scaling Law — Removing Easy Data Improves Performance After Sufficient Volume

The paper’s most counterintuitive and potentially impactful conceptual contribution is the empirical demonstration that when training an iterative theorem prover, there exists a crossover point beyond which removing easy training data improves performance more than adding more data. This is visible in Figure 3, where performance plateaus around iteration v12 at roughly 4.25B training tokens, and then increases after v12 when the authors deliberately “remove some easy training data” from early iterations. By v16, BFS+PC accuracy reaches 64.75% — a gain achieved not by scaling data volume further but by curating the difficulty distribution of the existing data.

What the field assumed before this work. The dominant paradigm in LLM training — both pretraining and fine-tuning — has been that more data is better, with filtering focused on removing noise (bad formatting, incorrect answers, toxic content) rather than removing correct but easy examples. In the theorem-proving domain specifically, prior systems (DeepSeek-Prover, InternLM2.5-StepProver, Lean-STaR) all emphasized data scale as the primary lever — generating more synthetic proofs, training on more examples, iterating to accumulate progressively larger datasets. The implicit assumption was that easy proofs are at worst harmless, providing useful practice on basic tactic usage. The idea that easy data could become actively detrimental after a certain volume threshold — that it would cause the model to overfit to simple proof patterns at the expense of the harder reasoning needed for benchmark performance — was not articulated or tested in prior work.

Why this is a conceptual advance rather than an incremental tuning trick. The finding is not simply “curate your data” (which is well-known) but rather that the optimal data composition is a function of total data volume. This introduces a two-phase scaling dynamic: in Phase 1 (early iterations, insufficient total data), maximizing data quantity dominates — you need enough examples for the model to learn basic tactic usage and proof structure, and filtering would be counterproductive because it would reduce an already-scarce resource. In Phase 2 (post-saturation, sufficient total data), data quality and difficulty composition dominate — the model already knows how to apply basic tactics, and seeing more easy proofs just reinforces patterns that don’t transfer to the hard problems that determine benchmark performance. This is conceptually analogous to curriculum learning but with an inverted signal: rather than ordering examples from easy to hard during training, the insight is that once the curriculum is complete, you remove the early lessons entirely for subsequent fine-tuning rounds.

This two-phase dynamic is not predicted by standard scaling laws, which model monotonic relationships between data volume and loss. It suggests that iterative self-improvement systems (expert iteration, STaR, RFT) may have a built-in tension: early iterations generate predominantly easy proofs because the prover is weak, and retaining all of them indefinitely creates a training distribution skewed toward simplicity that eventually caps performance. The paper’s solution — retrospectively pruning easy data from early iterations — is a post-hoc correction for this distributional skew, and the fact that it works (a multi-point gain in Figure 3) suggests the skew is a real and significant problem that other iterative self-improvement systems likely also suffer from.

Tie to evidence. Figure 3 shows the inflection clearly: v8 (2.75B tokens, ~62%), v10 (3.5B tokens, ~62.5%), v12 (4.25B tokens, ~62%) — essentially flat. Then after removing easy data, v14 reaches ~63% and v16 reaches ~64.75% with BFS+PC (and 68.44% with BFS+DC in Table 2). The paper states: “Most of the removed training data are relatively easy statements. We can see the performance boost is achieved by removing these easy data. This highlights the importance of data selection in the iterative improving process.” The fact that they tested this at all — that they tried reducing training data after seeing a plateau — reflects a diagnostic mindset that prior work in the space did not exhibit, where the default response to a plateau would be “generate more data” or “improve the search algorithm.”

Innovation 2: The Distance Critic as a Learned Search Heuristic That Solves the Data Sparsity Problem Through Hierarchical Representation

The distance critic represents the paper’s primary architectural innovation at inference time, and its conceptual contribution is the insight that coarse-to-fine hierarchical prediction can provide richer search guidance than binary success/failure signals while being trainable from exactly the same automatically-labeled data. This is a diagnostic move: identifying what specific information would improve search beyond what a standard PRM provides (distance to goal, not just reachability), recognizing why directly predicting that information is difficult (data sparsity — each integer distance value appears too rarely in training data to learn reliably), and then designing a representation (the balanced binary tree) that makes the prediction problem tractable by sharing statistical strength across similar distances.

What the field did before. Prior critic models for theorem proving and mathematical reasoning fell into two categories. Outcome reward models (ORMs) and process reward models (PRMs) — including Math-Shepherd (Wang et al., 2024c), which this paper directly builds on — predict a binary or continuous value representing the probability of eventual success from a given state. These tell the search algorithm whether a state is promising but not how promising relative to other promising states. Two states that both eventually lead to a proof receive similar positive scores even if one is 2 steps from completion and the other is 20 steps away. Policy confidence — used as the cold-start critic in this paper and the default in systems without learned critics — is even coarser, providing only a measure of the policy model’s certainty about its own output without any outcome information at all. The conceptual limitation of both approaches is that they provide a one-dimensional signal (good vs. bad) for what is fundamentally a structured problem: proof states differ not just in provability but in how much work remains, and an optimal search should prioritize states that are both provable and close to completion.

Why the binary tree representation is the key conceptual move, not just an implementation detail. The paper could have attempted to train a critic to directly regress on the remaining number of steps (output a scalar), which is the naive solution. The authors explicitly reject this approach, stating: “it is likely to suffer from data sparsity issue. When the state is very complex, it is very difficult to predict an accurate number of the remaining steps.” This diagnosis is correct and non-obvious: in a dataset of proof trees, the number of training examples at each exact distance value is small, especially for large distances. A model trained to output “37 steps remaining” from a handful of examples would be unreliable.

The binary tree representation solves this by transforming a sparse regression problem into a hierarchical classification problem where predictions at coarse levels are trained on orders of magnitude more data. The root-level prediction (“left half [1-32] or right half [33-64]?”) is trained on all examples — half the dataset goes to each branch. The second-level prediction is trained on half the data, the third level on a quarter, and so on. Each level is a binary classification with roughly balanced classes (by design of the balanced tree), and errors at fine levels don’t invalidate the coarser prediction. This is a form of parameter sharing through representation design: rather than learning independent parameters for each distance value, the model learns a shared representation where similar distances (e.g., 7 and 8) share most of their prediction path and differ only at the finest levels.

The hierarchical comparison procedure — comparing two states by comparing their predicted tuples depth-first — inherits this robustness. If the model correctly predicts that state A is in the left half (closer to completion) and state B is in the right half, the comparison is resolved at level 1 and subsequent errors at finer levels don’t matter. This “coarse-to-fine evaluation” (the paper’s phrase) means the distance critic degrades gracefully with prediction uncertainty — it’s more reliable at distinguishing states with large distance gaps (which are correctly ordered at coarse levels) than states with small gaps (which require fine-level accuracy). This property matches exactly what a search algorithm needs: the ability to confidently prioritize a state 5 steps from completion over a state 40 steps from completion, without needing perfect discrimination between states 5 and 6 steps away.

Why this is a conceptual contribution beyond theorem proving. The binary tree representation is domain-agnostic — it applies to any problem where you want to predict an integer-valued quantity under data sparsity and where hierarchical coarse-to-fine predictions are acceptable. Potential applications include predicting remaining tokens in code generation, estimating dialogue turns until task completion, or forecasting rollout length in planning problems. The paper doesn’t make this generalization argument, but the architecture is transferable.

Tie to evidence. Table 2 shows the distance critic’s impact: at v14, replacing policy confidence with the distance critic improves BFS from 62.70% to 65.57% (+2.87 points); at v16, from 64.75% to 68.44% (+3.69 points). This is the single largest critic-driven improvement in the paper’s ablation. Figure 4 provides structural evidence for how the distance critic helps: it discovers more deep proofs (length >9 steps) compared to policy-confidence-guided BFS — exactly what you would expect if the critic helps the search stay focused on promising branches in long proofs rather than getting distracted by dead ends. The paper does not ablate the binary tree against direct integer regression, so we cannot quantify how much of the gain comes from the hierarchical representation versus simply having some distance signal. This is a limitation, but the conceptual argument for the binary tree’s necessity under data sparsity is well-motivated.

Innovation 3: Autoformalization as an Economic Multiplier — Converting Informal Math Corpora into Prover Training Data at 400× Scale

The paper’s autoformalization pipeline (Section 2.1) is not algorithmically novel — it fine-tunes a model on 260K parallel natural-language-to-LEAN pairs and applies it to 30M informal problems — but its conceptual contribution lies in demonstrating that autoformalization can serve as an economic bridge between the abundant resource of informal mathematics and the scarce resource of formal proof data, and that this bridge can function at sufficient scale and quality to drive a 400× expansion in usable training statements (from 50K in mathlib4 to 20M filtered LEAN statements).

What the field assumed before. Prior theorem-proving systems relied primarily on formal proof data. DeepSeek-Prover used synthetic data generation from formal statements but started from existing formal corpora. InternLM2.5-StepProver generated proofs for large-scale LEAN problems scraped from online repositories. Lean-STaR used informal thoughts interleaved with formal tactics but trained on mathlib4-style data. The common thread is that the formal statements themselves were either human-written or generated from existing formal statements — the system’s training data was bottlenecked by the size of available formal corpora. Autoformalization (converting natural language to formal statements) existed as a research direction (e.g., MMA, Lean Workbook) but had not been demonstrated as the primary data scaling mechanism for a SOTA prover — prior work used it as a supplementary data source, not as the foundation of a 400× data expansion.

Why this is an economic argument, not an algorithmic one. The 30M internal math problems the paper uses are not described as especially high-quality or carefully curated — they are “internal math problems in natural language.” The fact that the autoformalizer can process them at scale (sampling 8 outputs per problem, filtering to 20M grammatically valid LEAN statements) and that the resulting statement pool suffices to train a SOTA prover is the key claim. It means the cost structure of building a theorem prover shifts: rather than paying human experts to formalize mathematics (expensive, slow, limited scale) or relying on existing formal libraries (limited in size), an organization can leverage its existing informal math problem corpora — which many educational and tutoring companies already possess — and convert them into formal training data at the cost of autoformalizer training and inference. The 50K → 20M expansion (400×) quantifies the magnitude of this economic leverage.

The unstated economics. The paper does not report the cost of training the autoformalizer (fine-tuning on 260K pairs) or running inference on 30M problems (240M LEAN candidates at 8 samples per problem), but these are modest compared to the alternative of human formalization. Even at pessimistic estimates, generating 20M formal statements via autoformalization is orders of magnitude cheaper than human annotation — and the resulting statements, while imperfect (only ~8.3% of generated candidates pass grammatical filters), are sufficient to fuel the iterative prover training loop.

Tie to evidence. The entire iterative data generation pipeline (Figure 3) rests on the autoformalized statement pool $D_q$ of 20M LEAN statements. The prover solves progressively harder subsets of this pool across 16 iterations, generating 20M+ tactic-level training examples. Without autoformalization at this scale, the data volume would be capped at mathlib4’s 50K theorems — a 400× difference that almost certainly would produce a much weaker prover. The paper cannot ablate this (it’s the foundation, not an optional component), but the magnitude of the scale-up relative to prior systems’ training data is strong circumstantial evidence that autoformalization is load-bearing.

Innovation 4: Verifier Diversity as a Performance Diagnostic — Multiple Critics Catch Different Failure Modes

A subtler contribution emerges from the pattern of critic effectiveness across Tables 1 and 2: different critics help in different ways, and the best system uses the critic best suited to the search algorithm and data regime, not necessarily the most sophisticated critic in isolation. This is a diagnostic insight rather than a method claim — it reframes critic design from “find the single best critic” to “understand which critic works when and why.”

The evidence for complementary critic strengths. Table 2 shows a clear progression: policy confidence (the weakest critic) achieves 61.07% at v12; MCTS+PRM improves to 62.29% (+1.22 points); BFS+DC reaches 65.57% at v14 and 68.44% at v16 (+3.69 points over the PC baseline at v16). The MCTS+PRM combination at v14 (66.39%) slightly outperforms BFS+DC (65.57%), but the gap is small. The paper cannot separately ablate MCTS and PRM (they are always used together), so we cannot determine whether MCTS or PRM drives the gain. However, the pattern suggests that (1) any learned critic substantially outperforms policy confidence, (2) the distance critic provides larger gains than the PRM in BFS, and (3) MCTS with PRM may capture some of the distance critic’s benefits through its exploration mechanism — by revisiting nodes and dynamically allocating budget, MCTS partially compensates for the PRM’s inability to distinguish close states from far states.

What this means conceptually. The “best” critic is not an absolute property but depends on the search algorithm it’s paired with. The PRM’s binary good/bad signal is less informative for BFS (which visits each node once and needs precise prioritization) than it is for MCTS (which can revisit nodes and thus tolerates coarser initial scores). The distance critic’s fine-grained distance estimates are particularly valuable for BFS because that algorithm commits to a greedy ordering and never revisits nodes — getting the ordering right the first time is critical. This is not argued explicitly in the paper, but it’s the logical implication of the pattern in Table 2.

Comparison to prior work’s critic usage. Prior systems treated the critic as a plug-in component — InternLM2.5-StepProver uses critic guidance as a binary flag (“CG” indicates critic-guided search in Table 1) without analyzing which critic properties matter for which search algorithm. Lean-STaR includes a critic but achieves only 46.3%, suggesting its critic (or search integration) is substantially weaker. This paper’s three-tier critic hierarchy — tested across search algorithms and prover versions — provides a more nuanced picture: critic design isn’t just about model architecture but about the match between the critic’s output structure (scalar confidence, binary value, hierarchical distance tuple) and the search algorithm’s information needs (one-shot ordering for BFS, dynamic re-ranking for MCTS).

Tie to evidence. Table 2 provides the ablation grid: (BFS, PC) vs. (BFS, DC) vs. (MCTS, PRM) at v14, plus the v12 and v16 baselines. The 3.69-point gain from PC → DC in BFS at v16 dwarfs the 1.22-point gain from PC → PRM in MCTS at v12, but this confounds prover version with critic type. The paper acknowledges the limitation: “Due to the limitation of time and computation resources, we leave separately examining the effectiveness of MCTS and PRM in future work.” The conceptual claim here is therefore partially speculative — the paper demonstrates that critics matter and that the distance critic is strong, but it does not isolate the interaction between critic type and search algorithm. The innovation is in posing the question and providing suggestive evidence, not in definitively answering it.

5. Experimental Analysis

Evaluation Methodology

• Dataset. All experiments use the miniF2F benchmark (Zheng et al., 2022), which tests formal problem-solving on high-school-level exercises and competition problems (AMC, AIME, IMO) with a focus on algebra and number theory. The benchmark comprises 244 validation problems and 244 test problems. The paper uses the validation set for checkpoint selection during fine-tuning and the test set for final reported accuracy.

• Base model(s). The prover is fine-tuned from HUNYUAN 7B, a 7B-parameter language model. The paper does not detail this model's pretraining corpus or architecture, treating it as a known internal Tencent model. The choice of 7B parameters places HunyuanProver in the same size class as its direct competitors — DeepSeek-Prover-V1.5 (7B) and InternLM2.5-StepProver (7B) — ensuring that performance differences are attributable to training data, search strategy, and critic design rather than raw parameter count. The paper also trains separate critic models (PRM, distance critic) that are based on the same underlying architecture with task-specific prediction heads.

• Metrics. The primary metric is miniF2F-test accuracy (%) — the fraction of the 244 test problems for which the system successfully finds a valid LEAN4 proof within the search budget. A proof is "successful" if the LEAN engine verifies that the sequence of tactics establishes the target statement with no remaining goals. The paper also reports proof length distributions (Figure 4), measured as the number of tactics in the shortest discovered proof for each solved theorem, to characterize whether critic improvements enable deeper proofs. No secondary metrics (e.g., average proof length, search steps to solution) are systematically reported.

• Baselines. The paper compares against three prior state-of-the-art systems, drawn from Table 1:

  • DeepSeek-Prover-V1.5-RL+MCTS (Xin et al., 2024b): a whole-proof generation method using reinforcement learning and Monte Carlo tree search, achieving 60.2% on miniF2F-test with a sample budget of 16 × 6400.
  • DeepSeek-Prover-V1.5-RL+RMaxTS (Xin et al., 2024b): a variant using a different search strategy, achieving 63.5% at 32 × 6400.
  • Lean-STaR+BFS+CG (Lin et al., 2024): an interactive step-proving method with best-first search and critic guidance, achieving 46.3% at 64 × 1 × 50.
  • InternLM2.5-StepProver+BFS (Wu et al., 2024): interactive step-proving with best-first search but no critic guidance, achieving 59.4% at 256 × 32 × 600.
  • InternLM2.5-StepProver+BFS+CG (Wu et al., 2024): the same system with critic-guided search, achieving 65.9% at 256 × 32 × 600 — this is the prior SOTA that HunyuanProver aims to surpass.

  The paper's internal baselines include HunyuanProver v16+BFS (without distance critic, achieving 64.8%) and earlier prover versions (v12, v14) tested with different critic and search combinations in Table 2.

• Generation budget / compute accounting. The paper uses two different cost notations depending on the search algorithm. For BFS methods, cost is reported as #Pass × #Beam × #Iteration — the number of independent search attempts per theorem, the branching factor (tactics sampled per expansion), and the maximum iterations per pass. For HunyuanProver v16+BFS+DC, this is 600 × 8 × 400, yielding up to 1,920,000 tactic evaluations per theorem in the worst case. For MCTS methods (used by DeepSeek-Prover-V1.5), cost is reported as #Pass × #Iteration, omitting the beam dimension since beam width is dynamically determined. The paper does not provide a unified FLOPs or wall-clock time comparison, making cross-system cost comparisons approximate at best. Additionally, each tactic execution in LEAN is bounded by a per-step timeout of 60 seconds and a whole-proof timeout of 3600 seconds. At most 800 search steps (selection + expansion cycles) are conducted for both BFS and MCTS. Temperature values for sampling are fixed at 0.7, 0.8, 1.0, and 1.1, with two tactics sampled per temperature, for a total of K = 8 tactics per expansion.

• Cross-validation / statistical protocol. The paper does not report cross-validation, confidence intervals, or statistical significance tests. Checkpoint selection during fine-tuning uses the miniF2F validation set (244 problems), and final results are reported on the miniF2F test set (244 problems). The difficulty binning used in other theorem-proving papers (e.g., by problem source or difficulty tier) is absent here — results are reported as aggregate accuracy across all 244 test problems. The absence of error bars or significance testing means that the reported differences (e.g., 68.4% vs. 65.9%, a 2.5-point gap on 244 problems) cannot be assessed for statistical reliability from the information provided.

Main Quantitative Results

Overall Benchmark Performance (Table 1)

The headline result: HunyuanProver v16 with BFS and distance critic guidance achieves 68.4% accuracy on miniF2F-test, surpassing the prior state-of-the-art (InternLM2.5-StepProver+BFS+CG at 65.9%) by 2.5 percentage points while using a smaller reported search budget (600 × 8 × 400 vs. 256 × 32 × 600).

Interpreting the cost comparison requires caution because the notations measure different things. InternLM2.5-StepProver's budget of 256 × 32 × 600 represents 256 passes, 32 beams, and 600 iterations — yielding up to 256 × 32 × 600 = 4,915,200 tactic evaluations per theorem, roughly 2.6× more than HunyuanProver's 1,920,000. However, both numbers are worst-case upper bounds (actual searches terminate early upon finding a proof), and the per-iteration expansion mechanics differ (InternLM2.5-StepProver maintains 32 beams throughout, while HunyuanProver expands 8 children per selected node). The paper's claim of "using less search budget" is directionally supported by the reported numbers but is not a controlled cost-matched comparison.

The distance critic's contribution is isolated by comparing HunyuanProver v16+BFS (without distance critic, using policy confidence) at 64.8% against HunyuanProver v16+BFS+DC at 68.4% — a 3.6-point gain attributable to the critic. This is the single largest factor driving HunyuanProver's SOTA status.

Compared to DeepSeek-Prover-V1.5, the best whole-proof generation system (63.5% at 32 × 6400), HunyuanProver's interactive step-proving approach with critic guidance yields a 4.9-point improvement. However, DeepSeek-Prover-V1.5 uses MCTS rather than BFS, and the cost metrics are not directly comparable.

HunyuanProver reports proving 4 IMO statements from miniF2F-test: IMO 1960 P2, IMO 1962 P2, IMO 1964 P2, and IMO 1983 P6. The paper provides the full LEAN proof for IMO 1962 P2 in Appendix A, demonstrating the system's ability to handle Olympiad-level problems. Whether these 4 problems represent all IMO problems in miniF2F-test or a subset is not stated.

Iterative Data Scaling and Data Curation (Figure 3)

Figure 3 plots miniF2F-test accuracy against total fine-tuning tokens across prover versions v2 through v16, using BFS with policy confidence as the critic throughout. The key finding is that performance gains from data scaling saturate around version v12 (4.25B tokens, ~62% accuracy), after which removing easy training data from early iterations unlocks additional improvements.

The trajectory shows three distinct phases:

• Rapid improvement (v2–v8): Accuracy climbs from roughly 52% (v2, ~0.5B tokens) to roughly 62% (v8, ~2.75B tokens) as data volume increases roughly 5.5×. This is the expected regime where more training data directly improves prover capability.
• Plateau (v8–v12): Accuracy hovers around 62% despite data volume increasing from ~2.75B to ~4.25B tokens. The prover has reached a saturation point where additional data — predominantly easy proofs from early iterations — provides diminishing returns. The paper states that after v12, they "remove some data generated from early iterations (before v8), Most of the removed training data are relatively easy statements."
• Post-curation improvement (v12–v16): After removing easy data, accuracy increases to roughly 63% at v14 and 64.75% at v16 with BFS+PC, and reaches 68.44% at v16 when the distance critic is added. This demonstrates that data quality and difficulty composition, not just volume, become the binding constraint after sufficient data scale is reached.

The paper does not report the exact amount of data removed or the precise difficulty threshold used for filtering, so the curation procedure cannot be precisely replicated from the text. The version numbering approximately corresponds to iteration count, suggesting roughly 16 rounds of iterative data generation and retraining.

Critic and Search Algorithm Comparison (Table 2)

Table 2 presents an ablation study testing different critic models and search algorithms across three prover versions (v12, v14, v16). The results establish a clear critic quality hierarchy and show that both learned critics substantially outperform policy confidence, with the distance critic providing the largest gains.

At v12:

• BFS with policy confidence: 61.07%
• MCTS with PRM: 62.29% (+1.22 points)

The improvement from MCTS+PRM over BFS+PC at this intermediate prover version is modest, and the paper cannot separate the contributions of MCTS versus PRM since they are always tested together.

At v14:

• BFS with policy confidence: 62.70%
• BFS with distance critic: 65.57% (+2.87 points)
• MCTS with PRM: 66.39% (+3.69 points over BFS+PC)

Here, both learned critics provide substantial gains over the PC baseline. MCTS+PRM slightly edges out BFS+DC (66.39% vs. 65.57%), but the gap is only 0.82 points — within the range where statistical uncertainty (unreported) could explain the difference. The important pattern is that simply replacing policy confidence with either learned critic yields a large improvement, confirming that outcome-based guidance is critical.

At v16:

• BFS with policy confidence: 64.75%
• BFS with distance critic: 68.44% (+3.69 points)

This is the paper's headline critic result. The 3.69-point gain from PC to DC at v16 is larger than the gain at v14 (2.87 points), suggesting that the distance critic's value increases as the prover becomes more capable — a stronger prover generates deeper search trees where fine-grained distance estimates matter more for efficient navigation. MCTS+PRM is not evaluated at v16, likely due to the "limitation on time and computation resources" the paper acknowledges.

Three structural limitations of this ablation deserve note. First, MCTS and PRM are never tested independently — we cannot determine whether MCTS provides value beyond BFS when both use the same critic, or whether PRM alone in BFS would match MCTS+PRM. Second, the distance critic is only tested with BFS, not MCTS — the natural experiment of (MCTS, DC) is missing. Third, the PRM is never tested as a standalone critic for BFS (BFS+PRM), which would isolate the critic effect from the search algorithm effect. These gaps mean Table 2 provides suggestive evidence about critic quality but not a clean decomposition of critic × search algorithm interactions.

Proof Length Distribution Analysis (Figure 4)

Figure 4 visualizes the distribution of solved miniF2F-test theorems by proof length (number of tactics in the shortest discovered proof) for HunyuanProver v16 with BFS+PC versus BFS+DC. The key finding is that the distance critic enables the system to discover more deep proofs without sacrificing performance on shallow proofs.

The bars show counts of solved theorems binned by proof length categories (1, 2, 3, 4, 5–6, 7–9, >9). BFS+DC matches or exceeds BFS+PC across all length categories, with the advantage most pronounced in the deepest categories:

• For proofs of length 1–3 (shallow proofs), both methods solve roughly similar numbers — the distance critic provides minimal advantage because these proofs require little search.
• For proofs of length 5–6 and 7–9, BFS+DC solves noticeably more theorems, consistent with the critic helping the search stay focused through intermediate-length proofs where branch management becomes important.
• For proofs of length >9 (deep proofs), BFS+DC again shows an advantage, demonstrating that fine-grained distance estimates help sustain effective search over many steps.

This distributional evidence supports the mechanism claimed for the distance critic: by distinguishing states that are close to completion from those that are far away, the critic helps the search algorithm allocate its limited expansion budget to branches that are genuinely progressing toward a proof, rather than wasting computation on branches that appear promising but require many more steps. The effect is most visible in intermediate-to-deep proofs where branch selection errors compound over many search steps.

The paper does not report whether the additional deep proofs discovered by BFS+DC are different theorems from those solved by BFS+PC, or whether they represent alternative proofs for theorems both systems solve. This distinction matters: if BFS+DC solves different theorems in the >9-step category, it represents an expansion of the prover's capability frontier; if it finds deep proofs for theorems that BFS+PC solves with shallow proofs, it represents improved proof diversity but not improved coverage.

Ablation Studies and Robustness Checks

Critic model type (PC vs. PRM vs. DC): Table 2 provides the primary critic ablation. Policy confidence serves as the untrained baseline. The PRM (trained on ±1 binary labels from previous search trees, using an LLM+MLP architecture with the scalar prediction at the last token) consistently outperforms PC when tested with MCTS — 62.29% vs. 61.07% at v12, 66.39% vs. 62.70% at v14. The distance critic outperforms both when tested with BFS, reaching 68.44% at v16 versus 64.75% for PC. The paper does not test (BFS, PRM) or (MCTS, DC), leaving the critic × search interaction uncharacterized. The consistent pattern is that learned outcome-based critics (PRM, DC) substantially outperform the untrained policy confidence signal, and the distance critic — which provides richer information (distance rather than binary success) — provides larger gains than the PRM when both are compared in their respective best search configurations.

Search algorithm (BFS vs. MCTS): The only direct comparison of search algorithms is at v14, where BFS+DC (65.57%) and MCTS+PRM (66.39%) achieve similar performance. However, this comparison confounds critic type with search algorithm — the 0.82-point difference cannot be attributed to BFS vs. MCTS because the critics differ. At v12, MCTS+PRM (62.29%) improves over BFS+PC (61.07%) by 1.22 points, but again the critic is not controlled. The paper acknowledges this limitation explicitly: "Due to the limitation of time and computation resources, we leave separately examining the effectiveness of MCTS and PRM in future work." No conclusions about BFS versus MCTS can be drawn from the reported experiments.

Data curation (removing easy data after v12): Figure 3 shows the effect of data curation between v12 and v16. After the plateau at v12 (~62% with BFS+PC), removing easy training data from early iterations (before v8) enables further improvement to 64.75% at v16 with the same BFS+PC configuration. This 2.75-point gain comes entirely from data quality improvement, not from additional data volume or algorithmic changes. The paper states that "Most of the removed training data are relatively easy statements" but does not specify the difficulty criterion used for filtering, the fraction of data removed, or whether the removal was done once or progressively. The robustness of this finding to alternative filtering strategies is therefore unknown.

Prover version (iterative training rounds): The progression from v12 → v14 → v16 in Table 2 shows consistent improvement across all critic configurations. BFS+PC improves from 61.07% (v12) to 62.70% (v14) to 64.75% (v16) — a total gain of 3.68 points from iterative training and data curation. BFS+DC improves from 65.57% (v14) to 68.44% (v16) — a 2.87-point gain in two versions. This confirms that the iterative data generation framework continues to provide benefits even after 12+ rounds, particularly when combined with data curation (removing easy examples) and improved critic guidance. The paper does not report whether performance would continue improving with additional iterations beyond v16, or whether a second saturation point is reached.

Temperature sampling strategy: Not ablated. The choice of four temperatures (0.7, 0.8, 1.0, 1.1) with two samples each is described as "empirically decided," with no comparison to alternative temperature schedules (e.g., all samples at a single temperature, different ranges, or different allocations per temperature). The total of K = 8 tactics per expansion is also not ablated against larger or smaller branching factors.

Distance critic tree depth: Not ablated. The paper uses an 8-level binary tree capable of representing distances up to 64, but does not test alternative depths (e.g., 4-level for distances up to 16, 10-level for distances up to 256) to determine whether the chosen granularity is optimal. The clamping of distances >64 to 64 means that all states sufficiently far from completion are treated identically; the impact of this clamping threshold on search behavior is not analyzed.

PRM labeling strategy: Not ablated. The paper uses ±1 binary labels following Wang et al. (2024c) but does not compare against soft labels (e.g., Monte Carlo rollout success fractions) used in other PRM training approaches. The choice of MSE loss rather than binary cross-entropy is also not ablated.

Diversity enhancement methods: Not ablated. The two diversity techniques — converting unfinished proof states into new statements, and collecting data from Olympiad-level problems — are described as beneficial but their individual contributions are not quantified. It is unknown whether performance would degrade without these techniques or whether one is more important than the other.

Negative result — MCTS without simulation: The paper removes the simulation step from ηMCTS "leaving it for future work," which is an acknowledged limitation rather than a tested negative result. The MCTS variant is therefore a partial implementation that relies entirely on the learned critic for value estimates without the Monte Carlo rollouts that typically provide complementary value signals in MCTS. The modest improvement of MCTS+PRM over BFS+DC at v14 (0.82 points) might be partly attributable to this omission.

Critical Assessment

The experimental section supports several of the paper's claims but leaves important gaps that prevent full validation of others.

Claim: "HunyuanProver achieves SOTA performances... 68.4% on miniF2F-test compared to 65.9%." Table 1 supports this claim numerically — 68.4% exceeds the prior best reported number of 65.9% — but several caveats weaken the comparison. First, the search budgets are not directly comparable across systems due to different cost notations and search mechanics; it is possible that HunyuanProver's advantage would shrink or disappear in a FLOPs-matched or wall-clock-matched comparison. Second, the miniF2F test set contains only 244 problems, so the 2.5-point difference represents approximately 6 additional solved problems — a difference that could arise from randomness in search, slight differences in LEAN environment configuration, or problem-specific luck rather than genuine capability improvement. No confidence intervals or significance tests are reported. Third, the paper cannot claim SOTA against systems not evaluated in the paper (e.g., any systems released between the cited baselines and HunyuanProver's development).

Claim: "Using explicitly trained critic for tree-search guidance is helpful." Table 2 provides strong support for this claim relative to the policy confidence baseline. At v16, switching from PC to DC improves accuracy by 3.69 points (64.75% → 68.44%). At v14, switching from PC to either DC (+2.87) or PRM+MCTS (+3.69) produces large gains. The evidence consistently shows that learned critics substantially outperform untrained policy confidence. However, the paper does not test whether these gains hold at smaller search budgets — it is possible that learned critics provide more value when search budgets are large (many iterations to benefit from better guidance) and less value when budgets are small (few iterations, so even poor guidance may stumble into a proof). The budget-sensitivity of critic benefits is unexplored.

Claim: "The scale of finetuning data for theorem proving is critical." Figure 3 provides partial support. The improvement from v2 (0.5B tokens, ~52%) to v8 (2.75B tokens, ~62%) clearly shows that scaling data volume improves performance in the early regime. However, after v8, data volume increases from ~2.75B to ~4.25B with essentially flat performance, suggesting that data scale alone is not sufficient — the paper's own finding is that data quality and difficulty composition become the binding constraint after a certain volume. The claim that scale is "critical" is true for the early regime but the paper's more interesting contribution is the second regime where scale stops helping and curation becomes necessary. The paper's abstract and introduction emphasize scale, but the experimental evidence in Figure 3 equally emphasizes curation — the narrative framing slightly overweights the scaling story relative to the curation story that the data actually tell.

Claim: "Data curation and selection is important as well when there is sufficient amount of training data." Figure 3 strongly supports this claim. The transition from v12 to v14/v16 — where removing easy data improves performance despite reducing training data volume — is the cleanest evidence in the paper for a novel finding. The gain is 2.75 points with BFS+PC comparing v12 (before curation, ~62%) to v16 (after curation, 64.75%). The paper does not provide an ablation comparing curation strategies (e.g., removing the easiest X% versus removing data below a difficulty threshold), so the robustness of the finding to specific curation choices is unknown, but the directional result — that pruning easy data helps after saturation — is clearly supported.

Missing experiments that would strengthen the paper. Several experiments are conspicuous by their absence. First, a cost-controlled comparison with InternLM2.5-StepProver — running both systems at matched search budgets (matched FLOPs or matched wall-clock time) — would test whether HunyuanProver's advantage is an efficiency gain or merely an accuracy gain at a different operating point. Second, BFS+PRM at v16 would isolate the critic effect from the search algorithm effect and show whether the distance critic specifically provides value beyond a standard PRM. Third, MCTS+DC at v16 would test whether the strongest critic combined with the theoretically more powerful search algorithm yields further improvements. Fourth, an ablation on K (the number of tactics sampled per expansion) would reveal whether the choice of 8 is near-optimal or whether larger branching factors would compensate for weaker critics. Fifth, performance on miniF2F-valid — the paper uses the validation set for checkpoint selection but never reports validation accuracy, making it impossible to assess overfitting or calibration. Sixth, breakdown by problem source or difficulty within miniF2F (e.g., separating AMC problems from IMO problems) would show where the gains concentrate and whether the distance critic helps uniformly or primarily on harder subsets.

Generalizability concerns. All experiments use a single benchmark (miniF2F) with a single base model (HUNYUAN 7B) and a single proof assistant (LEAN4). Whether the distance critic's benefits transfer to other formal systems (Isabelle, Coq), other benchmarks (ProofNet, FIMO), or other base model families is entirely untested. The paper's claims are valid for the specific configuration tested but cannot be assumed to generalize. Additionally, the miniF2F test set of 244 problems is small by modern ML benchmarking standards, making the reported accuracies sensitive to individual problem difficulty. A 2.5-point improvement represents roughly 6 problems — moving these 6 problems from "unsolved" to "solved" could depend on specific implementation details (timeout values, temperature sampling, LEAN version) rather than fundamental algorithmic advances.

Statistical reliability. The paper reports no error bars, confidence intervals, statistical tests, or multiple random seeds. Theorem proving via tree search with sampled tactics is inherently stochastic — different random seeds produce different search trees and potentially different outcomes. On a 244-problem test set, differences of 1–3 points could plausibly arise from seed variation alone. The paper's claim that HunyuanProver "advances" the prior SOTA would be strengthened by reporting variance across multiple runs or by conducting the comparison under controlled conditions (same LEAN version, same hardware, same random seeds where applicable).

6. Limitations and Trade-offs

Limitation 1: The MCTS Implementation Is Incomplete, Preventing Clean Algorithm Comparisons

The assumption or constraint. The paper's adaptation of ηMCTS removes the simulation (rollout) step that is central to standard MCTS:

"Here we remove the step of simulation, leaving it for future work." (Section 3.1)

This means ηMCTS as implemented relies entirely on the learned critic (PRM) for node value estimates, without the Monte Carlo rollouts that typically complement learned value functions in MCTS — providing noisy but unbiased estimates of a node's true value and often compensating for critic errors through averaging.

The consequence. The paper cannot disentangle whether the modest improvement of MCTS+PRM over BFS+DC at v14 (66.39% vs. 65.57%, a 0.82-point gap in Table 2) reflects a genuine advantage of MCTS's exploration mechanism (UCB selection, dynamic expansion budgets) or whether the removal of simulation is crippling MCTS and a full implementation would perform substantially better. Worse, the paper never tests (BFS, PRM) — that is, BFS with the same PRM critic used in MCTS — so we cannot determine whether MCTS provides any value beyond BFS when the critic is held constant. The 1.22-point gain of MCTS+PRM over BFS+PC at v12 (62.29% vs. 61.07%) confounds critic quality with search algorithm, since PC is a much weaker critic than PRM. A practitioner deciding between BFS and MCTS receives no actionable evidence from this paper — the only direct comparison (v14, BFS+DC vs. MCTS+PRM) uses different critics, making the algorithm comparison uninterpretable.

What evidence exists in the paper. Table 2 contains exactly three MCTS data points, all with PRM: v12 (62.29%), v14 (66.39%), and the system is not tested at v16 at all ("due to the limitation of time and computation resources"). There is no (MCTS, PC), (MCTS, DC), or (BFS, PRM) configuration. The paper's ablation grid is incomplete in the dimension that matters most for algorithm selection.

Mitigation status. The paper acknowledges the limitation explicitly: "Due to the limitation of time and computation resources, we leave separately examining the effectiveness of MCTS and PRM in future work." This is an honest flag but does not mitigate the limitation within the current paper. The MCTS results should be treated as preliminary and insufficient for drawing conclusions about search algorithm choice.

Limitation 2: Difficulty Estimation Cost Is Completely Unaccounted for and Could Dwarf the Search Budget

The assumption or constraint. The iterative data generation pipeline requires running best-first search with the current prover on all unsolved statements in $D_q$ at each iteration (Equation 1, Section 2.2). $D_q$ contains 20 million LEAN statements. Even if only a fraction of these are attempted in each iteration (the paper reports "more than 20 million tactic-level data is obtained" cumulatively across more than 10 iterations), the total computation expended on unsuccessful proof attempts — which produce no training data but consume search budget — is unmeasured. The iterative framework's cost includes both the successful trajectories (which become training data) and the failed searches (which are discarded). Only the former is reported; the latter is a pure overhead necessary to discover which statements are solvable by the current prover.

The consequence. The true computational cost of producing the 20M+ tactic training examples is substantially higher than what the paper implies by reporting only the successful data volume. Each iteration requires running BFS (with up to 800 search steps, 8 tactics per step, against a LEAN engine with 60-second per-step timeouts) on statements that may be far beyond the current prover's capability, consuming the full budget and yielding nothing. For a practitioner attempting to replicate the iterative data generation pipeline, this hidden cost is the dominant economic factor — it determines whether the approach is feasible on their compute budget. The paper's framing of "more than 20 million tactic-level data is obtained" obscures that perhaps hundreds of millions or billions of tactic evaluations may have been required to discover those 20M successful examples. Without accounting for this, the method's efficiency relative to alternatives (e.g., using human-written proofs, or reinforcement learning approaches that learn from failures) cannot be assessed.

What evidence exists in the paper. The paper reports only the output of the data generation pipeline (20M+ tactics, Figure 3 showing total fine-tuning tokens growing to ~4.25B) — never the input cost. The BFS budget used during data generation (the #Pass × #Beam × #Iteration for the generation runs) is not stated, nor is the solve rate (what fraction of attempted statements yielded proofs) at each iteration. The autoformalization pipeline's cost — running inference on 30M problems with 8 samples each to produce 240M candidates, then filtering to 20M — is similarly unreported. Neither GPU-hours, nor LEAN engine CPU-hours, nor total tactic evaluations during data generation appear anywhere in the paper.

Mitigation status. The paper does not acknowledge this as a limitation. The iterative data generation is described entirely in terms of its output, with the implicit assumption that the cost is acceptable. No future work is suggested for reducing the cost of data generation or for learning from negative results (failed proof attempts). This is the most significant omission for practitioners considering adopting the method.

Limitation 3: Single Benchmark and Single Model Family — No Evidence of Generalization

The assumption or constraint. Every result in the paper is on a single benchmark (miniF2F, 244 test problems) using a single base model (HUNYUAN 7B) and a single proof assistant (LEAN4). The paper makes no attempt to evaluate on other theorem-proving benchmarks (FIMO, ProofNet, miniF2F-valid reported separately from checkpoint selection), other model families, or other formal systems. The authors state they "believe this model is representative of the capabilities of many contemporary LLMs" (implied by the choice of a 7B model class that matches competitors), but this belief is not tested.

The consequence. Three distinct generalizability questions are unresolved. First, benchmark generalizability: miniF2F focuses on algebra and number theory problems at high-school to Olympiad level. Whether the distance critic provides value on other mathematical domains (analysis, topology, category theory) or on benchmarks with different difficulty distributions is unknown. The paper's finding that the distance critic helps specifically with deeper proofs (Figure 4, proofs of length >9) suggests it might not help on benchmarks dominated by shallow proofs — a regime where the coarse PRM signal would suffice. Second, model generalizability: the HUNYUAN 7B architecture and pretraining may have specific properties (e.g., its calibration of token probabilities for policy confidence, its LEAN syntax understanding) that affect critic training and search behavior. A different base model might produce different quality PRM training data (affecting critic reliability) or different search tree structures (affecting where the distance critic provides value). Third, proof system generalizability: LEAN4 has specific tactical conventions and automation levels. In a system with different tactic granularity (e.g., Isabelle's more automated proof methods, or Coq's different tactic language), the distance critic's 8-level binary tree (representing distances up to 64) might need different calibration — the average proof length and the variance in proof length could differ substantially, making the chosen tree depth either too coarse or too fine.

What evidence exists in the paper. None. The paper contains no cross-benchmark, cross-model, or cross-system experiments. The miniF2F test set of 244 problems is the sole evaluation target. The absence is total — this is not a case of insufficient evidence but of zero evidence for generalizability.

Mitigation status. The paper does not acknowledge this as a limitation or suggest multi-benchmark evaluation as future work. This is standard for conference-paper-length technical reports in the theorem-proving domain (prior systems like DeepSeek-Prover and InternLM2.5-StepProver similarly report primarily on miniF2F), but a practitioner cannot assume the approach transfers to their specific domain, model, or proof system without additional validation.

Limitation 4: No Statistical Reliability Assessment on a 244-Problem Test Set

The assumption or constraint. The miniF2F test set contains 244 problems. The paper reports single-point accuracy estimates (e.g., 68.4%) with no error bars, confidence intervals, significance tests, or multiple random seeds. Theorem-proving via tree search with sampled tactics is inherently stochastic — the policy model's temperature sampling, the order in which nodes are selected and expanded, and the LEAN engine's behavior (which can vary subtly with timing) all introduce randomness. Two runs with identical configurations but different random seeds could produce different sets of solved problems.

The consequence. The headline comparison — 68.4% vs. 65.9% (InternLM2.5-StepProver), a 2.5-point gap — represents approximately 6 additional solved problems on a 244-problem test set. It is entirely plausible that this difference could arise from seed variation, differences in the LEAN environment (timeout handling, memory limits, package versions), or problem-specific luck rather than a genuine capability improvement. The paper's internal comparisons (e.g., BFS+DC vs. BFS+PC at v16: 68.44% vs. 64.75%, a 3.69-point gap representing ~9 problems) are also vulnerable to this concern. Without variance estimates, a practitioner comparing HunyuanProver to InternLM2.5-StepProver cannot determine whether the reported difference is statistically reliable or practically meaningful. The small test set size amplifies this problem — on larger benchmarks (thousands of problems), 2–3 point differences are more robust; on 244 problems, they are fragile.

What evidence exists in the paper. The paper reports no statistical measures of any kind. Checkpoint selection during fine-tuning uses the miniF2F validation set (244 problems), but validation accuracy is never reported. No ablation is run with multiple seeds. The paper does not report problem-level solve/non-solve patterns that would allow McNemar's test or other paired statistical comparisons. The cost notation for BFS (#Pass × #Beam × #Iteration) implies multiple passes, but whether the reported accuracy is the best-of-N across passes (which would inflate performance relative to single-pass evaluation) or an average is not explicitly stated.

Mitigation status. The paper does not acknowledge this limitation or discuss statistical reliability. Reporting variance across multiple search runs (e.g., standard deviation across 3–5 random seeds) or providing problem-level solve data for the main comparisons would substantially strengthen confidence in the results. The absence is particularly notable because the paper's central claim — advancing SOTA by 2.5 points — rests entirely on a point estimate from a single evaluation run on a small test set.

Limitation 5: The 4× Search Budget Reduction Claim Does Not Account for Critic Training and Inference Cost

The assumption or constraint. Table 1 highlights that HunyuanProver v16+BFS+DC uses a search budget of 600 × 8 × 400 compared to InternLM2.5-StepProver+BFS+CG's 256 × 32 × 600. The paper's narrative frames this as achieving better accuracy "using less search budget." However, this comparison accounts only for the policy model's inference cost during search — it excludes the cost of (1) training the distance critic (requiring generating search trees, labeling nodes with distances, and fine-tuning an LLM+MLP model), (2) training the PRM (similarly requiring tree generation and LM+MLP fine-tuning), and (3) running the critic at inference time during search (the distance critic must be evaluated on every active node to produce scores for selection, and the PRM — if used — must be evaluated on every node for UCB and importance score computation).

The consequence. The true cost of HunyuanProver's search is the policy model inference cost plus the critic inference cost. If the distance critic is the same scale as the policy model (an LLM with an MLP head, as described in Section 3.2), then evaluating the critic on a state costs approximately as much as generating a single tactic with the policy. In BFS with K = 8 tactics per expansion, every node expansion involves 1 critic evaluation (to score the node when it enters the active set) and 8 policy calls (to sample tactics). The critic adds roughly 12.5% overhead to the per-expansion inference cost. In MCTS with dynamic expansion budgets, nodes may be scored multiple times as they are revisited, potentially increasing critic overhead. While this overhead is modest relative to the policy cost, it means the search budget comparison in Table 1 understates HunyuanProver's true inference cost relative to a system using policy confidence as the critic (which adds zero overhead, since policy confidence is derived from the policy's own output probabilities). The 4× efficiency advantage implied by the budget numbers is therefore slightly optimistic — the true efficiency gain is smaller once critic inference is accounted for. More importantly, the training cost of the critics is entirely excluded from all comparisons, making the method's total computational cost (training + inference) unknown relative to baselines that may use simpler or no critic models.

What evidence exists in the paper. The paper provides no estimates of critic training cost (GPU-hours, data volume, number of training steps), critic inference cost (model size, latency per evaluation), or the fraction of total search time spent in critic evaluation versus policy sampling. The PRM and distance critic architectures are described (LLM + MLP head, scalar prediction at last token), which implies costs similar to a forward pass of the policy model, but this is not quantified. The critic training data construction is described procedurally (generate search trees, label nodes with ±1 or distances) but the scale of this data (number of trees, number of nodes, total tokens) is unreported.

Mitigation status. The paper does not acknowledge this as a limitation. The cost accounting focuses exclusively on the policy model's generation budget, treating the critic as free. For a practitioner implementing the system, the critic's training cost matters because it must be incurred before any inference-time benefit is realized — if training the distance critic requires generating search trees for thousands of statements, that upfront cost may exceed the search budget saved on the benchmark problems. The paper's implicit claim that critic-guided search is "more efficient" is directionally supported but quantitatively incomplete without critic cost accounting.

Limitation 6: Hard Problems Remain Fundamentally Unsolved — The Method Amplifies Existing Capability but Does Not Create It

The assumption or constraint. The iterative data generation framework (Section 2.2) can only generate training data for statements the current prover can already solve — it is a pure exploitation mechanism. At each iteration $t$, the prover $\pi_{t-1}$ attempts to prove unsolved statements from $D_q$. Statements that $\pi_{t-1}$ cannot prove within the search budget remain unsolved and carry forward to the next iteration. If a statement requires a proof technique or mathematical insight that the prover has not learned (because no training data exemplifies it), the prover will never generate a proof for it, and it will never enter the training set — creating a capability ceiling that the iterative loop cannot break through.

The consequence. The prover's performance is bounded by the capabilities present in its initial training data (mathlib4, ~50K theorems) plus whatever capabilities can be discovered through random exploration during search. Complex proof techniques that require creative insight — especially those that differ substantially from patterns in mathlib4 — may never be discovered, regardless of how many iterations are run. The paper's own results are consistent with this: while miniF2F-test accuracy climbs from ~52% (v2) to 68.4% (v16), roughly 32% of problems remain unsolved. The paper provides no analysis of which problems remain unsolved and whether they share characteristics (e.g., requiring specific proof techniques, being drawn from particular competition sources, or having longer average proof lengths). If the unsolved problems represent a qualitatively different difficulty class — problems that require genuinely novel reasoning rather than more effective search — then further iterations of the current framework will not solve them. The FLOPs-matched comparison to pretraining (which the reference example paper performed to show test-time compute cannot substitute for fundamentally missing capabilities) is absent here — the paper never tests whether a larger base model or a model pretrained on more formal mathematics would solve the remaining 32%.

What evidence exists in the paper. The paper does not analyze the unsolved problems. Figure 3 shows that accuracy plateaus around v12 for BFS+PC, suggesting diminishing returns from iterative training alone, though data curation and the distance critic push the ceiling higher. Figure 4 shows that the distance critic helps with deeper proofs (length >9), but the absolute number of deep proofs solved is modest (the bar heights show fewer than 20 theorems in the >9-step category for both BFS+PC and BFS+DC). The paper does not report a breakdown by problem difficulty within miniF2F (e.g., AMC vs. AIME vs. IMO problems), which would reveal whether gains concentrate on easier subsets while hard subsets remain flat.

Mitigation status. The paper does not discuss this limitation or propose mechanisms for breaking the capability ceiling. The diversity enhancement methods (converting unfinished states to new statements, targeting Olympiad problems) are attempts to broaden the training distribution within the existing framework, but they cannot introduce genuinely novel proof techniques — they can only recombine existing capabilities in new contexts. The paper's future work mentions "better curation for prover training data" and "other more cost-efficient tree search algorithms such as Q*" but does not address the fundamental exploration problem. A practitioner facing difficult theorems outside the training distribution should not expect the current iterative RFT framework alone to solve them — additional mechanisms (e.g., incorporating human proofs, using stronger base models, or reinforcement learning with exploration bonuses) would likely be necessary.

7. Implications and Future Directions

How This Work Changes the Landscape

This paper does not introduce a new paradigm for automated theorem proving — it refines and integrates existing techniques (autoformalization, expert iteration, critic-guided tree search) into a system that achieves SOTA through careful engineering and two specific innovations: the distance critic architecture and the empirical finding that data curation (removing easy examples) becomes critical after scale saturation. The conceptual shift it contributes is therefore diagnostic rather than paradigmatic: it identifies which components of the theorem-proving pipeline are currently binding constraints and provides evidence that certain previously underappreciated factors — critic granularity beyond binary reward, and data difficulty composition after sufficient volume — deserve first-class attention in future system design.

The primary reframing: critics should predict structure, not just outcomes. Prior to this work, the dominant paradigm for search guidance in theorem proving (and LLM reasoning more broadly) was the process reward model — a learned binary or continuous value function predicting whether a state can lead to success (Wang et al., 2024c; Math-Shepherd; the PRM in this very paper). The distance critic challenges this paradigm not by replacing PRMs but by demonstrating that predicting a richer structural property of the search space — distance to goal — provides strictly more informative guidance than binary success prediction, and that this richer prediction is trainable from exactly the same automatically-labeled data. The 3.69-point gain from policy confidence to distance critic at v16 (Table 2, 64.75% → 68.44%), compared to the modest 1.22-point gain from policy confidence to PRM+MCTS at v12 (61.07% → 62.29%), suggests that the type of signal matters at least as much as whether the signal is learned at all.

This reframing has implications beyond theorem proving. In any domain where tree search or planning is guided by learned critics — code generation, task planning, mathematical reasoning, game playing — the paper's message is: don't just predict whether a state is good; predict how much work remains, and design your prediction architecture so that errors at fine granularity don't corrupt coarser judgments. The balanced binary tree representation is a specific instantiation of this principle, but the general lesson is that critic design should reflect the search algorithm's information needs: BFS, which commits to a greedy node ordering and never revisits decisions, benefits disproportionately from fine-grained distance estimates because getting the ordering right the first time is critical. MCTS, which revisits nodes and dynamically reallocates budget, may tolerate coarser critics because its exploration mechanism compensates for early ordering errors. This interaction between critic granularity and search algorithm mechanics is not fully tested in the paper (MCTS+DC is missing from Table 2), but the conceptual framework is established.

The data curation finding challenges a core assumption of iterative self-improvement. The observation that removing easy training data after iteration v12 improves performance (Figure 3) contradicts the implicit assumption driving most expert-iteration systems (DeepSeek-Prover, InternLM2.5-StepProver, STaR, ReST) — that more successful trajectories are always better, and that the training distribution should grow monotonically. The paper shows that this assumption fails after sufficient data volume: easy proofs from early iterations, when the prover was weak, create a distributional skew toward simple proof patterns that eventually caps performance on harder benchmarks. This finding has immediate implications for any system that iteratively generates and trains on its own outputs:

• It makes data curation a first-class research problem in iterative self-improvement, not an afterthought. Future systems should monitor the difficulty distribution of their training data across iterations and potentially prune or reweight examples from earlier, weaker policies.
• It suggests that iterative self-improvement may have an inherent tension between exploration (generating training data for hard problems by solving them, which requires a strong policy) and exploitation (training on all accumulated data, which biases the policy toward the easier problems that dominate early iterations). The pruning strategy is a post-hoc correction for this tension, but more principled approaches — such as weighting training examples by the policy version that generated them, or using a fixed-size replay buffer with prioritized sampling — could be developed.
• It partially explains why some iterative self-improvement systems plateau: they may be drowning in their own early successes. The paper does not claim this is universal, but the empirical result is clear enough that practitioners should test whether pruning easy data helps in their domain.

The paper resolves a latent tension in how critic guidance should be evaluated. Prior work on critic-guided theorem proving (Lean-STaR, InternLM2.5-StepProver) treated critic guidance as a binary property — a system either has "critic guidance" (CG) or doesn't. This paper's ablation (Table 2) demonstrates that the type of critic matters enormously: policy confidence, PRM, and distance critic produce progressively better results in BFS (62.70% → not tested → 65.57% at v14; 64.75% → not tested → 68.44% at v16). This shifts the research question from "should we use critic guidance?" (settled: yes) to "what information should the critic predict, and how should that information be represented for the specific search algorithm being used?" — a more nuanced and productive framing.

Research directions that become more attractive. The paper's findings make several lines of inquiry more promising than they appeared before:

• Learned critics that predict structured properties of search trees (distance, branching factor, expected subtree size, proof complexity) rather than just success/failure. The distance critic provides a template: identify a useful structural property, design a hierarchical representation that mitigates data sparsity, and train from automatically-labeled data.
• Dynamic data curation in iterative training loops, where the training distribution is actively managed across iterations to maintain an appropriate difficulty mix — potentially using the critic itself to estimate example difficulty and filter accordingly.
• Critic-search co-design, where critic architecture and search algorithm are jointly optimized rather than treated as independent components. The paper's suggestion that MCTS tolerates coarser critics while BFS benefits from fine-grained ones implies that the optimal critic for one search algorithm may not be optimal for another.

Research directions that become less attractive. Conversely, the paper's results suggest that some directions may have diminishing returns:

• Pure data scaling without curation hits a ceiling (Figure 3, v8–v12 plateau). Simply generating more training data from the same iterative process, without managing the difficulty distribution, is unlikely to push performance substantially further.
• More sophisticated search algorithms without better critics may provide limited gains. The modest improvement of MCTS+PRM over BFS+DC at v14 (0.82 points, Table 2) — even with MCTS's theoretically appealing exploration mechanism — suggests that critic quality is the binding constraint, not search algorithm sophistication. The paper's finding that lookahead-like simulation in MCTS was removed without catastrophic performance loss (MCTS+PRM still achieves 66.39%) further supports this: the critic carries the weight.
• Simple critic architectures (binary PRMs, policy confidence) are clearly dominated by more informative critics when data is available. Future work should invest in richer critic signals rather than refining binary PRM training.

What this work does NOT change. The paper does not challenge the fundamental architecture of LLM-based theorem proving (interactive step-by-step tactic generation with LEAN verification), nor does it propose a new training paradigm (RFT remains the learning algorithm). It does not demonstrate that test-time compute can substitute for pretraining scale (the paper includes no FLOPs-matched pretraining comparison, unlike the reference example). It does not provide a theoretical framework for why the distance critic works — the binary tree representation is empirically motivated but not theoretically justified. And it leaves the hardest problems unsolved (roughly 32% of miniF2F-test remains unproven, with no analysis of what makes these problems hard), meaning the capability ceiling of the current approach is unexplored.

Follow-Up Research This Work Enables

1. Controlled ablation of critic granularity: binary PRM vs. scalar distance vs. tree-structured distance, all in BFS, at matched training data. The paper shows that the distance critic (tree-structured) substantially outperforms policy confidence (untrained) in BFS, but never tests BFS with the PRM (binary trained critic) as a standalone critic. The critical missing experiment is: BFS+PRM at v16 versus BFS+DC at v16, with both critics trained on the same search trees and evaluated at the same search budget. This would isolate whether the distance critic's advantage comes from (a) having any learned signal beyond policy confidence, (b) having distance information specifically, or (c) having the hierarchical tree representation of distance. A strong follow-up would train three critics from identical data: (i) a binary PRM predicting ±1 success/failure, (ii) a scalar regression model predicting raw distance as a continuous value, and (iii) the tree-structured distance critic from the paper — then compare all three in BFS at multiple search budgets (16, 64, 256, 800 iterations). The prediction: the binary PRM should substantially outperform policy confidence (confirming that any learned signal helps), the scalar distance model should outperform the binary PRM (confirming that distance information is useful beyond mere success prediction), and the tree-structured model should outperform the scalar model at low training data volumes (confirming that hierarchical representation mitigates data sparsity) with the gap narrowing as training data increases. This experiment would decompose the distance critic's 3.69-point gain into its component factors and provide actionable guidance for critic design in other domains.

2. Dynamic difficulty-based data curation during iterative training, with a held-out "hard problem" probe set. The paper's post-hoc data curation (removing easy examples after v12) was applied once based on observing a plateau. A principled version would actively manage the training distribution throughout the iterative process, using the critic model to estimate each example's difficulty (e.g., predicted distance to proof) and constructing training batches that oversample medium-to-hard examples while maintaining a minimum proportion of easy examples for stability. The experiment: run the same 16-iteration data generation pipeline with the HUNYUAN 7B base model, but at each iteration, use the current distance critic to score all accumulated training examples by estimated difficulty, and construct the RFT training set by stratified sampling from difficulty quintiles — e.g., sample 10% from the easiest quintile, 20% from the second, 25% from the middle, 25% from the fourth, and 20% from the hardest. Compare against the paper's approach (train on all data until plateau, then prune) on miniF2F-test. Additionally, maintain a held-out probe set of 50-100 hard problems (e.g., IMO-level statements from miniF2F that were never solved during training) and track whether the dynamically curated training improves solve rates on these probes — testing whether better data management during training translates to genuinely novel capability gains rather than just improved efficiency on problems the model could already solve.

3. Extending the distance critic to multi-metric guidance: simultaneously predicting distance, proof complexity, and branch quality. The distance critic predicts a single integer (remaining steps). But search could benefit from multiple guidance signals: (a) estimated remaining steps (when to prefer shallower branches), (b) estimated branching factor (how many valid tactics exist from this state — prefer states with fewer options to reduce search), and (c) a confidence score (how certain the distance prediction is — prefer states with low predictive uncertainty to avoid dead ends). These could be predicted jointly using a shared representation with multiple output heads, or through a tree-structured representation where each metric has its own hierarchical decomposition. The experiment: train a multi-metric critic on the same search tree data used for the paper's distance critic, with the three heads described above. During BFS, compute a composite score that combines the three metrics (e.g., lower distance is better, lower branching factor is better, higher confidence is better). Compare against the single-metric distance critic at v16 on miniF2F-test, and analyze which metrics contribute most to the gain — the hypothesis being that branching factor information helps BFS avoid states with many valid but unproductive tactics (common in intermediate proof states with many hypotheses), and confidence information helps avoid states where the distance estimate is unreliable (potentially due to the state being dissimilar from training examples). If the multi-metric critic underperforms the single-metric distance critic due to training difficulties (multiple objectives competing), that would be a valuable negative result showing that richer critic signals require more careful training.

4. Testing the distance critic on code generation and multi-step reasoning benchmarks to assess domain generality. The paper's distance critic is motivated by data sparsity in theorem proving, but the same problem — distinguishing states that are 2 steps from completion versus 20 steps while training from automatically-labeled data — arises in code generation (predicting remaining lines/tokens to complete a function), multi-step QA (predicting remaining reasoning steps), and task planning (predicting remaining actions to goal). A domain-transfer experiment would: (a) take a SOTA code generation model (e.g., CodeLlama 7B, for comparability with HUNYUAN 7B), (b) generate search trees on a code synthesis benchmark like HumanEval or MBPP by sampling partial programs and checking against test cases (analogous to LEAN verification), (c) train a distance critic using the same 8-level binary tree representation to predict remaining lines of code to a passing solution, (d) use this critic to guide best-first search over partial programs, and (e) compare against policy-confidence-guided BFS and against a PRM trained on binary (passes tests / doesn't pass tests) labels. The key question: does the distance critic provide gains comparable to the 3.69 points seen in theorem proving, or is the benefit domain-specific? If the gain transfers, it suggests the distance critic is a general technique for search problems with verifiable outcomes and variable-length solutions. If it doesn't transfer (e.g., because code generation states have different structure, or because test-case verification is noisier than LEAN verification), that would reveal boundary conditions on when hierarchical distance prediction helps — a valuable negative result.

5. Combining the distance critic with MCTS (MCTS+DC) to test whether the strongest critic combined with the theoretically more powerful search algorithm yields super-additive gains. The paper tests MCTS only with PRM and BFS only with DC — the natural combination of MCTS with the distance critic is missing. The experiment would run ηMCTS (with the simulation step still removed, for comparability) using the distance critic for both UCB exploitation scores and importance score computation (Equation 4), at v16 on miniF2F-test. The hypothesis: MCTS+DC should outperform BFS+DC because MCTS's dynamic budget allocation (giving more expansion budget to nodes with high importance scores) amplifies the distance critic's ability to distinguish promising states — a state predicted to be 3 steps from completion might receive substantially more expansion budget than a state predicted to be 40 steps away, and MCTS's revisitation mechanism could correct early misjudgments if initial distance predictions are noisy. If MCTS+DC doesn't outperform BFS+DC, that would be a striking result suggesting either that the distance critic is so reliable that BFS's one-shot ordering is sufficient (revisitation adds no value), or that the paper's MCTS implementation (missing simulation, simplified from Tian et al., 2024) is fundamentally limited. If MCTS+DC does outperform, it opens the path to cost-controlled comparisons: at what search budget does MCTS's additional overhead (critic evaluations on revisited nodes, importance score computation) pay off relative to BFS's simpler approach?

6. Analyzing the 32% of miniF2F problems that remain unsolved to diagnose the capability ceiling. The paper solves 68.4% of miniF2F-test — 167 of 244 problems — but provides no analysis of the 77 unsolved problems. A diagnostic follow-up would categorize these problems by: (a) problem source (AMC vs. AIME vs. IMO — does the system struggle specifically with Olympiad-level problems?), (b) mathematical domain (algebra vs. number theory vs. other — does the training data skew toward certain domains?), (c) proof length of known human proofs (are unsolved problems those requiring unusually long or complex proofs?), and (d) whether the prover partially solves them — does BFS make progress (reducing the number of goals, applying relevant tactics) before exhausting its budget, or does it fail at the first step? Additionally, test whether a substantially larger search budget (e.g., 4800 iterations instead of 800) solves any of these problems — if increasing the budget by 6× yields no new solutions, the bottleneck is likely prover capability rather than search inadequacy, and future work should focus on training data diversity (incorporating human proofs, using larger base models) rather than search improvements. This analysis would transform the "68.4%" headline into actionable guidance for where to invest effort to reach 75% or 80%.

Practical Applications and Downstream Use Cases

1. Automated formalization of existing informal mathematical corpora at scale. The autoformalization pipeline (30M problems → 20M LEAN statements, Section 2.1) demonstrates that a fine-tuned 7B model can convert natural language mathematics into formal LEAN statements with sufficient quality to fuel prover training. For organizations with large repositories of informal mathematical content — textbook publishers, online learning platforms (Khan Academy, Brilliant, Art of Problem Solving), or mathematical competition archives (IMO Shortlist, national olympiads) — this pipeline offers a concrete path to building machine-verifiable formal versions of their problem libraries. The specific benefit: converting 30M informal problems to 20M filtered formal statements required only 260K training pairs for the autoformalizer (from Lean Workbook and MMA), meaning the upfront annotation cost is modest (~260K aligned pairs, which could be produced by a small team of LEAN-proficient mathematicians over weeks to months) and the inference cost scales linearly. A platform like Art of Problem Solving, which has archives of tens of thousands of competition problems with solutions, could autoformalize their entire problem bank, enabling formal verification of student-submitted proofs — a capability that currently requires human graders and is limited to informal correctness checking.

2. Critic-guided proof search for formal verification of software and hardware properties. While the paper focuses on mathematical theorem proving, the same architecture — a policy model proposing proof steps, a distance critic guiding best-first search, and a LEAN (or Coq, or Isabelle) engine verifying each step — applies directly to formal verification of program correctness, security properties, and hardware designs. In these domains, the "statements" are verification conditions (e.g., "this sorting function produces a sorted array for all inputs," "this cryptographic protocol preserves confidentiality under adversary model X"), and the "proofs" are interactive tactic sequences. The practical benefit of the distance critic in this setting: formal verification proofs are often long and repetitive (many cases, many invariants), and a critic that can distinguish "2 steps from finishing this subgoal" from "40 steps from finishing" would dramatically reduce the human effort required to guide the prover. Specifically, for a verification engineer working on a large codebase, the distance critic could prioritize which subgoals to focus on next — presenting the engineer with the subgoals closest to completion — and could automatically dispatch shallow subgoals (distance < 3) without human intervention. The 3.69-point improvement from adding the distance critic at v16 (Table 2) on math problems suggests comparable gains are plausible for verification tasks with similar structural properties (variable proof length, many dead ends, sparse training data).

3. Iterative data generation as a cost-efficient alternative to human annotation for formal proof libraries. mathlib4, the largest open-source LEAN4 library, contains roughly 50K theorems with tactics — the product of years of volunteer effort by the mathematical formalization community. The paper's iterative pipeline generates over 20 million tactic-level training examples in more than 10 iterations, starting from the same mathlib4 as the base training set. This represents roughly a 400× amplification of the formal proof corpus with zero additional human annotation (beyond the initial 260K autoformalization training pairs). For the LEAN community specifically, this pipeline could be run on mathlib4's existing theorem statements (which are already formalized but may have only one human-written proof) to automatically discover alternative proofs, shorter proofs, or proofs using different tactics — enriching the library with multiple proof strategies per theorem. The discovered proofs are machine-verified by construction, so they can be added to mathlib4 as additional lemmas. The practical bottleneck is the computational cost of running the iterative pipeline (Section 2.2), which the paper does not quantify — but the economic comparison is between that compute cost and the cost of paying mathematicians to write formal proofs, which is substantially higher per proof. For a funding agency or research lab deciding how to invest in formal mathematics, this paper provides evidence that compute spent on iterative proof generation is a viable substitute for human expert time, at least for problems within the difficulty range that the bootstrap prover can handle.

4. On-demand proof assistance for mathematicians learning or using LEAN. A working mathematician who wants to formalize a new result in LEAN — or a student learning formal proof — typically spends substantial time on routine subgoals (algebraic simplifications, basic inequality chains, standard induction patterns) that are conceptually simple but tactically tedious. A system combining the paper's policy model (fine-tuned on 20M+ tactic examples) with the distance critic could serve as an interactive proof assistant: the human provides the high-level proof strategy (e.g., "use induction on n, then consider cases on parity"), and the system automatically dispatches the routine subgoals, using the distance critic to allocate search budget to subgoals that are close to completion and flagging subgoals where the distance estimate exceeds a threshold (say, >20 steps) for human attention. The specific benefit is productivity: the mathematician focuses on the mathematically interesting parts of the proof while the system handles the parts that are "obvious" but time-consuming to write out in LEAN tactics. The paper's results on proof depths (Figure 4) show that BFS+DC solves more deep proofs (>9 steps) than BFS+PC, suggesting the system could handle moderately complex subgoals autonomously, while the unsolved 32% of miniF2F-test represents problems where human intervention would be needed. A practical deployment would integrate the system into the LEAN4 VS Code extension, with the critic providing real-time "distance to proof" estimates for each open goal.

When to Prefer This Method

The paper does not explicitly frame its contributions as a tradeoff against specific named alternatives — it presents HUNYUANPROVER as a system that achieves SOTA through the combination of data scaling, critic-guided search, and data curation, without articulating decision rules for when to prefer its individual components (distance critic, iterative data generation with curation, autoformalization) over alternative approaches. The comparison against prior systems in Table 1 shows that HUNYUANPROVER achieves higher accuracy than InternLM2.5-StepProver, DeepSeek-Prover-V1.5, and Lean-STaR, but the paper does not analyze why a practitioner would choose one of these alternatives over HUNYUANPROVER under different constraints (e.g., limited compute budget, different problem distributions, different base model availability). The ablation in Table 2 compares critic types and search algorithms within HUNYUANPROVER but does not position these against external alternatives.

The closest the paper comes to articulating a tradeoff is the implicit comparison between policy confidence (zero training cost, weakest guidance), PRM (moderate training cost, improved guidance), and distance critic (similar training cost to PRM, best guidance). However, this comparison is incomplete — the paper never tests BFS+PRM, so a practitioner cannot determine whether the distance critic's architectural complexity (8-level binary tree, special token vocabulary, tuple-based comparison) is worth the implementation effort compared to a simpler PRM. The data curation finding (removing easy data after v12) is a specific empirical result rather than a general decision rule — the paper does not provide criteria for when data curation becomes necessary or which data to remove.

Given the absence of explicit framing from the paper, forcing a generic "decision matrix" would be fabricating analysis the paper does not support. The practical takeaways must be inferred from the experimental results rather than extracted from explicit guidance in the text.