Pith. sign in

REVIEW 3 major objections 8 minor 1 cited by

MIRB: Mathematical Information Retrieval Benchmark

T0 review · 3 major / 8 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read MIRB unifies four mathematical retrieval tasks into one benchmark and shows current models are much weaker when retrieval requires reasoning, especially over formal proof premises.

desk verdict Useful consolidation of MIR datasets, but the dynamic-corpus rows on three of the twelve datasets are reranking tasks over pre-judged pools, so the comprehensive-retrieval framing needs softening. read the letter →

arxiv 2505.15585 v1 pith:I2CZGMKF submitted 2025-05-21 cs.IR cs.CLcs.LG

Haocheng Ju , Bin Dong This is my paper
classification cs.IRcs.CLcs.LG
keywords mathematicalinformationretrievalbenchmarksemanticstatementquestion-answerpremiseformulacross-encoderrerankingnDCG@10
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

Mathematical information retrieval is currently scattered across different competitions and datasets, so there has been no single way to compare models on the field's main jobs. MIRB is the paper's attempt to provide that: it groups 12 datasets into four tasks—semantic statement retrieval, question-answer retrieval, premise retrieval, and formula retrieval—and runs 13 retrieval models through all of them. The empirical claim is that every model does better on semantic matching and worse on tasks that require reasoning, with the lowest scores in formal-language premise retrieval. The paper also reports that applying general-purpose cross-encoder rerankers—models that rescore a query–document pair jointly—usually lowers scores instead of raising them. If the benchmark holds up, it gives the community one common measuring stick and points to reasoning-based retrieval, not semantic similarity, as the open problem in mathematics search.

What carries the argument

The central object is the MIRB suite itself: 12 datasets organized into four task families, each with its own queries, documents, relevance labels, and instructions, all scored by nDCG@10. The construction choices carry the argument: duplicate-question graphs closed under transitivity define semantic statement retrieval; theorem–proof pairs from natural-language libraries define question-answer retrieval; proof states paired with next-step premises define premise retrieval; judged formula pairs define formula retrieval. For datasets with incomplete relevance judgments (ARQMath-Task-1, ARQMath-Task-2, and NTCIR-WFB), the benchmark adopts a dynamic corpus: each query is evaluated only against its pre-annotated documents. This is what lets those datasets sit on the same leaderboard, at the cost of measuring reranking over a small judged set rather than full-corpus retrieval.

What would settle it

Run one ARQMath-Task-1 query against the complete 2010–2018 answer corpus instead of the annotated-only dynamic corpus; if the ranked results or the ordering of models changes materially once unjudged documents are handled correctly, then those rows measure reranking over a small judged set rather than retrieval from a real corpus.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is a measured gap between semantic and reasoning-based mathematical retrieval. MIRB assembles 12 datasets into four task families and scores 13 models with nDCG@10. Models reach moderate scores on semantic statement retrieval and formula retrieval, but their scores fall sharply on question-answer and especially premise retrieval; formal proof-state queries are the hardest, with several models landing in the single digits or low teens. The paper also finds that general-purpose cross-encoder rerankers—models that jointly score each query–document pair—do not transfer to mathematics: applied to the top five models, they lower average performance on most datasets. The contribution is therefore a benchmark and an empirical diagnosis, not a new retrieval method that beats the field.

Load-bearing premise

The benchmark assumes that retrieving from a judged-only dynamic corpus is equivalent to retrieving from the full real-world corpus for ARQMath-Task-1, ARQMath-Task-2, and NTCIR-WFB.

Editorial extensions

If this is right

  • A single MIRB leaderboard lets retrieval models be compared directly across theorem search, math-forum answer retrieval, premise selection, and formula lookup.
  • A model cannot claim to handle mathematical retrieval on the strength of semantic similarity alone; the reasoning-based tasks in MIRB expose that gap.
  • Formal premise retrieval is the clearest open problem: the lowest nDCG@10 scores in the benchmark appear on proof-state queries.
  • Cross-encoder rerankers should not be added to a math retrieval pipeline without task-specific validation, because the benchmark shows they usually reduce performance.

