# MIRB: Mathematical Information Retrieval Benchmark

arXiv: https://arxiv.org/abs/2505.15585 · HTML: https://mlsanity.com/paper/2505.15585/

## 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 (most cited first, 30 of 30)

- [Text Embeddings by Weakly-Supervised Contrastive Pre-training](https://mlsanity.com/paper/2212.03533/) (2022)
- [BEIR: A Heterogenous Benchmark for Zero-shot Evaluation of Information Retrieval Models](https://mlsanity.com/paper/2104.08663/) (2021)
- [M3-Embedding: Multi-Linguality, Multi-Functionality, Multi-Granularity Text Embeddings Through Self-Knowledge Distillation](https://mlsanity.com/paper/2402.03216/) (2024)
- [Towards General Text Embeddings with Multi-stage Contrastive Learning](https://mlsanity.com/paper/2308.03281/) (2023)
- [CodeSearchNet Challenge: Evaluating the State of Semantic Code Search](https://mlsanity.com/paper/1909.09436/) (2019)
- [MTEB: Massive Text Embedding Benchmark](https://mlsanity.com/paper/2210.07316/) (2022)
- [C-Pack: Packed Resources For General Chinese Embeddings](https://mlsanity.com/paper/2309.07597/) (2023)
- [NV-Embed: Improved Techniques for Training LLMs as Generalist Embedding Models](https://mlsanity.com/paper/2405.17428/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Text and Code Embeddings by Contrastive Pre-Training](https://mlsanity.com/paper/2201.10005/) (2022)
- [One Embedder, Any Task: Instruction-Finetuned Text Embeddings](https://mlsanity.com/paper/2212.09741/) (2022)
- [Improving Text Embeddings with Large Language Models](https://mlsanity.com/paper/2401.00368/) (2023)
- [Generative Representational Instruction Tuning](https://mlsanity.com/paper/2402.09906/) (2024)
- [BRIGHT: A Realistic and Challenging Benchmark for Reasoning-Intensive Retrieval](https://mlsanity.com/paper/2407.12883/) (2024)
- [MMTEB: Massive Multilingual Text Embedding Benchmark](https://mlsanity.com/paper/2502.13595/) (2025)
- [Gecko: Versatile Text Embeddings Distilled from Large Language Models](https://mlsanity.com/paper/2403.20327/) (2024)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [CoSQA: 20,000+ Web Queries for Code Search and Question Answering](https://mlsanity.com/paper/2105.13239/) (2021)
- [NaturalProver: Grounded Mathematical Proof Generation with Language Models](https://mlsanity.com/paper/2205.12910/) (2022)
- [CoIR: A Comprehensive Benchmark for Code Information Retrieval Models](https://mlsanity.com/paper/2407.02883/) (2024)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [LongEmbed: Extending Embedding Models for Long Context Retrieval](https://mlsanity.com/paper/2404.12096/) (2024)
- [xCodeEval: A Large Scale Multilingual Multitask Benchmark for Code Understanding, Generation, Translation and Retrieval](https://mlsanity.com/paper/2303.03004/) (2023)
- [RAR-b: Reasoning as Retrieval Benchmark](https://mlsanity.com/paper/2404.06347/) (2024)
- [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024)
- [HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving](https://mlsanity.com/paper/1703.00426/) (2017)
- [MAIR: A Massive Benchmark for Evaluating Instructed Retrieval](https://mlsanity.com/paper/2410.10127/) (2024)
- [ChemTEB: Chemical Text Embedding Benchmark, an Overview of Embedding Models Performance & Efficiency on a Specific Domain](https://mlsanity.com/paper/2412.00532/) (2024)
- [Evaluating Token-Level and Passage-Level Dense Retrieval Models for Math Information Retrieval](https://mlsanity.com/paper/2203.11163/) (2022)
- [Mathematical Information Retrieval: Search and Question Answering](https://mlsanity.com/paper/2408.11646/) (2024)

## Built on by (most cited first, 6 of 6)

- [LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.13137/) (2026)
- [Lean Finder: Semantic Search for Mathlib That Understands User Intents](https://mlsanity.com/paper/2510.15940/) (2025)
- [StatEval: A Comprehensive Benchmark for Large Language Models in Statistics](https://mlsanity.com/paper/2510.09517/) (2025)
- [GraphPO: Graph-based Policy Optimization for Reasoning Models](https://mlsanity.com/paper/2606.18954/) (2026)
- [Does My Embedding Reflect That A = B? Evaluating Mathematical Equivalence in Embedding Models](https://mlsanity.com/paper/2606.23959/) (2026)
- [Recipe-Matching, Not Equivalence](https://mlsanity.com/paper/2609.31927/) (2026)

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