发生了什么？
Deborah Ferreira 与 André Freitas 提出自然语言前提选择任务：系统接收由数学文字与公式共同表达的 conjecture，并检索最可能支持其证明的定义或命题；作者同时发布源自 ProofWiki 的数据集与可复现的数据抽取流程。
为什么重要？
参考资料选择是非形式与形式数学推理中的共同瓶颈。该工作直接在面向人类的数学文本上定义 benchmark，为更早的形式化 premise selection 研究通向后来 NaturalProofs 式检索与参考资料约束的证明生成提供了桥梁。
重要性说明：Natural Language Premise Selection 将从普通数学文本中检索相关定义与命题明确建模为机器学习任务，并发布源自 ProofWiki 的评测数据集。它为同时处理数学自然语言与公式的推理提供了较早 benchmark，并早于后来的自然语言定理证明数据集与 grounded proof generation 系统。
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- 仅计算支持
- 形式保障
- 有形式化工件
如何理解这些标签？ →
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 非形式化, 符号
- AI 贡献
- 机器学习与检索模型被训练和评测，用于排序与证明相关的数学陈述；任务定义、ProofWiki 数据抽取与相关性关系由研究者从既有人工数学材料中构建。
- 人类贡献
- 研究者定义任务、构建源自 ProofWiki 的语料与抽取管线、设计评测划分和基线，并分析从数学文字与公式混合语篇中检索相关前提的难点。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-15
技术细节
- 系统
- nl-ps, ps-proofwiki
- 机构
- university-of-manchester
- 数学问题
- natural-language-premise-selection
- 方法
- premise-selection, information-retrieval, mathematical-language-processing, dataset-construction
