Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization

Haotian Liu; Hongteng Xu; Shanwen Wang; Yicheng Tao

REVIEW 2 major objections 4 minor 31 references

Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization

T0 review · 2 major / 4 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2501.13959 v3 pith:BZTBLYV7 submitted 2025-01-21 cs.CL cs.AIcs.IR

Yicheng Tao , Haotian Liu , Shanwen Wang , Hongteng Xu This is my paper · ORCID

classification cs.CLcs.AIcs.IR

keywords premiseretrievalLeantheoremprovingformalmathematicscontrastivelearningdensere-rankingBERTMathlib

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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.

The 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.

The 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.

Who 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.

Recommendation: send it to review.

Referee Report

2 major / 4 minor

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.

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 (2)

[§4.1 (pre-training corpus); §4.2 (RI split); Table 2.] 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.
[§4.1 (Baselines); §4.5 (MiniF2F results).] 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.

minor comments (4)

[Abstract; Figure 5.] 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.
[Eq. (6) in §3.3.] 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.
[§4.5 and §5.] 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.
[§4.1 and §4.2 (terminology).] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the retrieval and theorem-proving results are benchmarked against external baselines and MiniF2F, not derived from the model's own definitions.

full rationale

The paper's central claims are empirical comparisons. The CFR model is learned by contrastive learning (Eq. 5) on state-premise pairs extracted from human-written Mathlib proofs, and the CAR model is learned by cross-entropy classification with hard negatives from the retriever (Eq. 6); neither objective defines the evaluation metric in terms of the model's own output. Retrieval metrics use ground-truth premises used by tactics (Table 1), and theorem-proving results use the external MiniF2F benchmark and an independently trained ByT5 generator, so the headline pass@1 comparison (30.74% vs. ReProver's 28.28%) is not forced by construction. Ablations (Table 3) attribute gains to pretraining, tokenizer, and similarity design rather than to a fitted input being renamed as a prediction. No load-bearing self-citation or imported uniqueness theorem is used to choose the architecture. The only notable weakness is methodological, not circular: in Section 4.1 the pretraining corpus is built from "states from the training set and all premises' argument lists and goals from the corpus," so the Reference Isolated split of Section 4.2 does not strictly test generalization to premise strings never seen in any training signal because the MLM pretraining saw all premise texts. That is a data-validity caveat affecting the RI generalization claim, but it does not make any retrieval result equivalent to a training label or fitted parameter, so it does not constitute circularity.

Assumptions & free parameters 4 free parameters · 4 assumptions · 0 invented entities

The central claim is an empirical engineering result. It does not introduce new physical or mathematical entities. The main contributions are model design choices and the data pipeline. The ledger above captures the manually chosen hyperparameters and the domain assumptions on which the evaluation rests. The most fragile item is the pre-training and evaluation overlap on the RI split.

free parameters (4)

Temperature tau in contrastive loss (Eq. 5) = not reported
Chosen by hand; affects embedding discrimination but the paper never gives its value.
Number of candidate premises k1 and final top-k = k1=100, k=20
Evaluation pipeline choices in Section 4.1; final metrics depend on them.
BERT architecture sizes = 6 layers, hidden 768, vocab 30,522
Design choices selected by the authors without an architecture search.
Maximum sequence lengths = state 512, premise 256, rerank 1024
Truncation thresholds that affect what information the model sees.

assumptions (4)

domain assumption Premises used in human-written Mathlib proofs are the ground-truth relevant premises for each proof state.
Section 3.1 builds the training and evaluation dataset from tactic-premise pairs; retrieval quality is scored against these human choices.
domain assumption The linearized string representation of a proof state and a premise (context with <VAR>, goal with <GOAL>) preserves enough information for retrieval.
Section 3.2 preprocesses all inputs into this flat text format; BERT can only see this representation.
ad hoc to paper MLM pre-training on the full Mathlib premise corpus, including validation and test premises, does not invalidate the Reference Isolated split.
Section 4.1 states the pre-training corpus includes all premises' argument lists and goals; the RI split is intended to test generalization to unseen premises.
standard math Standard transformer and contrastive learning machinery (BERT, WordPiece, in-batch negatives) behaves as claimed in prior work.
Sections 3.2-3.3 rely on established ML methodology without re-proving it.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization." pith.science (2026). https://pith.science/paper/BZTBLYV7

@misc{pith2026250113959,
  author       = {Pith},
  title        = {Pith review of: Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BZTBLYV7}},
  note         = {Machine review of arXiv:2501.13959}
}

