@inproceedings{proctor-etal-2026-naturalprism,
title = "{N}atural{PRISM}: 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
Jansari, Vinita Gangaram and
Hernandez, Carlos Toxtli and
Puente, Luis David Garcia and
Nye, Benjamin E",
editor = "Valentino, Marco and
Ferreira, Deborah and
Thayaparan, Mokanarangan and
Ranaldi, Leonardo and
Cheng, Jo-Ku and
Freitas, Andre",
booktitle = "The Proceedings of the 4th Workshop on Mathematical Natural Language Processing ({M}ath{NLP} 2026)",
month = oct,
year = "2026",
address = "Budapest, Hungary",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2026.mathnlp-main.13/",
pages = "167--176",
ISBN = "979-8-89176-468-2",
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.\par 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.\par 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."
}<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="proctor-etal-2026-naturalprism">
<titleInfo>
<title>NaturalPRISM: A Natural Language Premise Retrieval Task for Research-level Intermediate Proof States</title>
</titleInfo>
<name type="personal">
<namePart type="given">Harris</namePart>
<namePart type="family">Proctor</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Li</namePart>
<namePart type="family">An</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Austin</namePart>
<namePart type="family">LaHue</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Michael</namePart>
<namePart type="family">Burr</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Vinita</namePart>
<namePart type="given">Gangaram</namePart>
<namePart type="family">Jansari</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Carlos</namePart>
<namePart type="given">Toxtli</namePart>
<namePart type="family">Hernandez</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Luis</namePart>
<namePart type="given">David</namePart>
<namePart type="given">Garcia</namePart>
<namePart type="family">Puente</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Benjamin</namePart>
<namePart type="given">E</namePart>
<namePart type="family">Nye</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<originInfo>
<dateIssued>2026-10</dateIssued>
</originInfo>
<typeOfResource>text</typeOfResource>
<relatedItem type="host">
<titleInfo>
<title>The Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026)</title>
</titleInfo>
<name type="personal">
<namePart type="given">Marco</namePart>
<namePart type="family">Valentino</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Deborah</namePart>
<namePart type="family">Ferreira</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Mokanarangan</namePart>
<namePart type="family">Thayaparan</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Leonardo</namePart>
<namePart type="family">Ranaldi</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Jo-Ku</namePart>
<namePart type="family">Cheng</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Andre</namePart>
<namePart type="family">Freitas</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<originInfo>
<publisher>Association for Computational Linguistics</publisher>
<place>
<placeTerm type="text">Budapest, Hungary</placeTerm>
</place>
</originInfo>
<genre authority="marcgt">conference publication</genre>
<identifier type="isbn">979-8-89176-468-2</identifier>
</relatedItem>
<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.\par 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.\par 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.</abstract>
<identifier type="citekey">proctor-etal-2026-naturalprism</identifier>
<location>
<url>https://aclanthology.org/2026.mathnlp-main.13/</url>
</location>
<part>
<date>2026-10</date>
<extent unit="page">
<start>167</start>
<end>176</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T NaturalPRISM: A Natural Language Premise Retrieval Task for Research-level Intermediate Proof States
%A Proctor, Harris
%A An, Li
%A LaHue, Austin
%A Burr, Michael
%A Jansari, Vinita Gangaram
%A Hernandez, Carlos Toxtli
%A Puente, Luis David Garcia
%A Nye, Benjamin E.
%Y Valentino, Marco
%Y Ferreira, Deborah
%Y Thayaparan, Mokanarangan
%Y Ranaldi, Leonardo
%Y Cheng, Jo-Ku
%Y Freitas, Andre
%S The Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026)
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-468-2
%F proctor-etal-2026-naturalprism
%X 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.\par 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.\par 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.
%U https://aclanthology.org/2026.mathnlp-main.13/
%P 167-176
Markdown (Informal)
[NaturalPRISM: A Natural Language Premise Retrieval Task for Research-level Intermediate Proof States](https://aclanthology.org/2026.mathnlp-main.13/) (Proctor et al., MathNLP 2026)
ACL
- Harris Proctor, Li An, Austin LaHue, Michael Burr, Vinita Gangaram Jansari, Carlos Toxtli Hernandez, Luis David Garcia Puente, and Benjamin E Nye. 2026. NaturalPRISM: A Natural Language Premise Retrieval Task for Research-level Intermediate Proof States. In The Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026), pages 167–176, Budapest, Hungary. Association for Computational Linguistics.