{"id":"f56dd38a-21a6-49e1-b8fd-27a5ad8a75b0","arxiv_id":"2504.19188","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"A hierarchical attention regularizer improves pass@64 on Lean theorem proving benchmarks by about two percentage points, while its proof-complexity reduction is computed on a small subset and is less robust.","lead":"The authors fine-tune a 2.8B language model for Lean4 theorem proving with a new regularizer that makes attention flow mostly upward from context to goal, and report modest pass-rate gains on miniF2F and ProofNet. The pass-rate gain is plausible but is tuned per benchmark split, and the reported proof-complexity reduction is computed on a small subset of jointly solved problems.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The five-level hierarchy is only as good as Algorithm 2's line-based parser, which is never validated; if tokens are misassigned, the attention loss constrains arbitrary structure and the small benchmark gains may be an artifact of the regularizer rather than evidence for hierarchical reasoning.","rationale":"The paper's headline result is a causal claim: the hierarchical attention regularizer improves theorem proving because it aligns attention with the mathematical structure of Lean proofs. That causal story requires Algorithm 2 to be a faithful projection of Lean's semantics onto the five-level hierarchy. The paper never tests this projection. Algorithm 2 is a set of line-based syntactic triggers, but Lean 4 code is not line-structured; a single tactic line can contain nested goals and term-mode expressions, and multi-line declarations are tagged by the last trigger seen. The parser also has no defined behavior for many common constructs, so token-level levels are at best approximate. Since every token's level feeds the flow loss, parser noise becomes model-level noise, and the observed gains are small enough that a mis-specified regularizer could plausibly produce them through generic regularization alone. The ablations in Tables 10-12 show that structural choices do affect results, which makes validating the parser more urgent rather than less. Section 5.3's attention analysis is partly self-confirming: constrained layers are explicitly trained to suppress invalid flows, and the unconstrained evidence rests on a single layer. The per-split hyperparameter selection in Table 9 and the lack of error bars are real secondary concerns about the strength and generality of the empirical claim, but they do not identify the mechanism as precisely as the parser validity question does. If a gold-standard parser comparison shows high fidelity, the central claim survives and the remaining issues still warrant a CONDITIONAL verdict. If not, the gains should be treated as an auxiliary-loss effect rather than evidence for hierarchical reasoning. Thus the reader's CONDITIONAL verdict stands, with parser fidelity as an explicit acceptance condition.","tokens_in":16523,"tokens_out":8256,"duration_ms":92764,"concrete_test":"Sample 200 random LeanDojo Benchmark 4 training proofs. Build a gold-standard level assignment from Lean 4's elaborated syntax/info tree: local context declarations as context, target type as goal, `match`/`cases` branches as case, `def`/`abbrev` type signatures as type, and `instance` declarations as instance. Run Algorithm 2's parser on the raw theorem strings and compute the per-token macro-F1 and the fraction of tokens assigned to each level, including the 'inherit previous level' cases. If macro-F1 is below 0.9 or more than 5% of tokens fall into an unrepresented or ambiguous category, the hand-written parser is not a faithful hierarchy; a subsequent ablation with random or reversed level labels should then be run to confirm whether the reported gains depend on the specific hierarchy at all.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central causal claim is that enforcing the five-level hierarchy context < case < type < instance < goal in Eq. 1 improves proof success and conciseness because the hierarchy matches Lean's mathematical structure. The entire constraint is mediated by Algorithm 2, a hand-written parser that assigns levels using line-level syntactic triggers: a line is goal if it contains ⊢, case if it starts with 'case', type if it contains 'Type' and ':', instance if it contains ':' but not 'Type' or ⊢, otherwise it inherits the previous level. Lean 4 proof states and tactic scripts are nested and multi-line; constructs such as `have`, `let`, `calc`, `match`, `fun` binders, and nested tactic blocks do not fit this scheme, and the parser is never evaluated against any ground-truth structure. Because Eq. 2's flow loss penalizes every attention pair with level(ti) > level(tj) in Algorithm 1's notation, misassigned tokens impose arbitrary constraints on the model's attention. The reported 2.05/1.69 percentage-point pass-rate gains and 23.81/16.50% complexity reductions could therefore be produced by the auxiliary regularization term alone, or by another incidental inductive bias, rather than by the claimed mathematical hierarchy. Section 5.3's attention analysis does not resolve this: in constrained layers, near-zero invalid flow is expected because the loss explicitly enforces it, and the 'unconstrained' evidence comes only from the final layer where αl = 0. Without a validity check of Algorithm 2, the paper's central interpretation is unsupported.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a regularization method for LLM-based Lean theorem proving. It defines a five-level hierarchy (context < case < type < instance < goal) over the tokens of a proof state, assigns levels with a hand-written rule-based parser (Algorithm 2), and adds to the standard cross-entropy loss a flow loss (Eq. 2) that penalizes attention from tokens of higher assigned levels to tokens of lower assigned levels, with layer-wise strength alpha_l = 1 - l/L. The authors fine-tune Pythia-2.8B on LeanDojo Benchmark 4 and evaluate pass@K and proof complexity on miniF2F and ProofNet under best-first search and single-pass sampling. They report consistent pass-rate gains at K=64 (e.g., 29.51% to 31.56% on miniF2F test) and reduced proof complexity (R_avg as low as 0.50 on ProofNet validation), along with ablations on layer-wise adaptation, granularity of the hierarchy, and an explicit-tags baseline.","tokens_in":16867,"tokens_out":10633,"duration_ms":98671,"significance":"The proposed regularizer is simple, model-agnostic, and could in principle be applied to any transformer-based formal prover; if the empirical claims survive scrutiny, the paper would make a useful contribution to the structural-reasoning literature. The manuscript is also transparent about training details, uses external benchmarks (miniF2F, ProofNet) rather than constructing a circular evaluation, and releases code. However, the central evidence is currently weakened by (i) per-benchmark selection of training hyperparameters, (ii) an unvalidated parser that is load-bearing for the method, (iii) an attention analysis that is partially circular, and (iv) proof-complexity statistics computed over a small and unquantified subset of proofs. The pass-rate gains are modest (1-2 percentage points at K=64) and are reported from a single seed without error bars. For these reasons the contribution is plausible but not yet established.","major_comments":[{"comment":"The hyperparameters λ and L reported in Table 9 are chosen separately for each of the four evaluation splits (miniF2F test, miniF2F valid, ProofNet test, ProofNet valid). Because λ and L are training hyperparameters, this means the reported pass-rate and complexity numbers are not produced by a single model or a single configuration; they are the result of per-benchmark post-hoc selection on the test sets. This is a load-bearing issue for the main claim, since the headline gains (2.05 and 1.69 percentage points) could in principle be an artifact of selecting the best configuration for each benchmark. The paper should either select λ and L once on a validation set (and report the resulting test numbers), or run a proper nested selection procedure and report the variance across configurations. Please also state explicitly whether the BFS and SPS results for a given row in Table 9 come from the same trained model.","section":"§5.1, Appendix A.1, Table 9"},{"comment":"The entire hierarchy is mediated by the hand-written parser in Algorithm 2, yet the parser is never validated against any ground-truth structural annotation. The line-based rules (a line is 'goal' if it contains ⊢, 'case' if it starts with 'case', 'type' if it contains 'Type' and ':', 'instance' if it contains ':' but not 'Type' or ⊢, otherwise inherit the previous level) cannot correctly capture the nested structure of Lean 4 proofs, which contain `have`, `let`, `calc`, `match`, `fun` binders, and nested tactic blocks. Since Eq. (2) penalizes every pair with level(t_i) > level(t_j), any misassignment is not a harmless approximation but an arbitrary constraint on the attention pattern. The paper should (i) evaluate parser accuracy on a sample of annotated Lean states, (ii) report the distribution of assigned levels and failure modes, and (iii) include a control experiment with randomly permuted levels to show that the specific hierarchy, rather than any level-based regularizer, is responsible for the gains.","section":"§4.1, Algorithm 2"},{"comment":"The attention analysis does not support the claim that the model has 'internalized' the hierarchy. In constrained layers (α_l ≠ 0), the near-zero invalid flows are a direct consequence of Eq. (2), since the loss explicitly penalizes those flows during training; observing them after training is therefore circular. The only unconstrained layer is the final layer, because α_l = 1 - l/L, so the right panel of Figure 3 reports a single layer, and the preservation of the pattern there could be a boundary effect rather than evidence of internalization. The paper should report per-layer attention statistics for all layers and compare against a control model trained with the same loss but with random or inverted level assignments; this is the minimal experiment that would isolate the effect of the hierarchy.","section":"§5.3, Figure 3"},{"comment":"The complexity metric is computed only over the subset of theorems for which both methods succeed with different proof lengths, which the table reports as 'Diff.' Rows like 8.11% (miniF2F test, K=64, BFS) mean that the claimed complexity reduction rests on a small, unquantified set of proofs; with a test set of about 244 problems, this could be on the order of a handful of examples. Moreover, the text states that 'the average proof length' drops from 2.10 to 1.60, which conflates the restricted subset with all common successes. Please report the number of proofs in T_com, the distribution of length differences, the mean and median complexity over all common successes (not only those with different lengths), and a confidence interval or significance test for the reduction.","section":"§5.2, Eq. (5)"}],"minor_comments":[{"comment":"The definition of attention direction is ambiguous. The paper says att_l(t_i,t_j) is 'attention score from t_i to t_j' and then 'how much t_i will affect embedding of t_j', while the bullets in §1 say 'Tokens at higher levels can access information from the same level or lower levels'. The mask in Algorithm 1 allows pairs with level(t_i) ≤ level(t_j), which is a lower-to-higher flow. Please clarify which of the two tokens is the query and which is the key, and align the verbal description with the implementation.","section":"§3.2, Algorithm 1"},{"comment":"Please state whether each row of Table 9 corresponds to a separately trained model and whether the same checkpoints were used for the best-first-search and single-pass-sampling evaluations; otherwise the reader cannot tell how many models the comparisons involve.","section":"Table 9, §5.1"},{"comment":"The definition of T_com is inconsistent: 'successfully proved by both methods with different proof lengths' appears before Eq. (4), while Eq. (5) uses T_com without restating the restriction. Please define it in one place and use a distinct symbol for the full set of common successes.","section":"Eq. (5) and surrounding text"},{"comment":"There is a placeholder '?' citation near 'Liu et al., 2023', and the reference to Kovács and Voronkov contains a stray space ('V oronkov'). Please fix these.","section":"Related Work"},{"comment":"The y-axis is said to combine attention percentages for tokens serving as source and target; this makes the 'invalid flow' percentages hard to interpret. Please plot source and target roles separately or explain the aggregation.","section":"Figure 3"},{"comment":"The definitions of N, S, and K are stated twice with different wording ('within N expansions' vs 'within K = N×S'), which is confusing; also for single-pass sampling, K=N since S=1. Please standardize the notation.","section":"Appendix A.2"}],"recommendation":"major_revision","confidential_remarks":"The strongest concern is the per-split hyperparameter selection in Table 9; in a field where test-set tuning is often hard to detect, this needs to be made absolutely explicit and, ideally, replaced by a validation-only selection. I would not recommend acceptance before this is addressed, but I do not see it as an irreparable flaw. The parser validation can be done with auxiliary Lean tooling and would substantially increase confidence."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: the paper reports a plausible small gain from an attention-flow regularizer on two Lean benchmarks, and the training/evaluation setup is explicit enough to re-implement. But the central interpretation — that the gains come from matching the true hierarchy of Lean proofs — is not supported, because the parser that assigns levels is never validated, and the hyperparameters are selected per split.\n\nWhat is new: the five-level hierarchy (context < case < type < instance < goal) plus a flow loss is a new combination. The ingredients are standard (rule-based parsing, attention masking, a regularizer), but nobody seems to have tried exactly this for LLM theorem proving. The paper also runs useful ablations: a coarse-grained hierarchy, a layer-wise adaptation schedule, and an explicit-tags baseline. The explicit-tags experiment is a nice negative result — just marking the levels in the input hurts, while steering attention helps. The training details are clear and the code link is provided.\n\nSoft spots, in rough order of severity:\n\n1. The load-bearing assumption is Algorithm 2, a line-based parser. It classifies a line as goal if it contains ⊢, case if it starts with 'case', type or instance by colon patterns, else inherits the previous level. Lean proofs are full of nested tactics, let/have/calc/match, and multi-line constructs that do not fit this scheme. The parser is never checked against any ground truth. If tokens are misassigned, the flow loss is penalizing arbitrary structure. Section 5.3's attention analysis does not rescue this: near-zero invalid flow in constrained layers is exactly what the loss enforces, and the 'unconstrained' evidence comes only from the final layer where α_l = 0. That is not evidence of internalization.\n\n2. Hyperparameter selection. Table 9 chooses λ and L separately for each test/valid split. That is test-set tuning, even if only two hyperparameters are involved. It inflates the reported gains. The authors should pick hyperparameters on one validation split and then run the test split once.\n\n3. No error bars and one random seed. The BFS gains are 1.69–2.05 percentage points; without repeated training runs, these could be noise. The SPS gains are larger (~4.5 pp) but also need repeats to be credible.\n\n4. The complexity claims are overstated in the abstract. Ravg = 0.76 on miniF2F test is computed only over theorems where the two methods' proofs differ, which is 8% of jointly solved problems. The 23.81% reduction is conditional on those differing cases, not an average over all solved proofs. A real effect, but smaller than the abstract suggests.\n\nWho this is for: people fine-tuning theorem-proving LLMs who might try this as a cheap regularizer. It deserves a serious referee, mainly because the setup is transparent and the ablation with explicit tags is informative. The referee should ask for parser validation (e.g., sample checks against Lean's actual elaboration or syntax tree), a single hyperparameter selection protocol, and confidence intervals. I would send it out.","headline":"A transparently specified attention-flow regularizer with modest but consistent benchmark gains, whose central hierarchy claim is undermined by an unvalidated parser and per-split hyperparameter selection.","tokens_in":17382,"tokens_out":3070,"would_cite":false,"duration_ms":31069,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper argues that a soft five-level attention regularizer makes a theorem-proving language model both more successful and more concise on formal benchmarks.","keywords":["hierarchical attention","formal theorem proving","Lean","attention regularization","proof conciseness","miniF2F","ProofNet","language model fine-tuning"],"falsifier":"One decisive check is to repeat the fine-tuning with the same loss and the same data but random or adversarially shuffled level assignments; if pass@64 and proof-length reductions persist under random labels, the five-level hierarchy is not what is doing the work. A second check is to audit the parser: on proofs where the level-assignment algorithm mislabels a line, such as calling a goal-context line a 'type' line, the paper's account predicts those proofs should be where the method helps least or fails.","tokens_in":16316,"feed_emoji":"🧮","tokens_out":9688,"duration_ms":87552,"temperature":0.7,"pith_summary":"The paper tries to establish that a language model fine-tuned for formal theorem proving in Lean reasons better when its attention is softly constrained to follow a five-level information hierarchy: context, case, type, instance, goal. The constraint is imposed by a regularization term that penalizes attention flowing from higher-level tokens to lower-level tokens, with the penalty weakened in deeper layers. On the miniF2F and ProofNet benchmarks, the paper reports that pass@64 under best-first search rises from 29.51% to 31.56% and from 13.56% to 15.25%, while successful proofs become shorter by 23.81% and 16.50% respectively. A sympathetic reader would care because, if true, this offers a lightweight way to inject mathematical structure into theorem-proving models without changing the input format or requiring a specialized architecture.","feed_headline":"Attention hierarchy boosts formal proof success and cuts proof length","feed_subtitle":"Proof success within 64 attempts rises on both benchmarks, and successful proofs get up to 23.81% shorter.","key_machinery":"The central object is the hierarchical flow loss, a regularization term added to the standard next-token cross-entropy loss during fine-tuning. It is driven by a hand-written parser that labels each token with one of five levels, context, case, type, instance, goal, and a binary mask $M_{ij}$ that permits attention only from a token to tokens at the same or lower level. The layer-dependent factor $\\alpha_l = 1 - l/L$ applies strong regularization in early transformer layers and relaxes it in later layers, which the paper argues preserves flexibility for complex proof steps. The loss is what carries the argument: it is the only mechanism through which the hierarchy enters training, and the paper's attention analyses trace its effects through constrained and unconstrained layers.","core_discovery":"The paper's central claim is that alignment between attention and mathematical proof structure is itself a learnable target: a model fine-tuned with a flow loss that suppresses attention from 'higher' to 'lower' hierarchical components will both solve more theorems and solve them more directly. The hierarchy orders tokens as $\\text{context} \\prec \\text{case} \\prec \\text{type} \\prec \\text{instance} \\prec \\text{goal}$, and the loss is $L_{\\text{flow}} = \\frac{1}{|T|} \\sum_{l=1}^{L} \\alpha_l \\sum_{i,j} \\operatorname{ReLU}(\\operatorname{att}_l(t_i,t_j)\\,(1 - M_{ij}))$, with $\\alpha_l = 1 - l/L$ and $M_{ij}=1$ exactly when $\\operatorname{level}(t_i) \\le \\operatorname{level}(t_j)$. The paper shows the constrained attention pattern persists in later layers where the penalty is zero, and reports that explicit level tags in the input hurt while the soft attention guidance helps.","pith_inferences":["If the hierarchy is what causes the gains, the method should transfer to other tactic-based proof assistants whose syntax admits the same level ordering; the paper notes Lean-specific parsing as a limitation, so Coq or Isabelle would be a natural test.","A random-label ablation would separate the hierarchy's content from the mere effect of extra regularization: if shuffled level labels keep the gains, the specific five-level ordering is not the active ingredient.","Shortening successful proofs by roughly a quarter could reduce the cost of proof search in practice, since fewer steps per trajectory means less branching and fewer expansions under the same budget.","The contrast with explicit level tags suggests a general design principle for structured domains: encode structure as a soft constraint during training rather than as a hard annotation in the input."],"forward_implications":["Under best-first search with a budget of 64, the method raises pass@64 on miniF2F test from 29.51% to 31.56% and on ProofNet test from 13.56% to 15.25%.","Successful proofs become more concise: the average complexity ratio falls to 0.76 on miniF2F test and 0.84 on ProofNet test, corresponding to the reported 23.81% and 16.50% reductions.","Under single-pass sampling, the method raises miniF2F test pass@64 from 23.36% to 27.87% and validation from 21.72% to 26.64%, a larger relative gain than under search.","The ablation without layer-wise adaptation still beats the baseline on every benchmark, so the five-level structure itself, not the adaptive schedule, is the core contributor.","Explicitly tagging tokens with their levels in the input hurts performance, suggesting the benefit comes from shaping attention rather than from giving the model structural labels it can read."],"supporting_citations":[{"why":"Supplies the miniF2F benchmark whose test and validation sets define the primary pass@K results.","marker":"(Zheng et al., 2021)"},{"why":"Supplies the ProofNet benchmark used for the second set of pass-rate and complexity results.","marker":"(Azerbayev et al., 2023)"},{"why":"Provides the LLMSTEP baseline whose model, training data, and hyperparameters the comparison reuses.","marker":"(Welleck and Saha, 2023)"},{"why":"Source of the LeanDojo training benchmark used to fine-tune the model.","marker":"(Yang et al., 2024)"},{"why":"Defines the Lean 4 syntax that the level parser's pattern matching relies on.","marker":"(Moura and Ullrich, 2021)"},{"why":"Supplies the 2.8-billion-parameter pretrained model that is fine-tuned in the experiments.","marker":"(Biderman et al., 2023)"}],"fun_headline_variants":["Attention hierarchy yields shorter, more successful proofs","Tune attention to proof structure for better theorem proving","Hierarchical attention cuts proof length, boosts success","Proofs get 23.8% shorter with attention tuned to hierarchy","Structured attention makes formal proofs easier and shorter"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole result rests on the hand-written rule that assigns each token to one of five levels, ordered from context up to goal; if those assignments do not match the real logical structure of Lean proofs, the regularizer is enforcing an arbitrary pattern and the benchmark gains would not show that hierarchical reasoning is the cause.","fun_headline_variants_meta":{"raw":{"variants":["Attention hierarchy yields shorter, more successful proofs","Tune attention to proof structure for better theorem proving","Hierarchical attention cuts proof length, boosts success","Proofs get 23.8% shorter with attention tuned to hierarchy","Structured attention makes formal proofs easier and shorter"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000812,"raw_usage":{"total_tokens":3526,"prompt_tokens":878,"completion_tokens":2648,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":494,"completion_tokens_details":{"reasoning_tokens":2572}},"tokens_in":494,"tokens_out":2648,"duration_ms":18135,"temperature":1.0,"reasoning_tokens":2572,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T05:59:38.859821+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"One decisive check is to repeat the fine-tuning with the same loss and the same data but random or adversarially shuffled level assignments; if pass@64 and proof-length reductions persist under random labels, the five-level hierarchy is not what is doing the work. A second check is to audit the parser: on proofs where the level-assignment algorithm mislabels a line, such as calling a goal-context line a 'type' line, the paper's account predicts those proofs should be where the method helps least or fails.","supporting_citations":[],"review_version":1}