核心发现
方法论
论文构建NaturalProofs，并将定理证明转化为参考结果检索与序列生成。模型包括TF-IDF、BERT Pairwise、BERT Joint及Autoregressive生成器。Pairwise用点积评分并以负采样训练；Joint以softmax计算全部参考的联合分布；生成器按p(r_t|r_<t,x)预测引用顺序、重复次数及结束符。
关键结果
- 在ProofWiki上，按源训练的BERT Joint达到mAP 36.75、R@10 42.45、R@100 75.90、Full@100 50.22，明显优于TF-IDF的6.19、10.27、23.09和9.43。
- 在Stacks上，BERT Joint取得mAP 28.32、R@10 39.10和Full@100 65.59；但教材零样本中，Real Analysis上的TF-IDF mAP为15.79，优于ProofWiki训练的BERT Joint 11.24。
- 生成任务较困难：Stacks上Autoregressive精确匹配仅3.87%，ProofWiki为3.69%；这说明模型虽能找到相关结果，却难以同时恢复引用集合、顺序和次数。
研究意义
NaturalProofs把人类实际使用的“自然语言加数学符号”纳入可复现实验，连接了形式化证明、信息检索与语言模型研究。它不只测试模型是否能匹配词面，还检验模型能否识别证明所需的关键定理、定义和公理。多领域及教材零样本设置揭示：强大的领域内分数并不等于数学知识迁移能力，为教育辅助、科学检索和自动化推理提供了更现实的评测基础。
技术贡献
论文提出统一数据模式、引用图和叶节点划分策略，避免测试定理已作为训练引用而造成泄漏。方法上比较独立评分的Pairwise模型与一次性建模全部候选的Joint模型，并将参考内容编码器预训练表示注入候选矩阵；同时提出自回归引用生成。检索指标包括mAP、R@k和Full@k，生成则评估精确匹配、编辑距离、BLEU、集合及多重集合恢复。
新颖性
相较只覆盖ProofWiki或形式系统的既有资源，NaturalProofs首次以统一模式整合ProofWiki、Stacks及两本教材，兼顾广覆盖、深覆盖和低资源真实文本。其核心新意不是提出全新神经架构，而是把自然数学中的“证明引用选择”定义为可量化的检索和生成任务，并提供严格的跨域、零样本协议。
局限性
- 模型容易检索主题相关但并未出现在真实证明中的结果；Category of Monoids案例显示，Joint虽改善排序，仍不能稳定区分“相关”与“证明必需”。
- BERT在教材零样本上没有超过TF-IDF，说明词面差异、LaTeX格式和领域分布变化会削弱迁移；生成器精确匹配率也很低。
- 数据依赖网页和教材中的显式引用链接，未必覆盖隐含推理、等价改写或未标注的数学依据。
未来方向
未来应结合符号结构、证明图、数学实体对齐和形式化验证，减少仅凭词面检索。可研究跨域预训练、少样本教材适配、图神经网络及检索—生成联合训练，并让生成的引用序列经过Lean、Mizar或其他证明助手验证。
AI 总览摘要
数学证明并不是公式计算的简单延伸。人类常常用自然语言、符号和既有定理共同组织论证，但多数自动定理证明研究依赖Lean、Mizar或Metamath等形式系统，难以刻画真实数学文本。NaturalProofs针对这一缺口，收集ProofWiki、Stacks代数几何项目，以及Real Analysis和Number Theory两本教材，形成约3.2万个定理、1.4万个定义和2千个其他页面的多领域语料库。
作者把证明理解为“寻找关键参考结果”的过程：给定定理，系统需要检索证明中实际出现的定理、定义或公理，进一步还要按正确顺序生成它们。基准比较TF-IDF、BERT Pairwise、BERT Joint和自回归模型。Joint模型一次性学习候选引用之间的竞争，在ProofWiki上mAP从Pairwise的16.82提升至36.75，R@10达到42.45，Top-100完整覆盖率达到50.22；Stacks上Full@100为65.59。
然而，结果也揭示了重要边界。教材零样本测试中，Real Analysis的TF-IDF mAP为15.79，高于ProofWiki训练BERT Joint的11.24；引用序列精确生成率在ProofWiki和Stacks分别只有3.69%和3.87%。因此，NaturalProofs的价值不仅在于提高分数，更在于建立了现实的测试：模型能否从相关知识中找出真正支撑证明的知识，并跨越学科、格式和写作风格迁移。它为自然数学理解、教育工具和自动化科学推理提供了基础，但完整可靠的证明仍需要符号推理与形式验证。
深度分析
研究背景
形式化数学研究已在HOL Light、Coq、Lean、Mizar和Metamath中取得进展，Premise Selection和HOList等工作证明神经模型能够帮助自动证明器选取假设。然而人类数学通常混合自然语言、LaTeX和上下文省略。ProofWiki等自然文本资源曾被用于前提选择，但多集中于单一来源，缺少跨领域、低资源和零样本评测。
核心问题
给定定理x及候选集合R，系统需找出其证明引用序列y=(r1,…,r|y|)。检索要求恢复引用集合；生成还要求正确预测数量、顺序和重复项。难点包括候选规模约4.6万个、数学词面变化、隐含结构、引用图依赖，以及测试定理不能出现在训练引用中的严格泛化要求。
核心创新
NaturalProofs统一三类来源：ProofWiki提供广覆盖，Stacks提供代数几何深覆盖，教材提供低资源真实文本。作者把所有页面组织为引用图，并以叶节点构造评测集，降低图泄漏。任务设计同时覆盖集合检索和序列生成，指标从mAP、R@10到Full@100，因而能区分“找到相关结果”和“完整支撑证明”。
方法详解
- �� 数据：抽取标题、混合文本与LaTeX、证明及显式引用，得到约25k个可用定理—证明样本，候选引用约46k。
- �� Pairwise：BERT分别编码定理和引用，使用点积sθ(x,r)，对正例与负例优化softmax对比损失。
- �� Joint：用候选矩阵R与定理向量fθ(x)计算softmax(Rfθ(x))；矩阵可使用独立引用编码器表示。
- �� Generation：自回归模型按pθ(rt|r<t,x)生成引用并以EOS结束，可用beam search解码。
- �� 评估：按来源内训练测试，并在RA、NT教材上进行零样本测试。
实验设计
主实验比较Random、Frequency、TF-IDF及BERT模型。P/S表示按单一来源训练，P+S表示ProofWiki与Stacks联合训练。检索使用mAP、微平均R@10/R@100和Full@10/Full@100；生成使用EM、编辑距离、BLEU、集合F1和多重集合F1。实验还比较Pairwise与Joint，并用集合、无序多重集合和前半序列oracle分析错误来源。
结果分析
ProofWiki上BERT P/S Joint的mAP为36.75，较Pairwise的16.82大幅提升；R@10为42.45，Full@100为50.22。Stacks对应mAP 28.32、R@10 39.10、Full@100 65.59。联合训练模型仍具竞争力，但单域模型通常更强。零样本时TF-IDF在Real Analysis达到mAP 15.79，高于BERT Joint 11.24，显示领域迁移仍未解决。
应用场景
系统可作为数学检索助手：输入一个定理，返回可能支撑证明的关键结果，帮助学生定位先修知识、帮助研究者浏览大型文献库。它也可作为自动证明器的前端，为Lean、Mizar等系统提供候选前提。实际部署需有结构化引用、领域词表和人工或形式化验证，以避免把“主题相关”误当作“证明必要”。
局限与展望
NaturalProofs依赖显式链接，无法完整表示没有引用标记的隐含推理。BERT主要依赖文本表示，对变量、等价公式和长程依赖的处理有限。候选集合大时Joint计算和表示学习成本上升；自回归生成还存在曝光偏差、错误累积和低精确匹配。未来需融合引用图、符号执行、跨域适配和证明助手验证。
通俗解读 非专业人士也能看懂
把数学证明想成一名图书管理员帮助你写报告。书架上有四万多本“知识卡片”，每张卡片可能是定理、定义或公理。你给他一个问题，他首先要找出真正用到的卡片，而不是只找主题相似的卡片。TF-IDF像按关键词查目录；BERT像读懂问题和卡片的意思；Pairwise逐张比较，Joint则把所有卡片放在一起排序。NaturalProofs还要求管理员把卡片按报告中的使用顺序念出来。
结果显示，Joint在ProofWiki中能把约42%的正确卡片放进前十名，并在前一百名中完整覆盖约一半证明所需卡片。但如果换成不同教材，普通关键词方法有时反而更好。这就像管理员熟悉网上百科，却不一定看得懂教授使用的另一套教材。研究说明，找到“相关资料”与找到“证明真正需要的资料”是两件事；真正可靠的数学助手还必须理解逻辑关系，并检查这些卡片是否真的能拼成完整证明。
简单解释 像给14岁少年讲一样
想象你在玩一款解谜游戏：每关都有一个看起来很难的任务，背包里有成千上万张技能卡。要通关，你不只要找“看起来像有用”的卡，还要找出真正能完成任务的卡，并按正确顺序使用。数学证明也差不多：定理是任务，其他定理和定义是技能卡。
NaturalProofs给电脑看了很多真实数学材料，包括ProofWiki、Stacks和两本教材。电脑先学习哪些卡片可能有关。BERT像一个读题很快的助手；Pairwise一次比较一张卡，Joint像把所有卡摊在桌上一起排名。还有一个生成模型，尝试直接说出证明会用哪些卡。
电脑在熟悉的材料上表现不错：ProofWiki中，Joint模型前十个答案里平均包含约42%的正确引用，前一百个答案能覆盖完整证明所需引用的比例约为50%。但换到新教材时，它会失灵，有时简单的关键词搜索反而更好。为什么？因为数学家可能用完全不同的说法表达同一个想法。
所以这项研究不是说电脑已经会证明数学了，而是建立了一场公平考试：电脑能不能找到真正需要的知识？下一步要让它理解符号、逻辑和证明步骤，并用证明软件检查答案。这样它才可能成为可靠的学习伙伴，而不只是会推荐“看起来相关”的页面！
术语表
Natural mathematical language（自然数学语言）
人类实际书写数学时使用的自然语言、符号和LaTeX的混合形式。它比纯形式语言更接近教材和论文。
NaturalProofs的全部文本表示。
Reference retrieval（参考结果检索）
给定定理，从候选定理、定义和其他页面中找出其证明实际引用的项目。目标通常是恢复集合而非生成完整证明。
论文的主要基准任务。
Pairwise parameterization（成对参数化）
独立计算定理x与引用r的匹配分数，再用正负样本训练。它便于使用BERT编码内容，但不能直接建模候选之间的竞争。
与Joint模型比较。
Joint parameterization（联合参数化）
一次性对所有候选引用计算softmax概率。它能优化完整候选分布，并改善排名顶部质量。
ProofWiki和Stacks中表现最佳的检索方法。
Full@k（前k项完整恢复率）
预测排名前k项包含证明全部真实引用的样本比例。该指标比普通Recall更严格。
衡量是否足以支持完整证明。
Zero-shot generalization（零样本泛化）
模型不使用目标领域训练样本，直接在新来源上测试。它衡量跨文本风格和数学领域迁移能力。
RA和NT教材评测。
开放问题 这项研究留下的未解疑问
- 1 模型如何识别等价但词面完全不同的数学表达？当前BERT和TF-IDF都容易受写作风格影响，需要符号规范化与数学实体对齐。
- 2 检索到的引用是否真的能组成有效证明？论文只评估引用匹配，没有普遍使用形式验证器检查逻辑闭合。
- 3 如何在数万候选中联合理解长证明、图结构和隐含前提，同时保持可接受计算成本，仍缺少成熟方案。
应用场景
近期应用
数学学习检索助手
学生输入一个定理，系统从教材或ProofWiki中返回可能用到的定义和先验定理，并显示相关性排名。教师可将其作为提示工具，但应人工核对，因为模型可能推荐主题相关而非证明必需的结果。
形式化证明前提筛选
在调用Lean、Mizar或其他证明器前，NaturalProofs式模型可先从大型库中筛选候选前提，减少搜索空间。实际使用需要把自然语言结果映射到形式声明，并由证明器最终验证。
远期愿景
跨领域数学研究助理
结合引用图、符号推理和形式验证后，系统可跨教材、论文与知识库迁移，帮助研究者发现证明依赖、补齐背景知识并提出可检查的证明草案。主要障碍是隐含推理和可靠性。
原文摘要
Understanding and creating mathematics using natural mathematical language - the mixture of symbolic and natural language used by humans - is a challenging and important problem for driving progress in machine learning. As a step in this direction, we develop NaturalProofs, a multi-domain corpus of mathematical statements and their proofs, written in natural mathematical language. NaturalProofs unifies broad coverage, deep coverage, and low-resource mathematical sources, allowing for evaluating both in-distribution and zero-shot generalization. Using NaturalProofs, we benchmark strong neural methods on mathematical reference retrieval and generation tasks which test a system's ability to determine key results that appear in a proof. Large-scale sequence models show promise compared to classical information retrieval methods, yet their performance and out-of-domain generalization leave substantial room for improvement. NaturalProofs opens many avenues for research on challenging mathematical tasks.