mlsanityData to 14 Oct 2026

MIRB: Mathematical Information Retrieval Benchmark

arXiv 2505.15585 ↗First posted 21 May 2025cs.IR cs.CL cs.LGcited by 6

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. Cited by 6 papers in the map (data through 14 Oct 2026). Builds on 30 of its 50 references that are in the map. First posted on arXiv 21 May 2025.

Builds on

30 of 50 references.

References · 30

  1. 2022Text Embeddings by Weakly-Supervised Contrastive Pre-trainingcited by 1,253
  2. 2021BEIR: A Heterogenous Benchmark for Zero-shot Evaluation of Information Retrieval Modelscited by 1,252
  3. 2024M3-Embedding: Multi-Linguality, Multi-Functionality, Multi-Granularity Text Embeddings Through Self-Knowledge Distillationcited by 1,073
  4. 2023Towards General Text Embeddings with Multi-stage Contrastive Learningcited by 723
  5. 2019CodeSearchNet Challenge: Evaluating the State of Semantic Code Searchcited by 654
  6. 2022MTEB: Massive Text Embedding Benchmarkcited by 640
  7. 2023C-Pack: Packed Resources For General Chinese Embeddingscited by 578
  8. 2024NV-Embed: Improved Techniques for Training LLMs as Generalist Embedding Modelscited by 472
  9. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  10. 2022Text and Code Embeddings by Contrastive Pre-Trainingcited by 361
  11. 2022One Embedder, Any Task: Instruction-Finetuned Text Embeddingscited by 333
  12. 2023Improving Text Embeddings with Large Language Modelscited by 303
18 more
  1. 2024Generative Representational Instruction Tuningcited by 233
  2. 2024BRIGHT: A Realistic and Challenging Benchmark for Reasoning-Intensive Retrievalcited by 158
  3. 2025MMTEB: Massive Multilingual Text Embedding Benchmarkcited by 125
  4. 2024Gecko: Versatile Text Embeddings Distilled from Large Language Modelscited by 83
  5. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 81
  6. 2021CoSQA: 20,000+ Web Queries for Code Search and Question Answeringcited by 75
  7. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  8. 2024CoIR: A Comprehensive Benchmark for Code Information Retrieval Modelscited by 60
  9. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  10. 2024LongEmbed: Extending Embedding Models for Long Context Retrievalcited by 48
  11. 2023xCodeEval: A Large Scale Multilingual Multitask Benchmark for Code Understanding, Generation, Translation and Retrievalcited by 47
  12. 2024RAR-b: Reasoning as Retrieval Benchmarkcited by 36
  13. 2024A Semantic Search Engine for Mathlib4cited by 31
  14. 2017HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Provingcited by 26
  15. 2024MAIR: A Massive Benchmark for Evaluating Instructed Retrievalcited by 23
  16. 2024ChemTEB: Chemical Text Embedding Benchmark, an Overview of Embedding Models Performance & Efficiency on a Specific Domaincited by 12
  17. 2022Evaluating Token-Level and Passage-Level Dense Retrieval Models for Math Information Retrievalcited by 9
  18. 2024Mathematical Information Retrieval: Search and Question Answeringcited by 3

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 2; 2026: 4.

6 papers.

  1. 2026LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Provingcited by 10
  2. 2025Lean Finder: Semantic Search for Mathlib That Understands User Intentscited by 8
  3. 2025StatEval: A Comprehensive Benchmark for Large Language Models in Statisticscited by 6
  4. 2026GraphPO: Graph-based Policy Optimization for Reasoning Modelscited by 3
  5. 2026Does My Embedding Reflect That A = B? Evaluating Mathematical Equivalence in Embedding Modelscited by 3
  6. 2026Recipe-Matching, Not Equivalencecited by 0