read the original abstract

Formalized mathematics has recently garnered significant attention for its ability to assist mathematicians across various fields. Premise retrieval, as a common step in mathematical formalization, has been a challenge, particularly for inexperienced users. Existing retrieval methods that facilitate natural language queries require a certain level of mathematical expertise from users, while approaches based on formal languages (e.g., Lean) typically struggle with the scarcity of training data, hindering the training of effective and generalizable retrieval models. In this work, we introduce a novel method that leverages data extracted from Mathlib to train a lightweight and effective premise retrieval model. In particular, the proposed model embeds queries (i.e., proof state provided by Lean) and premises in a latent space, featuring a tokenizer specifically trained on formal corpora. The model is learned in a contrastive learning framework, in which a fine-grained similarity calculation method and a re-ranking module are applied to enhance the retrieval performance. Experimental results demonstrate that our model outperforms existing baselines, achieving higher accuracy while maintaining a lower computational load. We have released an open-source search engine based on our retrieval model at https://premise-search.com/. The source code and the trained model can be found at https://github.com/ruc-ai4math/Premise-Retrieval.

Figures

Figures reproduced from arXiv: 2501.13959 by the authors.

**Figure 1.** A schematic diagram illustrating user interactions with an ITP (e.g., Lean) given our premise retrieval model. 1. Introduction Formalized mathematics has recently attracted significant attention. It helps verify existing mathematical results, identify errors in the literature, and has the potential to accelerate the peer-review process for mathematical papers. This process involves proving natural language theorem… view at source ↗

**Figure 2.** Examples of the theorem-proving process in Lean. require additional premises to take effect, while others operate independently. Furthermore, the behavior of certain tactics may vary depending on the presence of premises. 2.2. Related Work Learning-based Retrieval Models In the field of information retrieval, traditional methods like BM25 (Harman, 1995; Robertson et al., 2009) and TF-IDF (Salton & Buckley, 1988) … view at source ↗

**Figure 3.** The overview of the retrieval framework. We extract 149,549 premises from Mathlib as our formal theorem corpus. In the context-free retrieval stage, all the premises are encoded by averaging the embeddings of context and goal. The top-k1 premises retrieved in this stage will be re-ranked in a context-aware manner. 3.2. Model Architecture Our premise retrieval model consists of two components: a context-free retrieva… view at source ↗

Figures from the paper (3 more)

**Figure 5.** Figure 5: The performance and efficiency comparison on Random split datasets. The size of each point reflects the parameter size of each model. performance even improves when k = 1. These results demonstrate that our retrieval model is robust to variations in the order of query …

**Figure 7.** Figure 7: Retrieval-augmented theorem proving results. researchers in the community. Although our method has yielded promising results, there is still room for optimization in the retriever’s backbone model. For the Lean premise retrieval task, the data corpus contains valuable…

**Figure 8.** Figure 8: illustrates the statistics related to context length and the number of premises in the dataset. The context length represents the length of Γ, while the premise number indicates how many premises are utilized in a specific tactic. It is important to note that tactics t…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

31 extracted references · 14 canonical work pages

[1]

write newline

" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION format.date year duplicate empty "emp...
[2]

The Coq proof assistant reference manual: Version 6.1

Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.-C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C., et al. The Coq proof assistant reference manual: Version 6.1. PhD thesis, Inria, 1997

work page 1997
[3]