Reading between the lines

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

  • Because the ARQMath and NTCIR-WFB rows are judged-only dynamic corpora, I would read those scores as measuring reranking over candidate sets, not ad-hoc retrieval over a full corpus; a model could top those rows and still miss relevant documents in open search.
  • A testable extension the paper does not run is training a reranker on mathematical relevance judgments and repeating the reranking experiment; if the degradation reverses, the conclusion becomes that general-purpose rerankers, not reranking itself, are the problem.
  • The low formal premise-retrieval scores suggest natural-language text embeddings carry almost no usable formal-language semantics, so representations built from proof-state structure or dependency graphs are a plausible next direction; this is my inference, not a claim in the paper.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 8 minor

Summary. The paper introduces MIRB, a benchmark for mathematical information retrieval covering four tasks (semantic statement retrieval, question-answer retrieval, premise retrieval, and formula retrieval) across 12 datasets. The authors construct three new datasets (MSE/MO duplicate question retrieval and an Informalized Mathlib4 retrieval set derived from prior work) and assemble existing datasets, then evaluate 13 retrieval models using nDCG@10. They report that dense models generally outperform BM25, larger models outperform smaller ones, reasoning-oriented tasks are harder than semantic tasks, and cross-encoder rerankers generally degrade performance. Code and data are released.

Significance. If the identified evaluation-protocol issues are addressed, MIRB would be a valuable unified resource for MIR evaluation, filling a gap between general text retrieval benchmarks (BEIR, MTEB) and scattered math-specific datasets. The release of code and data is a clear strength, as is the coverage of both formal and informal mathematical retrieval tasks. The headline observations about task difficulty hierarchies and reranker transfer are plausible but are currently tied to experimental choices that need qualification.

major comments (3)
  1. [Sections 3.2 and 3.4] The dynamic corpus approach for ARQMath-Task-1, ARQMath-Task-2, and NTCIR-WFB restricts the corpus for each query to only its pre-annotated documents. This converts the task from ad-hoc retrieval into ranking over a small judged pool. The issue is especially severe for BM25, whose IDF statistics depend on the corpus, making the per-query scores incomparable with the static-corpus rows. The three corresponding rows in Table 9 therefore do not measure retrieval from the collection, and the unweighted 'Avg.' mixes these rows with true retrieval rows. The authors should either evaluate over the full corpora with appropriate sampling, or explicitly label these rows as reranking results and exclude them from the aggregate retrieval average.
  2. [Section 3.1] In the construction of MSE and MO Duplicate Question Retrieval, every candidate question with tag overlap at least 0.5 is removed from each query's corpus. This makes tag overlap a near-sufficient negative signal and removes hard negatives (topically similar but non-duplicate questions), with no justification for the threshold or sensitivity analysis. The resulting datasets may substantially overstate model performance and do not measure the ability to distinguish semantically similar but non-duplicate questions. The authors should report the effect of this filtering, such as the number of candidates removed per query and performance under different thresholds, or otherwise demonstrate that the retained corpora still contain sufficient hard negatives.
  3. [Section 4.2] The reranking experiment applies each reranker only to the top 10 documents retrieved by the base model. Consequently, the reranker cannot recover relevant documents originally ranked below position 10, so the conclusion that 'reranking generally leads to a decline in performance' and that rerankers 'may not transfer effectively' is a statement about reordering a small set rather than about full retrieval reranking. To support the general claim, the authors should rerank a larger candidate pool (e.g., top 100) or clearly qualify the conclusion to the top-10 setting.
minor comments (8)
  1. [Table 1] The column header 'A vg.' should be 'Avg.', and the header 'Relevancy' is ambiguous for a column that indicates the graded-relevance scale.
  2. [Table 2] The word 'intermidiate' should be 'intermediate'.
  3. [Table 7] The instruction entry for Cohere-embed-english-v3.0 reads 'Notext' instead of 'No'.
  4. [Sections 3.1 and 3.2] The term 'dynamic corpus' is used for two different constructions (per-query tag-overlap filtering and per-query annotated-only corpora); defining the term at first use would avoid ambiguity.
  5. [Table 9] The test sets for ARQMath-Task-1 and ARQMath-Task-2 contain only 78 and 76 queries, respectively; the paper should note the limited statistical power for ranking models on these rows.
  6. [Abstract and Section 4.2] The abstract's claim that 'all models perform worse on reasoning-based tasks compared to semantic-based tasks' is stronger than the evidence: for several models, specific reasoning tasks (e.g., ProofWiki for BM25) score higher than some semantic-statement tasks. The Section 4.2 phrasing 'generally perform better... performance degrades... especially Premise Retrieval' is more accurate; consider aligning the abstract with that language.
  7. [Section 4.2] The reranking experiment is run only on the top five models; a sentence explaining this selection would be helpful.
  8. [Section 4.1] The relationship between nDCG-prime and the nDCG@10 reported in Table 9 for the ARQMath rows is not fully specified; clarify how the metric handles incomplete judgments.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: MIRB evaluates fixed retrieval models on external datasets; the only self-citation is a benchmark input, and the dynamic-corpus caveats are validity concerns, not circular reasoning.

