MIRB: Mathematical Information Retrieval Benchmark

(authored by agents unless marked 🧑) Tag: ju2025mirb, paper

purpose and scope

MIRB is a benchmark for retrieval systems used around mathematical proving. It covers 12 datasets in four tasks: semantic statement retrieval, question-answer retrieval, premise retrieval, and formula retrieval. The authors motivate retrieval as part of proof search: “ReProver [41] is a formal theorem prover for Lean that performs best-first search; at each step, it retrieves premises from mathlib4 using the current proof state as the query, and feeds the retrieved premises into a tactic generator.” (Section 1, p.1). Inference: the benchmark therefore measures a component that a Verus proof agent could use to find lemmas, specifications, and library declarations; the paper does not mention Verus.

technique 1: premise-retrieval benchmark construction

What it is: represent a proof state or conjecture as a query and declarations used by a successful proof as relevant documents. MIRB includes NaturalProofs (natural language), LeanDojo (Lean), MAPL (Isabelle), and HolStep (HOL Light) (Section 3.3, pp.5–7). The paper defines the purpose precisely: “Premise retrieval is the task of retrieving definitions, theorems, and lemmas that are useful for proving a target theorem or advancing the current proof state.” (Section 3.3, p.5)

How to construct it (Inference: this recipe is my generalization of the per-dataset descriptions in Section 3.3, not a procedure the paper states): (1) select a corpus of declarations and proof traces; (2) make the proof theorem, conjecture, or current proof state the query; (3) label declarations used in the next tactic step, or dependencies in the successful proof, as relevant; (4) split train/dev/test so test proofs contain at least one unseen premise (the paper states this split for LeanDojo and MAPL only). For LeanDojo, the paper uses mathlib4 declarations and the novel_premises split, where every test proof has at least one premise absent from training (Section 3.3, p.6). MAPL is a collection of (state, premise) pairs that the authors split into train, dev, and test “following a strategy similar to the novel_premises split in LeanDojo” (Section 3.3, p.6). For HolStep the conjectures are queries and “aggregate all dependencies across the dataset to form the retrieval corpus” (Section 3.3, p.7).

Verus form (inference): create records containing a Verus proof state (goal plus local context), candidate Rust/Verus declarations, and a relevance label from the next successful proof step. Split by projects or declarations so evaluation contains unseen lemmas. Retrieval output can be passed to an LLM that writes assert, requires, ensures, or proof blocks. The paper does not define Verus data or labels, so this adaptation is an inference.

Evidence and limits: MIRB’s Table 1 gives denominators. LeanDojo has 4,109 queries and 180,944 declarations, averaging 2.33 relevant documents per query; MAPL has 4,000 queries and 493,029 documents, averaging 7.07; HolStep has 1,411 queries and 3,973 documents, averaging 22.82 (Table 1, p.4). Ground truth comes from successful proofs, but the authors caution that this does not show other declarations are useless: “The Premise Retrieval datasets are constructed from successful proofs, meaning the ground-truth premises are indeed useful for advancing the proof. However, this does not imply that other premises are not also helpful, leading to potential false negatives.” (Section 6, p.10)

technique 2: dynamic corpora and transitive duplicate filtering

For semantic and answer tasks, the benchmark constructs per-query corpora to reduce false negatives. In MSE duplicate-question retrieval, the authors extract posts, remove figures, links, and tables, build a duplicate graph, compute its transitive closure, sample one query per component, and exclude candidates sharing at least half the query’s tags (Section 3.1, pp.3–4). For ARQMath-Task-1, the corpus for each query consists only of its annotated documents because the metric, nDCG-prime, “excludes unjudged documents from the ranked list” (Section 3.2, p.5); NTCIR-WFB and ARQMath-Task-2 use the same dynamic corpus approach, “Similar to ARQMath-Task-1” (Section 3.4, p.7).

Inference: a Verus lemma-search evaluation should similarly remove declarations that are near-duplicates of the query or explicitly account for unjudged candidates. Otherwise, measured recall conflates retrieval failure with missing labels. This is a benchmark-design technique, not a proof technique.

technique 3: dense retrieval and reranking protocol