M 3-embedding: Multi-linguality, multi-functionality, multi-granularity text embeddings through self-knowledge distillation

Chen, J., Xiao, S., Zhang, P., Luo, K., Lian, D., and Liu, Z. M 3-embedding: Multi-linguality, multi-functionality, multi-granularity text embeddings through self-knowledge distillation. In Ku, L.-W., Martins, A., and Srikumar, V. (eds.), Findings of the Association for Computational Linguistics: ACL 2024, pp.\ 2318--2335, Bangkok, Thailand, August 2024. ...

doi:10.18653/v1/2024.findings-acl.137 2024
[4]

A simple framework for contrastive learning of visual representations

Chen, T., Kornblith, S., Norouzi, M., and Hinton, G. A simple framework for contrastive learning of visual representations. In International conference on machine learning, pp.\ 1597--1607. PMLR, 2020

2020
[5]

The lean theorem prover (system description)

De Moura, L., Kong, S., Avigad, J., Van Doorn, F., and von Raumer, J. The lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp.\ 378--388. Springer, 2015

work page 2015
[6]

BERT : Pre-training of deep bidirectional transformers for language understanding

Devlin, J., Chang, M.-W., Lee, K., and Toutanova, K. BERT : Pre-training of deep bidirectional transformers for language understanding. In Burstein, J., Doran, C., and Solorio, T. (eds.), Proceedings of the 2019 Conference of the North A merican Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long and Short...

doi:10.18653/v1/n19-1423 2019
[7]

A semantic search engine for mathlib4

Gao, G., Ju, H., Jiang, J., Qin, Z., and Dong, B. A semantic search engine for mathlib4. In Al-Onaizan, Y., Bansal, M., and Chen, Y.-N. (eds.), Findings of the Association for Computational Linguistics: EMNLP 2024, pp.\ 8001--8013, Miami, Florida, USA, November 2024. Association for Computational Linguistics. doi:10.18653/v1/2024.findings-emnlp.470. URL h...

doi:10.18653/v1/2024.findings-emnlp.470 2024
[8]

U ni X coder: Unified cross-modal pre-training for code representation

Guo, D., Lu, S., Duan, N., Wang, Y., Zhou, M., and Yin, J. U ni X coder: Unified cross-modal pre-training for code representation. In Muresan, S., Nakov, P., and Villavicencio, A. (eds.), Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp.\ 7212--7225, Dublin, Ireland, May 2022. Association ...

doi:10.18653/v1/2022.acl-long.499 2022

Show all 31 references

[9]

Harman, D. K. Overview of the third text retrieval conference (TREC-3). Number 500. DIANE Publishing, 1995

1995
[10]

Momentum contrast for unsupervised visual representation learning

He, K., Fan, H., Wu, Y., Xie, S., and Girshick, R. Momentum contrast for unsupervised visual representation learning. In Proceedings of the IEEE/CVF conference on computer vision and pattern recognition, pp.\ 9729--9738, 2020

2020
[11]

Unsupervised dense information retrieval with contrastive learning

Izacard, G., Caron, M., Hosseini, L., Riedel, S., Bojanowski, P., Joulin, A., and Grave, E. Unsupervised dense information retrieval with contrastive learning. Transactions on Machine Learning Research, 2022. ISSN 2835-8856. URL https://openreview.net/forum?id=jKN1pXi7b0

2022
[12]

Dense passage retrieval for open-domain question answering

Karpukhin, V., Oguz, B., Min, S., Lewis, P., Wu, L., Edunov, S., Chen, D., and Yih, W.-t. Dense passage retrieval for open-domain question answering. In Webber, B., Cohn, T., He, Y., and Liu, Y. (eds.), Proceedings of the 2020 Conference on Empirical Methods in Natural Languag...

2020 doi
[13]

Llama2vec: Unsupervised adaptation of large language models for dense retrieval