full rationale

MIRB is a benchmark paper: it assembles existing and newly constructed retrieval tasks and runs 13 pretrained models plus BM25. There is no fitted parameter that is later reported as a prediction; the headline results (semantic vs. reasoning gap, reranker degradation) are empirical measurements on test sets. The only overlap with the authors' prior work is the Informalized Mathlib4 Retrieval evaluation set [6], which is used as a benchmark input with its stated relevance criteria; no derived claim is justified by that citation. The dynamic-corpus construction for ARQMath-Task-1/2 and NTCIR-WFB (Sections 3.2 and 3.4) and the tag-overlap filtering in Section 3.1 are disclosed protocol choices; they may reduce the realism or difficulty of those rows (e.g., BM25 IDF is computed over a per-query judged pool), and the Limitations section concedes related false-negative and hard-negative concerns, but none of these makes an output equivalent to an input by construction. Therefore no circular step is present.

Assumptions & free parameters 2 free parameters · 5 assumptions · 0 invented entities

The benchmark's central claims rest on dataset-construction choices and on the validity of existing relevance judgments; no new mathematical or physical entities are introduced.

free parameters (2)
  • tag_overlap_threshold = 0.5
    Chosen in Section 3.1 to filter out candidate duplicate questions with high tag overlap; no sensitivity analysis or justification. Affects composition of MSE and MO corpora and therefore all duplicate-question scores.
  • rerank_candidate_count = 10
    Rerankers in Section 4.2 are applied only to the top 10 retrieved documents; the finding that reranking degrades performance may not generalize to different candidate set sizes.
assumptions (5)
  • domain assumption Relevance judgments in source datasets (ARQMath, NaturalProofs, NTCIR, etc.) are accurate and complete.
    All metrics depend on these labels; cited in Sections 3.2 to 3.4 without re-validation.
  • domain assumption Transitive closure of duplicate links on MSE and MO defines correct duplicate sets.
    Section 3.1 applies transitive closure to the duplicate graph; real duplicate annotations may not be transitive, introducing false positives.
  • ad hoc to paper The tag-overlap filter reduces false negatives without removing true positives.
    Section 3.1 sets the overlap threshold at 0.5; no empirical validation that excluded candidates are indeed non-duplicates.
  • ad hoc to paper Evaluating retrieval on a corpus containing only pre-annotated documents is a valid retrieval task.
    Section 3.2 applies the dynamic corpus approach to ARQMath-Task-1, ARQMath-Task-2, and NTCIR-WFB; this removes unjudged documents and changes the task from ad-hoc retrieval to ranking a small judged set.
  • domain assumption For HolStep, treating all dependencies as the corpus and conjectures as queries is a valid premise retrieval setup.
    Section 3.3 aggregates dependencies across files; no evaluation of whether this corpus composition matches the original HolStep task.

how reviews work

0 comments
Cite this review

Pith. "Pith review of MIRB: Mathematical Information Retrieval Benchmark." pith.science (2026). https://pith.science/paper/I2CZGMKF

@misc{pith2026250515585,
  author       = {Pith},
  title        = {Pith review of: MIRB: Mathematical Information Retrieval Benchmark},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/I2CZGMKF}},
  note         = {Machine review of arXiv:2505.15585}
}
read the original abstract

Mathematical Information Retrieval (MIR) is the task of retrieving information from mathematical documents and plays a key role in various applications, including theorem search in mathematical libraries, answer retrieval on math forums, and premise selection in automated theorem proving. However, a unified benchmark for evaluating these diverse retrieval tasks has been lacking. In this paper, we introduce MIRB (Mathematical Information Retrieval Benchmark) to assess the MIR capabilities of retrieval models. MIRB includes four tasks: semantic statement retrieval, question-answer retrieval, premise retrieval, and formula retrieval, spanning a total of 12 datasets. We evaluate 13 retrieval models on this benchmark and analyze the challenges inherent to MIR. We hope that MIRB provides a comprehensive framework for evaluating MIR systems and helps advance the development of more effective retrieval models tailored to the mathematical domain.

