{"id":"cba874a9-b15b-4300-aa2a-4d37766e5a7e","arxiv_id":"2501.13959","paper_version":3,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"A compact BERT retriever for Lean premises, trained with a Lean-specific tokenizer and fine-grained similarity plus re-ranking, outperforms prior retrievers on most splits and lifts MiniF2F pass@1.","lead":"This paper trains a small BERT-style model to help users find the right theorems in the Lean proof assistant, using Mathlib data and a tokenizer built for Lean's formal language. In tests, it retrieves the correct premise more often than existing tools and slightly boosts an automated theorem prover's success on the MiniF2F benchmark.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The Reference Isolated split is compromised: MLM pretraining on all premises, including validation/test premises, means RI does not measure generalization to unseen premises; the 'superior adaptability' claim on RI is not established.","rationale":"The reader's weakest_assumption identifies the same load-bearing concern: MLM pretraining on all premises, including validation/test premises, contaminates the Reference Isolated split. This is the single most important threat to the paper's generalization claim because the RI split is explicitly designed to demonstrate robustness to premises unseen during training, and the paper explicitly invokes this result to claim 'superior adaptability.' The contamination is not hypothetical: §4.1's wording directly includes all premises in the pretraining corpus, and the release of code and model makes the inclusion checkable. The concern is specific and falsifiable: if a retrained model with test premises excluded from pretraining retains its RI advantage, then the current RI result is not inflated; if the advantage shrinks substantially, the generalization claim is overstated. I do not see an equally load-bearing internal inconsistency elsewhere. The computational-load claim in Figure 5 is somewhat loose ('comparable' GFLOPs with reranking versus 'lower' in the abstract), but it does not threaten the main retrieval-accuracy results. The ablations, four-split evaluation, and MiniF2F theorem-proving experiment provide real independent support for the core engineering contribution, which is why the appropriate outcome remains conditional acceptance pending the pretraining-leakage check rather than rejection.","tokens_in":16701,"tokens_out":5085,"duration_ms":55613,"concrete_test":"Retrain the model exactly as in §4.1–§4.2, but restrict the MLM pretraining corpus to premises that appear in the training split only, excluding all validation and test premise declarations; keep contrastive fine-tuning and the RI evaluation unchanged. Then re-run Table 2's RI row. If R@1/R@5 drop materially (e.g., R@1 falls from 7.79 toward the ReProver baseline of 5.05), the RI result is inflated by transductive pretraining, and the 'superior adaptability' claim should be reworded or withdrawn. Also report the same restricted-pretraining RI numbers for RD as a control to separate the pretraining effect from general training dynamics.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's cleanest test of generalization to new premises is the Reference Isolated (RI) split, defined in §4.2 as \"Premises in the validation and test sets will not appear in the training set.\" However, §4.1 states that the MLM pretraining corpus is built by concatenating \"states from the training set and all premises' argument lists and goals from the corpus.\" The phrase \"all premises\" includes validation and test premises. Thus, although those premises are absent from the contrastive fine-tuning labels, their exact textual forms are present during pretraining. Since the premise encoder is initialized from this pretrained BERT, seeing the test premise strings can improve tokenization and embeddings for precisely the items that RI is supposed to hold out, especially for rare or unusual formal tokens. Consequently, the RI results in Table 2 (e.g., R@1 7.79 vs. ReProver 5.05) do not support the §4.2 claim that the model \"exhibits superior adaptability\" to premises never encountered during training. The RD, PL, and PF splits are less affected because they do not hold premises out of fine-tuning, so the broader claim of improved retrieval accuracy on those splits is not undermined. But the RI result, which is the paper's primary evidence for generalization to novel premises, is confounded by transductive pretraining.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a premise retrieval system for Lean/Mathlib formalization. The method consists of a context-free retrieval (CFR) module and a context-aware re-ranking (CAR) module, both built on a small 6-layer BERT encoder with a WordPiece tokenizer trained on formal Lean text; the encoder is MLM pre-trained on a formalized corpus and then fine-tuned with in-batch contrastive learning on state-premise pairs extracted from Mathlib4 v4.10.0. The CFR module uses a fine-grained similarity that separately encodes a premise's arguments and goal, while the CAR module re-ranks the top-k1 candidates with a cross-encoder. Retrieval is evaluated on four splits (Random, Reference Isolated, Proof Length, Premise Frequency) against ReProver, UniXcoder, E5-large, and BGE-m3, with ablations on pre-training, tokenizer, and similarity design. The retriever is also integrated with a ByT5 tactic generator trained independently, yielding 30.74% pass@1 on MiniF2F versus 28.28% for ReProver. Code, a trained model, and a live search engine are released.","tokens_in":17039,"tokens_out":14812,"duration_ms":139072,"significance":"If the central results hold, the paper demonstrates that a compact domain-specific retriever with a formal-language tokenizer can outperform off-the-shelf embedders and the ReProver baseline on Mathlib premise selection at a fraction of the parameter count, and that better retrieval translates into improved proof pass rates on MiniF2F. The paper's strengths include a clean ablation isolating the contributions of pre-training, tokenizer retraining, and the fine-grained similarity, and the release of code, a trained model, and a deployed search engine, which are concrete assets for the Lean community. The primary caveat is that the Reference Isolated split, the only split designed to test generalization to unseen premises, is confounded by MLM pre-training on the full premise corpus, so the 'superior adaptability' claim is not yet established; the RD, PL, and PF retrieval results and the MiniF2F outcome are not directly affected by this issue.","major_comments":[{"comment":"The Reference Isolated (RI) split is the paper's only experimental device for testing generalization to premises unseen during training, and §4.2 uses the RI results to claim that the model 'exhibits superior adaptability' to such premises. This claim is confounded: §4.1 states that the pre-training corpus is built from 'states from the training set and all premises' argument lists and goals from the corpus', where 'all premises' includes the validation and test premises of the RI split, and §3.3 trains the WordPiece tokenizer on the same formalized corpus. The MLM pre-training therefore exposes the model to the exact textual forms of the premises that RI is supposed to hold out, giving the premise encoder (and the CAR module) a transductive advantage over the baselines, none of which are pre-trained on Lean text. Consequently, the RI numbers in Table 2 (e.g., R@1 7.79 vs. ReProver's 5.05) do not establish the claimed generalization to new premises; please re-run the RI experiment with a pre-training corpus and tokenizer restricted to training-set premises, or, failing that, withdraw or substantially scope the 'superior adaptability' claim. The RD, PL, and PF splits are largely unaffected and continue to support the retrieval-accuracy claims.","section":"§4.1 (pre-training corpus); §4.2 (RI split); Table 2."},{"comment":"The comparison against ReProver, the paper's primary baseline, is specified too loosely to verify the central 'outperforms existing baselines' claim. §4.1 first says ReProver 'serves as our primary baseline' and then adds that 'we retrain the model using our dataset and following the setting in (Yang et al., 2024)', and it is not stated whether Table 2, Figure 7, and the MiniF2F pass@1 figures (30.74% vs. 28.28% in §4.5) are obtained with the official ReProver checkpoint or with a retrained ReProver, on which of the four splits, and with which generator configuration. The source of the ReProver MiniF2F figure is not identified, and it differs from the pass@1 reported in the original LeanDojo paper, so a reader cannot tell whether the comparison is apples-to-apples. Please specify the exact ReProver configuration for each table and figure, including the checkpoint, training data, and the tactic generator used in §4.5.","section":"§4.1 (Baselines); §4.5 (MiniF2F results)."}],"minor_comments":[{"comment":"The abstract's claim of maintaining 'a lower computational load' should be scoped: in Figure 5 the CFR-only model has the lowest GFLOPs, but the full system that produces the Table 2 results, with the CAR module active, has GFLOPs comparable to ReProver (134.3M vs. 217.66M parameters). Please qualify the efficiency claim to the configuration actually being discussed.","section":"Abstract; Figure 5."},{"comment":"In Eq. (6), the sigmoid output Pr(s,p) of Eq. (4) is inserted into a softmax-style normalization as if it were a logit or an exponentiated score; this is non-standard, and the loss should be written directly on the logits of Eq. (4) or the notation should be explained.","section":"Eq. (6) in §3.3."},{"comment":"The authors note in §5 that the theorem-proving results 'need further clarification with stronger provers', and §4.5 reports that on the RD test set the proposed retriever performs slightly worse than ReProver in proving despite better retrieval; this tension deserves a more detailed analysis in the main text, and Figure 7 would benefit from multi-seed variance information.","section":"§4.5 and §5."},{"comment":"The paper should define 'corpus', 'training set', and 'pre-training corpus' explicitly at first use, and state whether the pre-training corpus and the tokenizer vocabulary are shared across the four data splits; the current wording of §4.1 and §4.2 makes the RI guarantee ('will not appear in the training set') ambiguous about whether pre-training is included.","section":"§4.1 and §4.2 (terminology)."}],"recommendation":"major_revision","confidential_remarks":"The RI leakage concern raised in the major comments is the main correctness risk and is local and fixable; I would ask the authors to re-run RI with a cleanly held-out pre-training corpus or to scope the claim, and to disclose the exact ReProver configuration since the headline comparison depends on it. I see no citation or novelty concerns; the released search engine and code are genuine strengths. For a journal version, the authors should also address the RD proving-performance tension and add variance reporting."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The one thing to know: this is a solid, honest engineering contribution to premise retrieval for Lean. It beats ReProver on the standard splits with a smaller model, and the authors ship code, a trained model, and a search engine. The one real flaw is that the Reference Isolated split, which is supposed to show generalization to premises never seen during training, is contaminated by the MLM pre-training corpus.\n\nThe paper's core novelty is the combination: a WordPiece tokenizer trained from scratch on Lean formal text, a fine-grained similarity that compares the proof state against a premise's argument list and goal separately, and a cross-encoder re-ranker trained with hard negatives. The ablations in Table 3 and Figure 4 earn their keep—they show all three components matter. The efficiency comparison in Figure 5 is honest: without re-ranking the model is very cheap, with re-ranking it is comparable to ReProver, and the pass@1 on MiniF2F (30.74 vs 28.28) is a small but real gain.\n\nThe soft spots, in order. First, the RI split. Section 4.1 says the pre-training corpus is built from \"all premises' argument lists and goals from the corpus,\" which includes validation and test premises. So the model has already seen the exact text of the held-out premises during MLM pre-training. That makes the RI numbers (R@1 7.79 vs ReProver 5.05) a transductive leak, not a clean test of generalization to new premises. The claim in Section 4.2 that the model \"exhibits superior adaptability\" on RI is therefore not supported. This does not hurt the RD, PL, and PF comparisons, since those splits keep the same premise pool for retrieval, but it removes the paper's best evidence for generalization to novel premises. Second, there are no error bars or across-seed variances anywhere in the main table. The gains are large enough that the core comparison likely survives, but the RI gap is the one place where variance could matter. Third, the theorem-proving integration is honest but mixed: the model does better than ReProver on the high-premise-frequency test sets, slightly worse on RD, and about the same on long proofs. The MiniF2F gain is 2.5 points, which is modest.\n\nWho this is for: anyone working on premise selection, Lean tooling, or retrieval-augmented theorem proving. The deployed search engine is a genuinely useful artifact. This deserves a serious peer review. The RI issue should be fixed by re-running pre-training without test premises, or by removing the RI claims, and the paper should report variance. But the core empirical story is credible.\n\nRecommendation: send it to review.","headline":"Solid premise-retrieval engineering for Lean with credible gains over ReProver, but the Reference Isolated split is contaminated by pre-training on test premises, so the generalization claim does not stand as written.","tokens_in":17514,"tokens_out":2353,"would_cite":true,"duration_ms":23333,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A small, Lean-specific retriever trained on Mathlib outperforms prior baselines and lifts retrieval-augmented theorem proving on MiniF2F from 28.28% to 30.74% pass@1.","keywords":["premise retrieval","Lean theorem proving","formal mathematics","contrastive learning","dense retrieval","re-ranking","BERT","Mathlib"],"falsifier":"Train the same architecture with masked-language-model pre-training restricted to premises from the training split only, then evaluate on the Reference Isolated test set: if Recall@1 falls back to roughly the ReProver level of 5.05%, the paper's generalization claim is not supported; if the gain persists, the claim survives.","tokens_in":16541,"feed_emoji":"🔍","tokens_out":6557,"duration_ms":58752,"temperature":0.7,"pith_summary":"The paper tries to establish that a domain-specific, lightweight premise retriever can outperform larger general-purpose models at Lean theorem proving by learning directly from formal-language data. It trains a compact BERT model from scratch on text extracted from Mathlib, using a tokenizer built for Lean, then retrieves premises by comparing a proof state against the argument list and goal of each theorem separately. A second cross-encoder re-ranks the top candidates using hard negatives from the first stage. On the MiniF2F benchmark, the retrieval-augmented prover built this way reaches a pass@1 rate of 30.74%, versus 28.28% for the ReProver baseline, and the retriever itself is small enough to run on a personal computer. The point of the work is that formal proof text is different enough from natural language that a smaller model trained on it can beat large models fine-tuned on natural-language corpora.","feed_headline":"Lean premise retriever reaches 30.74% pass@1","feed_subtitle":"A 66M-parameter model with a Lean-trained tokenizer beats ReProver's 28.28% on MiniF2F.","key_machinery":"Context-free retrieval plus context-aware re-ranking. The CFR module embeds a Lean proof state and each premise independently and computes similarity as the cosine similarity between the state embedding and the average of the premise's argument and goal embeddings, allowing either applicability or goal-satisfaction to drive a match. The CAR module concatenates state and premise and passes the pair through a BERT-style cross-encoder whose [CLS] representation is mapped to a relevance probability; training it against hard negatives selected from the CFR's top-k outputs is what makes the final ranking accurate at short list lengths. The shared foundation is a BERT pre-trained from scratch with a tokenizer learned on formal corpus text, which is what lets a small model internalize Lean syntax rather than being fine-tuned across the natural-language/formal-language gap.","core_discovery":"The central claim is that an effective premise retriever for Lean can be learned entirely from formalized mathematics, without relying on natural-language supervision, and that this retriever improves downstream theorem proving. The authors show that a six-layer BERT pre-trained with masked language modeling on Mathlib-derived text, paired with a WordPiece tokenizer trained on the same formal corpus, produces embeddings that separate relevant from irrelevant premises better than fine-tuned general-purpose encoders such as UniXcoder, E5-large-v2, and BGE-m3. Their retrieval stage uses a fine-grained similarity: the proof-state embedding is compared to the average of the premise's argument embedding and goal embedding, which lets a premise match either because it applies to the current context or because it would finish the current goal. The re-ranking stage, trained with hard negatives drawn from the first stage's top candidates, then lifts recall at small k. In retrieval-augmented proving on MiniF2F the combined system achieves pass@1 30.74% against ReProver's 28.28%, with roughly one-third the parameters of ReProver.","pith_inferences":["A corollary the paper leaves implicit is that the same recipe, training a tokenizer and small encoder directly on a formal library, should transfer to other proof assistants such as Coq or Isabelle, because the failure mode it fixes, natural-language pre-training mismatching formal syntax, is library-independent.","The Reference Isolated generalization result would be a stiffer test if masked-language-model pre-training were restricted to training-split premises only; that experiment is not run, so the RI numbers may overstate how much generalization comes from the model rather than from unsupervised exposure to test-premise text.","One testable extension suggested by the robustness results is to stress the retriever with adversarial renaming or variable-obfuscation of query states; the current perturbations only shuffle or delete context, so they do not probe whether retrieval depends on surface identifiers rather than mathematical structure.","Conditional on the pass@1 gain on MiniF2F, pairing this retriever with a much stronger tactic generator than ByT5, a direction the paper itself notes, would likely make the retrieval-quality gap visible in prove-rate differences on the splits where it is currently on par."],"forward_implications":["Retrieval-augmented theorem proving on MiniF2F improves with this retriever: pass@1 rises from 28.28% (ReProver) to 30.74%.","A Lean-specific tokenizer and masked-language-model pre-training are the components that carry most of the gain, since omitting the tokenizer degrades Recall@5 and Recall@10 sharply.","The fine-grained similarity function contributes separately to retrieval quality, as the ablation replacing it with a single-embedding cosine similarity shows lower Recall@10.","Because premise embeddings are precomputed and the CFR model is small, the system can serve as a real-time search engine deployed for premise lookup during formalization.","The re-ranking module is what makes top-1 to top-10 recall competitive; without it the retriever only consistently beats ReProver at larger list sizes such as 10 or more."],"supporting_citations":[{"why":"ReProver is the primary baseline and supplies the LeanDojo extraction pipeline, training setup, and retrieval-augmented proving methodology.","marker":"(Yang et al., 2024)"},{"why":"BERT is the backbone architecture for both the context-free retrieval module and the context-aware re-ranking module.","marker":"(Devlin et al., 2019)"},{"why":"Dense retrieval with separately encoded queries and documents motivates the design of the context-free retrieval stage.","marker":"(Karpukhin et al., 2020)"},{"why":"Sequence-pair classification with BERT is the template for the context-aware re-ranking module.","marker":"(Nogueira & Cho, 2019)"},{"why":"ByT5 is the tactic generator used in the theorem-proving evaluation pipeline.","marker":"(Xue et al., 2022)"},{"why":"MiniF2F provides the benchmark and pass@1 metric for comparing retrieval-augmented provers.","marker":"(Zheng et al., 2022)"},{"why":"Contrastive learning with in-batch negatives supplies the learning objective for the retrieval model.","marker":"(Izacard et al., 2022)"},{"why":"Contrastive learning formulations are cited as the framework for training both modules.","marker":"(Chen et al., 2020; He et al., 2020)"}],"fun_headline_variants":["Lightweight Lean premise retriever beats ReProver","66M-param retriever improves Lean proof search","Data-only premise retriever for Lean outdoes baselines","Efficient retriever trained on Mathlib boosts proving","Lean premise search hits 30.74% pass@1"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that unsupervised masked-language-model pre-training on the text of every premise in the corpus, including premises that appear in the validation and test sets, does not itself teach the model which of those premises answer a given proof state; if that assumption fails, the Reference Isolated split measures transductive exposure rather than clean generalization to unseen premises.","fun_headline_variants_meta":{"raw":{"variants":["Lightweight Lean premise retriever beats ReProver","66M-param retriever improves Lean proof search","Data-only premise retriever for Lean outdoes baselines","Efficient retriever trained on Mathlib boosts proving","Lean premise search hits 30.74% pass@1"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001132,"raw_usage":{"total_tokens":4737,"prompt_tokens":1011,"completion_tokens":3726,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":627,"completion_tokens_details":{"reasoning_tokens":3653}},"tokens_in":627,"tokens_out":3726,"duration_ms":23062,"temperature":1.0,"reasoning_tokens":3653,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T17:43:08.461514+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Train the same architecture with masked-language-model pre-training restricted to premises from the training split only, then evaluate on the Reference Isolated test set: if Recall@1 falls back to roughly the ReProver level of 5.05%, the paper's generalization claim is not supported; if the gain persists, the claim survives.","supporting_citations":[{"cited_title":"J., and Anandkumar, A","cited_arxiv_id":null,"evidence_quote":"ReProver is the primary baseline and supplies the LeanDojo extraction pipeline, training setup, and retrieval-augmented proving methodology."},{"cited_title":"Byt5: Towards a token-free future with pre-trained byte-to-byte models","cited_arxiv_id":null,"evidence_quote":"ByT5 is the tactic generator used in the theorem-proving evaluation pipeline."},{"cited_title":"M., and Polu, S","cited_arxiv_id":null,"evidence_quote":"MiniF2F provides the benchmark and pass@1 metric for comparing retrieval-augmented provers."}],"review_version":1}