As AI use progresses in research-level mathematics, automated information retrieval systems for constructing relevant prompts are increasingly important. Existing benchmarks and datasets for identifying which prior results are necessary to prove a statement do not align well with current workflows in which a natural language proof is in progress, but it is unclear what the next step(s) should be.

We introduce NaturalPRISM, a benchmark task and dataset containing 1.7 million pairs of intermediate proof states and the premise invoked in the next step of the proof. All pairs are extracted from natural language research-level mathematics papers published on arXiv, and span all 32 subject categories.

We evaluate the effect of fine-tuning retrieval models for domain-specific vs. domain-agnostic use cases, and find that the combination of sufficient training data with alignment between the training and testing distributions allows smaller specialized models to dramatically outperform larger general models.