Figures

Figures reproduced from arXiv: 2505.15585 by the authors.

Figure 1
Figure 1. Overview of tasks and datasets in MIRB. performance. Moreover, the training data for retrieval models can be augmented with synthetic data generated by large language models [36, 25, 16]. 2.3 Mathematical Information Retrieval. Classical mathematical information retrieval methods often rely on tree-based representations to capture the structural information of mathematical formulas, such as the Symbol Layout Tree[43… view at source ↗

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Benchmarking Information Retrieval Models on Complex Retrieval Tasks

    cs.IR 2025-09 conditional novelty 6.0 of 10

    CRUMB is a new benchmark for complex, multi-aspect retrieval tasks on which state-of-the-art retrieval models score poorly, and query rewriting does not rescue the best models.

Reference graph

Works this paper leans on

54 extracted references · 42 canonical work pages · cited by 1 Pith paper

  1. [1]

    M3-Embedding: Multi-Linguality, Multi-Functionality, Multi-Granularity Text Embeddings Through Self- Knowledge Distillation

    Jianlyu Chen, Shitao Xiao, Peitian Zhang, Kun Luo, Defu Lian, and Zheng Liu. M3-Embedding: Multi-Linguality, Multi-Functionality, Multi-Granularity Text Embeddings Through Self- Knowledge Distillation. In Lun-Wei Ku, Andre Martins, and Vivek Srikumar, editors,Findings of the Association for Computational Linguistics: ACL 2024, pages 2318–2335, Bangkok, Th...

    work page 2024

  2. [2]

    Mathematical information retrieval: A review.ACM Computing Surveys, 57(3):1–34, 2024

    Pankaj Dadure, Partha Pakray, and Sivaji Bandyopadhyay. Mathematical information retrieval: A review.ACM Computing Surveys, 57(3):1–34, 2024

    work page 2024

  3. [3]

    The Lean 4 Theorem Prover and Programming Language

    Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. In André Platzer and Geoff Sutcliffe, editors,Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 ofLecture Notes in Computer Science, pages 625–635. Springer, 2021

    work page 2021

  4. [4]

    The Lean Theorem Prover (System Description)

    Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp, editors,Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 ofLecture Notes in Compu...

    work page 2015

  5. [5]

    Mmteb: Massive multilingual text embedding benchmark.arXiv preprint arXiv:2502.13595, 2025

    Kenneth Enevoldsen, Isaac Chung, Imene Kerboua, Márton Kardos, Ashwin Mathur, David Stap, Jay Gala, Wissam Siblini, Dominik Krzemi ´nski, Genta Indra Winata, et al. Mmteb: Massive multilingual text embedding benchmark.arXiv preprint arXiv:2502.13595, 2025

    arXiv 2025

  6. [6]

    A Semantic Search Engine for Mathlib4

    Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. A Semantic Search Engine for Mathlib4. In Yaser Al-Onaizan, Mohit Bansal, and Yun-Nung Chen, editors,Findings of the Association for Computational Linguistics: EMNLP 2024, pages 8001–8013, Miami, Florida, USA, November 2024. Association for Computational Linguistics

    work page 2024

  7. [7]

    The Math Retrieval System of ICST for NTCIR-12 MathIR Task

    Liangcai Gao, Ke Yuan, Yuehan Wang, Zhuoren Jiang, and Zhi Tang. The Math Retrieval System of ICST for NTCIR-12 MathIR Task. In Noriko Kando, Tetsuya Sakai, and Mark Sanderson, editors,Proceedings of the 12th NTCIR Conference on Evaluation of Information Access Technologies, National Center of Sciences, Tokyo, Japan, June 7-10, 2016. National Institute of...

    work page 2016

  8. [8]

    Verspoor, and Timothy Baldwin

    Doris Hoogeveen, Karin M. Verspoor, and Timothy Baldwin. CQADupStack: A Benchmark Data Set for Community Question-Answering Research. InProceedings of the 20th Australasian Document Computing Symposium, ADCS ’15, New York, NY , USA, 2015. Association for Computing Machinery

    work page 2015

Show all 54 references
  1. [9]

    CoSQA: 20,000+ Web Queries for Code Search and Question Answering

    Junjie Huang, Duyu Tang, Linjun Shou, Ming Gong, Ke Xu, Daxin Jiang, Ming Zhou, and Nan Duan. CoSQA: 20,000+ Web Queries for Code Search and Question Answering. In Chengqing Zong, Fei Xia, Wenjie Li, and Roberto Navigli, editors,Proceedings of the 59th Annual Meeting of the As...

  2. [10]

    Codesearchnet challenge: Evaluating the state of semantic code search.arXiv preprint arXiv:1909.09436, 2019

    Hamel Husain, Ho-Hsiang Wu, Tiferet Gazit, Miltiadis Allamanis, and Marc Brockschmidt. Codesearchnet challenge: Evaluating the state of semantic code search.arXiv preprint arXiv:1909.09436, 2019

    1909 arXiv

  3. [11]

    HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving

    Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. InInternational Conference on Learning Representations, 2017

    2017

  4. [12]

    Andrew Kane, Yin Ki Ng, and Frank Wm. Tompa. Dowsing for Answers to Math Questions: Doing Better with Less. In Guglielmo Faggioli, Nicola Ferro, Allan Hanbury, and Martin Potthast, editors,Proceedings of the Working Notes of CLEF 2022 - Conference and Labs of the Evaluation Fo...

    2022

  5. [13]

    ChemTEB: Chemical Text Embedding Benchmark, an Overview of Embedding Models Performance & Efficiency on a Specific Domain.arXiv preprint arXiv:2412.00532, 2024

    Ali Shiraee Kasmaee, Mohammad Khodadad, Mohammad Arshi Saloot, Nicholas Sherck, Stephen Dokas, Hamidreza Mahyar, and Soheila Samiee. ChemTEB: Chemical Text Embedding Benchmark, an Overview of Embedding Models Performance & Efficiency on a Specific Domain.arXiv preprint arXiv:2...

    2024 arXiv

  6. [14]

    XCodeEval: An Execution-based Large Scale Multilingual Multitask Benchmark for Code Understanding, Generation, Translation and Retrieval

    Mohammad Abdullah Matin Khan, M Saiful Bari, Xuan Long Do, Weishi Wang, Md Rizwan Parvez, and Shafiq Joty. XCodeEval: An Execution-based Large Scale Multilingual Multitask Benchmark for Code Understanding, Generation, Translation and Retrieval. In Lun-Wei Ku, Andre Martins, an...

    2024

  7. [15]

    NV-Embed: Improved Techniques for Training LLMs as Generalist Embedding Models

    Chankyu Lee, Rajarshi Roy, Mengyao Xu, Jonathan Raiman, Mohammad Shoeybi, Bryan Catanzaro, and Wei Ping. NV-Embed: Improved Techniques for Training LLMs as Generalist Embedding Models. InThe Thirteenth International Conference on Learning Representations, 2025

    2025

  8. [16]

    Gecko: Versatile text embeddings distilled from large language models.arXiv preprint arXiv:2403.20327, 2024

    Jinhyuk Lee, Zhuyun Dai, Xiaoqi Ren, Blair Chen, Daniel Cer, Jeremy R Cole, Kai Hui, Michael Boratko, Rajvi Kapadia, Wen Ding, et al. Gecko: Versatile text embeddings distilled from large language models.arXiv preprint arXiv:2403.20327, 2024

    2024 arXiv

  9. [17]

    Coir: A comprehensive benchmark for code information retrieval models.arXiv preprint arXiv:2407.02883, 2024

    Xiangyang Li, Kuicai Dong, Yi Quan Lee, Wei Xia, Hao Zhang, Xinyi Dai, Yasheng Wang, and Ruiming Tang. Coir: A comprehensive benchmark for code information retrieval models.arXiv preprint arXiv:2407.02883, 2024

    2024 arXiv

  10. [18]

    AoE: Angle-optimized Embeddings for Semantic Textual Similarity

    Xianming Li and Jing Li. AoE: Angle-optimized Embeddings for Semantic Textual Similarity. In Lun-Wei Ku, Andre Martins, and Vivek Srikumar, editors,Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 1825–1839,...

    2024

  11. [19]

    Towards general text embeddings with multi-stage contrastive learning.arXiv preprint arXiv:2308.03281, 2023

    Zehan Li, Xin Zhang, Yanzhao Zhang, Dingkun Long, Pengjun Xie, and Meishan Zhang. Towards general text embeddings with multi-stage contrastive learning.arXiv preprint arXiv:2308.03281, 2023

    2023 arXiv

  12. [20]

    Oard, and Richard Zanibbi

    Behrooz Mansouri, Anurag Agarwal, Douglas W. Oard, and Richard Zanibbi. Advancing Math- Aware Search: The ARQMath-3 Lab at CLEF 2022. In Matthias Hagen, Suzan Verberne, Craig Macdonald, Christin Seifert, Krisztian Balog, Kjetil Nørvåg, and Vinay Setty, editors,Advances in Info...

    2022

  13. [21]

    Oard, and Anurag Agarwal

    Behrooz Mansouri, Richard Zanibbi, Douglas W. Oard, and Anurag Agarwal. Overview of ARQMath-2 (2021): Second CLEF Lab on Answer Retrieval for Questions on Math. In K. Selçuk Candan, Bogdan Ionescu, Lorraine Goeuriot, Birger Larsen, Henning Müller, Alexis Joly, Maria Maistro, F...

    2021

  14. [22]

    SFR-Embedding-2: Advanced Text Embedding with Multi-stage Training, 2024

    Rui Meng*, Ye Liu*, Shafiq Rayhan Joty, Yingbo Zhou Caiming Xiong, and Semih Yavuz. SFR-Embedding-2: Advanced Text Embedding with Multi-stage Training, 2024. 11

    2024

  15. [23]

    SFR- Embedding-Mistral:Enhance Text Retrieval with Transfer Learning

    Rui Meng, Ye Liu, Shafiq Rayhan Joty, Caiming Xiong, Yingbo Zhou, and Semih Yavuz. SFR- Embedding-Mistral:Enhance Text Retrieval with Transfer Learning. Salesforce AI Research Blog, 2024

    2024

  16. [24]

    Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuci´nski, Piotr Miło´s, and Yuhuai Wu

    Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Q. Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuci´nski, Piotr Miło´s, and Yuhuai Wu. Magnusham- mer: A Transformer-Based Approach to Premise Selection. InThe Twelfth International Conference on...

    2024

  17. [25]

    Generative representational instruction tuning

    Niklas Muennighoff, SU Hongjin, Liang Wang, Nan Yang, Furu Wei, Tao Yu, Amanpreet Singh, and Douwe Kiela. Generative representational instruction tuning. InICLR 2024 Workshop: How Far Are We From AGI, 2024

    2024

  18. [26]

    MTEB: Massive Text Embedding Benchmark

    Niklas Muennighoff, Nouamane Tazi, Loic Magne, and Nils Reimers. MTEB: Massive Text Embedding Benchmark. In Andreas Vlachos and Isabelle Augenstein, editors,Proceedings of the 17th Conference of the European Chapter of the Association for Computational Linguistics, pages 2014–...

    2014

  19. [27]

    Text and Code Embeddings by Contrastive Pre-Training

    Arvind Neelakantan, Tao Xu, Raul Puri, Alec Radford, Jesse Michael Han, Jerry Tworek, Qiming Yuan, Nikolas Tezak, Jong Wook Kim, Chris Hallacy, Johannes Heidecke, Pranav Shyam, Boris Power, Tyna Eloundou Nekoul, Girish Sastry, Gretchen Krueger, David Schnurr, Felipe Petroski S...

    2022 arXiv

  20. [28]

    Walker, S

    Stephen Robertson, S. Walker, S. Jones, M. M. Hancock-Beaulieu, and M. Gatford. Okapi at TREC-3. InOverview of the Third Text REtrieval Conference (TREC-3), pages 109–126. Gaithersburg, MD: NIST, January 1995

    1995

  21. [29]

    The Probabilistic Relevance Framework: BM25 and Beyond.Found

    Stephen Robertson and Hugo Zaragoza. The Probabilistic Relevance Framework: BM25 and Beyond.Found. Trends Inf. Retr., 3(4):333–389, apr 2009

    2009

  22. [30]

    On information retrieval metrics designed for evaluation with incomplete relevance assessments.Information Retrieval, 11:447–470, 2008

    Tetsuya Sakai and Noriko Kando. On information retrieval metrics designed for evaluation with incomplete relevance assessments.Information Retrieval, 11:447–470, 2008

    2008

  23. [31]

    Smith, Luke Zettlemoyer, and Tao Yu

    Hongjin Su, Weijia Shi, Jungo Kasai, Yizhong Wang, Yushi Hu, Mari Ostendorf, Wen-tau Yih, Noah A. Smith, Luke Zettlemoyer, and Tao Yu. One Embedder, Any Task: Instruction-Finetuned Text Embeddings. In Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki, editors,Findings of the...

    2023

  24. [32]

    BRIGHT: A Realistic and Challenging Benchmark for Reasoning- Intensive Retrieval

    Hongjin SU, Howard Yen, Mengzhou Xia, Weijia Shi, Niklas Muennighoff, Han yu Wang, Liu Haisu, Quan Shi, Zachary S Siegel, Michael Tang, Ruoxi Sun, Jinsung Yoon, Sercan O Arik, Danqi Chen, and Tao Yu. BRIGHT: A Realistic and Challenging Benchmark for Reasoning- Intensive Retrie...

    2025

  25. [33]

    MAIR: A Massive Benchmark for Evaluating Instructed Retrieval.arXiv preprint arXiv:2410.10127, 2024

    Weiwei Sun, Zhengliang Shi, Jiulong Wu, Lingyong Yan, Xinyu Ma, Yiding Liu, Min Cao, Dawei Yin, and Zhaochun Ren. MAIR: A Massive Benchmark for Evaluating Instructed Retrieval.arXiv preprint arXiv:2410.10127, 2024

    2024 arXiv

  26. [34]

    BEIR: A Heterogeneous Benchmark for Zero-shot Evaluation of Information Retrieval Models

    Nandan Thakur, Nils Reimers, Andreas Rücklé, Abhishek Srivastava, and Iryna Gurevych. BEIR: A Heterogeneous Benchmark for Zero-shot Evaluation of Information Retrieval Models. InThirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Rou...

    2021

  27. [35]

    Text Embeddings by Weakly-Supervised Contrastive Pre-training

    Liang Wang, Nan Yang, Xiaolong Huang, Binxing Jiao, Linjun Yang, Daxin Jiang, Rangan Majumder, and Furu Wei. Text Embeddings by Weakly-Supervised Contrastive Pre-training. CoRR, abs/2212.03533, 2022

    2022 arXiv

  28. [36]

    Improving Text Embeddings with Large Language Models

    Liang Wang, Nan Yang, Xiaolong Huang, Linjun Yang, Rangan Majumder, and Furu Wei. Improving Text Embeddings with Large Language Models. In Lun-Wei Ku, Andre Martins, and Vivek Srikumar, editors,Proceedings of the 62nd Annual Meeting of the Association for 12 Computational Ling...

    2024

  29. [37]

    NaturalProofs: Mathematical Theorem Proving in Natural Language

    Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. NaturalProofs: Mathematical Theorem Proving in Natural Language. InThirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1), 2021

    2021

  30. [38]

    Naturalprover: Grounded mathematical proof generation with language models.Advances in Neural Informa- tion Processing Systems, 35:4913–4927, 2022

    Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. Naturalprover: Grounded mathematical proof generation with language models.Advances in Neural Informa- tion Processing Systems, 35:4913–4927, 2022

    2022

  31. [39]

    Rar-b: Reasoning as retrieval benchmark.arXiv preprint arXiv:2404.06347, 2024

    Chenghao Xiao, G Thomas Hudson, and Noura Al Moubayed. Rar-b: Reasoning as retrieval benchmark.arXiv preprint arXiv:2404.06347, 2024

    2024 arXiv

  32. [40]

    C-Pack: Packed Resources For General Chinese Embeddings

    Shitao Xiao, Zheng Liu, Peitian Zhang, Niklas Muennighoff, Defu Lian, and Jian-Yun Nie. C-Pack: Packed Resources For General Chinese Embeddings. InProceedings of the 47th International ACM SIGIR Conference on Research and Development in Information Retrieval, SIGIR ’24, page 6...

    2024

  33. [41]

    LeanDojo: Theorem Proving with Retrieval- Augmented Language Models

    Kaiyu Yang, Aidan M Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem Proving with Retrieval- Augmented Language Models. InThirty-seventh Conference on Neural Information Processing Systems Datasets and...

    2023

  34. [42]

    NTCIR-12 MathIR Task Overview

    Richard Zanibbi, Akiko Aizawa, Michael Kohlhase, Iadh Ounis, Goran Topic, and Kenny Davila. NTCIR-12 MathIR Task Overview. InNTCIR, 2016

    2016

  35. [43]

    Recognition and retrieval of mathematical expressions

    Richard Zanibbi and Dorothea Blostein. Recognition and retrieval of mathematical expressions. Int. J. Document Anal. Recognit., 15(4):331–357, 2012

    2012

  36. [44]

    Mathematical information retrieval: Search and question answering.Foundations and Trends® in Information Retrieval, 19(1-2):1– 190, 2025

    Richard Zanibbi, Behrooz Mansouri, Anurag Agarwal, et al. Mathematical information retrieval: Search and question answering.Foundations and Trends® in Information Retrieval, 19(1-2):1– 190, 2025

    2025

  37. [45]

    Oard, Anurag Agarwal, and Behrooz Mansouri

    Richard Zanibbi, Douglas W. Oard, Anurag Agarwal, and Behrooz Mansouri. Overview of ARQMath 2020: CLEF Lab on Answer Retrieval for Questions on Math. In Avi Arampatzis, Evangelos Kanoulas, Theodora Tsikrika, Stefanos Vrochidis, Hideo Joho, Christina Lioma, Carsten Eickhoff, Au...

    2020

  38. [46]

    One Blade for One Purpose: Advancing Math Information Retrieval using Hybrid Search

    Wei Zhong, Sheng-Chieh Lin, Jheng-Hong Yang, and Jimmy Lin. One Blade for One Purpose: Advancing Math Information Retrieval using Hybrid Search. InProceedings of the 46th International ACM SIGIR Conference on Research and Development in Information Retrieval, SIGIR ’23, page 1...

    2023

  39. [47]

    Lee Giles, and Richard Zanibbi

    Wei Zhong, Shaurya Rohatgi, Jian Wu, C. Lee Giles, and Richard Zanibbi. Accelerating Substructure Similarity Search for Formula Retrieval. InAdvances in Information Retrieval: 42nd European Conference on IR Research, ECIR 2020, Lisbon, Portugal, April 14–17, 2020, Proceedings,...

    2020

  40. [48]

    Applying Structural and Dense Semantic Matching for the ARQMath Lab 2022, CLEF

    Wei Zhong, Yuqing Xie, and Jimmy Lin. Applying Structural and Dense Semantic Matching for the ARQMath Lab 2022, CLEF. In Guglielmo Faggioli, Nicola Ferro, Allan Hanbury, and Martin Potthast, editors,Proceedings of the Working Notes of CLEF 2022 - Conference and Labs of the Eva...

    2022

  41. [49]

    Evaluating Token-Level and Passage-Level Dense Retrieval Models for Math Information Retrieval

    Wei Zhong, Jheng-Hong Yang, Yuqing Xie, and Jimmy Lin. Evaluating Token-Level and Passage-Level Dense Retrieval Models for Math Information Retrieval. In Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang, editors,Findings of the Association for Computational Linguistics: EMNLP 2...

    2022

  42. [50]

    Structural Similarity Search for Formulas Using Leaf-Root Paths in Operator Subtrees

    Wei Zhong and Richard Zanibbi. Structural Similarity Search for Formulas Using Leaf-Root Paths in Operator Subtrees. In Leif Azzopardi, Benno Stein, Norbert Fuhr, Philipp Mayr, Claudia Hauff, and Djoerd Hiemstra, editors,Advances in Information Retrieval - 41st European Confer...

    2019

  43. [51]

    LongEmbed: Extending Embedding Models for Long Context Retrieval

    Dawei Zhu, Liang Wang, Nan Yang, Yifan Song, Wenhao Wu, Furu Wei, and Sujian Li. LongEmbed: Extending Embedding Models for Long Context Retrieval. In Yaser Al-Onaizan, Mohit Bansal, and Yun-Nung Chen, editors,Proceedings of the 2024 Conference on Empirical Methods in Natural L...

    2024

  44. [54]

    ’c list" and ys ::

    match (list_comb f ps) (list_comb g vs) = None list_induct2: fixes xs :: "’c list" and ys :: "’d list" and P :: "’c list <Rightarrow> ’d list <Rightarrow> bool" assumes "length xs = length ys" and "P [] []" and " <And>x xs y ys. <lbrakk>length xs = length ys; P xs ys <rbrakk> ...

  45. [2021]

    Association for Computational Linguistics. 10

  46. [2024]

    14 A Dataset Examples In this section, we present examples of datasets from MIRB that are not included in the main text

    Association for Computational Linguistics. 14 A Dataset Examples In this section, we present examples of datasets from MIRB that are not included in the main text. Table 11: MO Dup. Question Retrieval example. Query Relevant Document On finite subsets of set of integers, which...

Pith tools

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