证明助手中的自然语言规格说明
该论文表明，通过使用现有的证明助理，可以以与建立证明助理自身的信任和可审计性原则相一致的方式，构建对自然语言表达的规范的支持。我们在 Lean 证明助理内实现了一种方式，以可扩展的正式英语子集提供规范，并自动将其翻译成正式的命题。我们的方法是可扩展的（对语法结构没有永久限制），模块化的（允许在库中分发有关新词的信息），并且生成解释了每个词的解释方式以及如何使用句子结构来计算含义的证明证书。我们将原型应用于从一本流行教材中翻译各种正式规范的英文描述；在仅需进行小幅修改的情况下，借助一个适度的词汇表，所有规范都能被正确翻译。
Oct, 2023
NaturalProofs 是一个使用自然数学语言编写数学命题和证明的多域语料库，可用于评估系统在数学参考检索和生成任务中确定证明中出现的关键结果的能力，并提供了许多研究理解和创建自然数学语言的挑战性数学任务的新途径。
Mar, 2021
本文提出了使用机器学习自动化证明助手交互的问题。研究人员通过构建 CoqGym 数据集和 ASTactic 模型，能够生成高效的策略程序并用于自动证明定理。
May, 2019
通过人工提供或查找背景参考条件，NaturalProver 能够生成数学证明，融合符号和自然语言，提高了下一步建议和生成证明的质量，在某些需要短证明的定理上具有证明能力，并且提供的下一步建议有超过 40% 的正确和有用率。
May, 2022
本研究介绍了一种基于 Universal Transformer 体系结构的语义解析方法，可以将基本数学证明转化为 Coq 互动定理证明器中的等效形式，以及将装饰有 Hoare 三元组的简单命令式代码翻译成 Coq 中的形式验证证明。通过人工和人工写作证明的有限领域的实验表明，这些模型对于训练期间未看到的中间长度和自然语言变化具有很好的泛化能力。
Jan, 2023
本文介绍了一种新的逐步方法 NLProofS，通过在给定假设的条件下学习生成相关步骤，从而在 NLP 中解决证明生成的问题，并在 EntailmentBank 上取得了最先进的性能。
May, 2022
我们提出利用形式证明来推进几个可解释的自然语言推理（NLI）任务的方法，并利用可靠和高性能的基于逻辑的 NLI 系统生成形式证明。通过利用生成的形式证明中的深度信息，我们展示了如何使用它来定义具有结构化解释的 NLI 任务。所提出的任务可以根据解释的粒度难度进行排序，并且我们认为这些任务在许多方面都比现有的可解释 NLI 任务（或数据集）具有更少缺陷。
Nov, 2023
本篇论文介绍了一种新的多模态、领域无关的方法，结合自然语言编程和演示编程，允许用户在高层次上自然描述任务和相关条件，并通过对话和演示递归地解决任何模糊不清的问题。PUMICE 是一个可供最终用户编程的代理系统，实现了这种方法。10 位用户的实验显示出系统的可用性。
Aug, 2019
本文提出了自然前提选择 (Natural Premise Selection) 这一新型自然语言处理 (NLP) 任务，以便找到能为生成某个语句非正式数学证明提供支持定义和支持命题的前提；此外，我们还提供了一个数据集 NL-PS，用于评估不同方法在此任务上的表现，并使用不同的基线模型来展示了该任务所涉及的基本解释挑战。
Apr, 2020