Li, C., Liu, Z., Xiao, S., Shao, Y., and Lian, D. Llama2vec: Unsupervised adaptation of large language models for dense retrieval. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp.\ 3490--3500, 2024

2024
[14]

Fine-tuning llama for multi-stage text retrieval

Ma, X., Wang, L., Yang, N., Wei, F., and Lin, J. Fine-tuning llama for multi-stage text retrieval. In Proceedings of the 47th International ACM SIGIR Conference on Research and Development in Information Retrieval, pp.\ 2421--2425, 2024

2024
[15]

P., Szegedy, C., Kuci \'n ski, ., Mi o \'s , P., and Wu, Y

Miku a, M., Antoniak, S., Tworkowski, S., Piotrowski, B., Jiang, A., Zhou, J. P., Szegedy, C., Kuci \'n ski, ., Mi o \'s , P., and Wu, Y. Magnushammer: A transformer-based approach to premise selection. In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS'23, 2023. ...

2023
[16]

Nipkow, T., Wenzel, M., and Paulson, L. C. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002

2002
[17]

and Cho, K

Nogueira, R. and Cho, K. Passage re-ranking with bert. CoRR, abs/1901.04085, 2019. URL http://arxiv.org/abs/1901.04085

1901 arXiv
[18]

Understanding the behaviors of bert in ranking

Qiao, Y., Xiong, C., Liu, Z., and Liu, Z. Understanding the behaviors of bert in ranking. arXiv preprint arXiv:1904.07531, 2019

1904 arXiv
[19]

X., Dong, D., Wu, H., and Wang, H

Qu, Y., Ding, Y., Liu, J., Liu, K., Ren, R., Zhao, W. X., Dong, D., Wu, H., and Wang, H. R ocket QA : An optimized training approach to dense passage retrieval for open-domain question answering. In Toutanova, K., Rumshisky, A., Zettlemoyer, L., Hakkani-Tur, D., Beltagy, I., B...

2021
[20]

Z., Shao, Z., Song, J., Xin, H., Wang, H., Zhao, W., Zhang, L., Fu, Z., Zhu, Q., Yang, D., Wu, Z

Ren, Z. Z., Shao, Z., Song, J., Xin, H., Wang, H., Zhao, W., Zhang, L., Fu, Z., Zhu, Q., Yang, D., Wu, Z. F., Gou, Z., Ma, S., Tang, H., Liu, Y., Gao, W., Guo, D., and Ruan, C. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal d...

2025 arXiv
[21]

The probabilistic relevance framework: Bm25 and beyond

Robertson, S., Zaragoza, H., et al. The probabilistic relevance framework: Bm25 and beyond. Foundations and Trends in Information Retrieval , 3 0 (4): 0 333--389, 2009

2009
[22]

and Buckley, C

Salton, G. and Buckley, C. Term-weighting approaches in automatic text retrieval. Information processing & management, 24 0 (5): 0 513--523, 1988

1988
[23]

Towards large language models as copilots for theorem proving in lean

Song, P., Yang, K., and Anandkumar, A. Towards large language models as copilots for theorem proving in lean. In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS'23, 2023. URL https://openreview.net/forum?id=C9X5sXa2k1

2023
[24]

Fast wordpiece tokenization

Song, X., Salcianu, A., Song, Y., Dopson, D., and Zhou, D. Fast wordpiece tokenization. In EMNLP (1), pp.\ 2089--2103, 2021. URL https://aclanthology.org/2021.emnlp-main.160

2021
[25]

cloze procedure

Taylor, W. L. “cloze procedure”: A new tool for measuring readability. Journalism quarterly, 30 0 (4): 0 415--433, 1953

1953
[26]

Text embeddings by weakly-supervised contrastive pre-training

Wang, L., Yang, N., Huang, X., Jiao, B., Yang, L., Jiang, D., Majumder, R., and Wei, F. Text embeddings by weakly-supervised contrastive pre-training. arXiv preprint arXiv:2212.03533, 2022

2022 arXiv
[27]

Improving text embeddings with large language models