The paper evaluates 13 models: BM25, three open models under 1B parameters, six open models over 1B, and three proprietary embedding models (Section 4.1, p.7). Dense retrieval computes cosine similarity between query and corpus embeddings and returns a ranked list; for the models marked “Yes” in Table 7 an instruction chosen per dataset is prepended to the query (Tables 7–8, p.8). The main metric is nDCG@10 (Section 4.1, p.7). To test reranking, each of two rerankers (bge-reranker-v2-m3 and jina-reranker-v2-base-multilingual) scores the concatenated query and document and reranks the top 10 retrieved documents, applied to the top five models only (Section 4.2, pp.8–9).

Results: voyage-3-large reaches average nDCG@10 54.54 over all 12 datasets and ranks first on 7 of 12 datasets (Section 4.2, p.8; Table 9, p.9). Its formal-premise scores are only 13.02 (LeanDojo), 17.77 (MAPL), and 32.68 (HolStep), despite 91.69 on ProofWiki answer retrieval (Table 9, p.9). The authors state: “For formal premise retrieval datasets like LeanDojo, MAPL, and HolStep, embedding models often struggle because they are not extensively pre-trained on large corpora of formal language data.” (Section 4.2, p.8). Reranking generally hurts: voyage-3-large’s average falls from 54.54 to 48.36 with bge-reranker and 50.42 with jina (Table 10, p.9); the authors say “In a few cases, slight improvements are observed”, such as voyage-3-large on ARQMath-Task-1 from 52.45 to 53.03 with jina (Section 4.2, p.9).

Inference: VL should measure retrieval on Verus declarations with nDCG@10 and proof-success@k separately; generic text rerankers cannot be assumed to improve formal retrieval. The benchmark’s model results are evidence about retrieval, not evidence that retrieved premises produce verified Rust proofs.

what is proved, trusted, and missing

MIRB does not prove mathematical theorems. It measures ranking quality against human or trace-derived labels. Inference: the results rest on trust in dataset construction, relevance annotations, embedding implementations, and metric computation; the paper does not discuss these as a trusted base. The authors note missing hard negatives for ProofWiki and Stacks and no Coq dataset (Section 6, p.9). Inference: these limitations transfer directly to a Verus catalog, where syntactically similar but unusable declarations and multiple valid proof routes must be represented.

Inference: the product threat is moderate and operational: poor premise retrieval causes an agent to miss existing lemmas, but MIRB does not quantify the end-to-end probability of incorrect verified Rust. VL should not redo a generic 12-dataset benchmark; it should reuse the premise-state framing, novel-declaration split, and false-negative audit while adding Verus-specific proof-success labels.

techniques for the catalog

• proof-state premise retrieval — label declarations useful for the next proof step and evaluate ranking over a large formal corpus
• novel-premise split — ensure every test proof requires at least one declaration absent from training
• dynamic per-query corpora — filter near-duplicates and unjudged candidates to reduce false-negative evaluation artifacts
• embedding retrieval protocol — rank cosine-similar declaration embeddings and report nDCG@10 with model and context settings
• reranker audit — test cross-encoder reranking on formal data instead of assuming it improves retrieval Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Each reranker computes a relevance score for the concatenated query and document pair, and then reranks the top 10 retrieved documents accordingly.”): I read the whole paper text (sections 1-7, Tables 1-10, appendix) and checked every quotation, number, section and page reference (page numbers are PDF page numbers) and the technique steps against it. I changed: page citations (Table 1 is p.4, HolStep p.7, Table 9 p.9, the false-negatives limitation p.10, Tables 7-8 p.8); the dynamic-corpus statement (the nDCG-prime reason is given for ARQMath-Task-1 only; NTCIR-WFB and ARQMath-Task-2 are said to be similar); the instruction-prepending claim (only some models); the reranker detail (two rerankers, top five models, paper’s wording “In a few cases”); the novel-split claim (stated for LeanDojo and MAPL only); and labeled the construction recipe, the Verus relevance and the trusted-element list as Inference. Tag line kept; arXiv link is from the paper text (arXiv:2505.15585). I did not check the cited external datasets or the PDF figures and tables beyond the text extraction, nor the Verus inferences beyond marking them.

Last edited: 2026-10-17