MathNLP @ EMNLP 2026 Workshop paper WorkshopForthcoming

NaturalPRISM: A Natural Language Premise Retrieval Task for Research-level Intermediate Proof States

Harris Proctor, Li An, Austin LaHue, Michael Burr, Carlos Toxtli-Hernández, Vinita Gangaram Jansari, Luis David Garcia Puente, Benjamin E. Nye

Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026), 2026

Website

Abstract

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.

Cite this work

Harris Proctor, Li An, Austin LaHue, Michael Burr, Carlos Toxtli-Hernández, Vinita Gangaram Jansari, Luis David Garcia Puente, and Benjamin E. Nye. 2026. NaturalPRISM: A Natural Language Premise Retrieval Task for Research-level Intermediate Proof States. Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026).

@inproceedings{Proctor2026NaturalPRISM,
  title = {NaturalPRISM: A Natural Language Premise Retrieval Task for Research-level Intermediate Proof States},
  author = {Proctor, Harris and An, Li and LaHue, Austin and Burr, Michael and Toxtli-Hernandez, Carlos and Jansari, Vinita Gangaram and Garcia Puente, Luis David and Nye, Benjamin E.},
  booktitle = {Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026)},
  address = {Budapest, Hungary},
  publisher = {Association for Computational Linguistics},
  year = {2026},
  month = October,
  note = {Forthcoming},
  url = {https://sites.google.com/view/mathnlp2026}
}

Related

Related publications