Wang, L., Yang, N., Huang, X., Yang, L., Majumder, R., and Wei, F. Improving text embeddings with large language models. In Ku, L.-W., Martins, A., and Srikumar, V. (eds.), Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long ...

2024 doi
[28]

and Saha, R

Welleck, S. and Saha, R. llmstep: LLM proofstep suggestions in lean. In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS'23, 2023. URL https://openreview.net/forum?id=ODOJuAM4Qj

2023
[29]

Byt5: Towards a token-free future with pre-trained byte-to-byte models

Xue, L., Barua, A., Constant, N., Al-Rfou, R., Narang, S., Kale, M., Roberts, A., and Raffel, C. Byt5: Towards a token-free future with pre-trained byte-to-byte models. Transactions of the Association for Computational Linguistics, 10: 0 291--306, 2022

2022
[30]

J., and Anandkumar, A

Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R. J., and Anandkumar, A. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36, 2024

2024
[31]

M., and Polu, S

Zheng, K., Han, J. M., and Polu, S. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2022. URL https://openreview.net/forum?id=9ZPegFuFTFv

2022

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.

[1] [1]

write newline

" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION format.date year duplicate empty "emp...

[2] [2]

The Coq proof assistant reference manual: Version 6.1

Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.-C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C., et al. The Coq proof assistant reference manual: Version 6.1. PhD thesis, Inria, 1997

work page 1997

[3] [3]

M 3-embedding: Multi-linguality, multi-functionality, multi-granularity text embeddings through self-knowledge distillation

Chen, J., Xiao, S., Zhang, P., Luo, K., Lian, D., and Liu, Z. M 3-embedding: Multi-linguality, multi-functionality, multi-granularity text embeddings through self-knowledge distillation. In Ku, L.-W., Martins, A., and Srikumar, V. (eds.), Findings of the Association for Computational Linguistics: ACL 2024, pp.\ 2318--2335, Bangkok, Thailand, August 2024. ...

doi:10.18653/v1/2024.findings-acl.137 2024

[4] [4]

A simple framework for contrastive learning of visual representations

Chen, T., Kornblith, S., Norouzi, M., and Hinton, G. A simple framework for contrastive learning of visual representations. In International conference on machine learning, pp.\ 1597--1607. PMLR, 2020

2020

[5] [5]

The lean theorem prover (system description)

De Moura, L., Kong, S., Avigad, J., Van Doorn, F., and von Raumer, J. The lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp.\ 378--388. Springer, 2015

work page 2015

[6] [6]

BERT : Pre-training of deep bidirectional transformers for language understanding

Devlin, J., Chang, M.-W., Lee, K., and Toutanova, K. BERT : Pre-training of deep bidirectional transformers for language understanding. In Burstein, J., Doran, C., and Solorio, T. (eds.), Proceedings of the 2019 Conference of the North A merican Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long and Short...

doi:10.18653/v1/n19-1423 2019

[7] [7]

A semantic search engine for mathlib4

Gao, G., Ju, H., Jiang, J., Qin, Z., and Dong, B. A semantic search engine for mathlib4. In Al-Onaizan, Y., Bansal, M., and Chen, Y.-N. (eds.), Findings of the Association for Computational Linguistics: EMNLP 2024, pp.\ 8001--8013, Miami, Florida, USA, November 2024. Association for Computational Linguistics. doi:10.18653/v1/2024.findings-emnlp.470. URL h...

doi:10.18653/v1/2024.findings-emnlp.470 2024

[8] [8]

U ni X coder: Unified cross-modal pre-training for code representation

Guo, D., Lu, S., Duan, N., Wang, Y., Zhou, M., and Yin, J. U ni X coder: Unified cross-modal pre-training for code representation. In Muresan, S., Nakov, P., and Villavicencio, A. (eds.), Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp.\ 7212--7225, Dublin, Ireland, May 2022. Association ...

doi:10.18653/v1/2022.acl-long.499 2022