本文介绍了一种新的逐步方法 NLProofS，通过在给定假设的条件下学习生成相关步骤，从而在 NLP 中解决证明生成的问题，并在 EntailmentBank 上取得了最先进的性能。
May, 2022
本文探讨了基于 Transformer 的语言模型在自动定理证明中的应用，提出了基于语言模型的生成能够解决自动定理证明器与人类相比的主要限制之一 —— 原始数学术语的生成问题。我们提出了一个自动证明器和证明辅助工具 GPT-f，使用 Metamath 形式语言，并分析了其性能。 GPT-f 发现了新的简短证明，并被采纳为正式数学社区所接受，这是我们所知道的第一次基于深度学习的系统为正式数学社区做出的贡献。
Sep, 2020
LEGO-Prover 使用技能库，通过模块化构建证明以及生成新技能，提高了大型语言模型在定理证明中的能力，并进一步推进了数学领域的研究。
Oct, 2023
基于大规模合成数据，使用 Lean 4 proof 数据生成方法，我们的模型在定理生成和解决题目方面取得了卓越的成果，证明了合成数据对提高 LLMs 中的定理证明能力的潜力。
May, 2024
提出了一种定理证明算法，该算法使用几乎没有领域启发式来指导其连接风格的证明搜索，而是运行许多蒙特卡罗模拟，通过强化学习来指导以前的证明尝试。
May, 2018
本文提出了 POET，一种新颖的推理预训练范式，使用程序及其执行结果对语言模型进行预训练，可以显著提高自然语言推理的模型性能，包括数字推理、逻辑推理和多跳推理。
Jan, 2022
本研究介绍了一种基于 Universal Transformer 体系结构的语义解析方法，可以将基本数学证明转化为 Coq 互动定理证明器中的等效形式，以及将装饰有 Hoare 三元组的简单命令式代码翻译成 Coq 中的形式验证证明。通过人工和人工写作证明的有限领域的实验表明，这些模型对于训练期间未看到的中间长度和自然语言变化具有很好的泛化能力。
Jan, 2023
DS-Prover 是一个用于定理证明的创新动态抽样方法，通过根据剩余时间和总分配时间来调整探索和开发之间的平衡，以提高证明搜索过程的效率，并通过拆分简化和重写策略为具有单个前提的策略来扩充训练数据集，从而在 MiniF2F 和 ProofNet 两个标准数据集上实现了显著的性能提升。
Dec, 2023
通过人工提供或查找背景参考条件，NaturalProver 能够生成数学证明，融合符号和自然语言，提高了下一步建议和生成证明的质量，在某些需要短证明的定理上具有证明能力，并且提供的下一步建议有超过 40% 的正确和有用率。
这篇论文展示了一个名为 ProofWriter 的生成模型，能够可靠地生成一个理论的两个蕴含和支持它们的自然语言证明，具有高精度的缺少检测性能，能够大幅提高神经方法用于自然语言推理的可行性。
Dec, 2020