- TPTP 世界中的非经典逻辑自动推理
本文介绍了 TPTP World 的最新扩展，提供用于非经典逻辑推理的语言和基础设施，并与现有 TPTP World 自由衔接
- EMNLP基于神经网络的自然语言逻辑推理统一化
本文提出了一种新的架构 —— 神经单元器，并提出了相应的训练过程，实现了最先进的推理结果，通过模拟一种众所周知的推理过程 —— 向后链接，即使模型只在浅层次的数据上进行训练，也能回答深度问题，并通过使用各种基准数据集进行实验。
- 用于自动定理证明的生成语言建模
本文探讨了基于 Transformer 的语言模型在自动定理证明中的应用，提出了基于语言模型的生成能够解决自动定理证明器与人类相比的主要限制之一 —— 原始数学术语的生成问题。我们提出了一个自动证明器和证明辅助工具 GPT-f，使用 Met - ICLRINT: 一个不等式基准用于评估定理证明中的泛化能力
介绍了一个基于不等式定理证明的学习辅助定理证明基准，旨在测试代理程序的泛化能力。该基准提供了轻量级且用户友好的定理证明环境，并评估了基于学习的基线和 Monte Carlo 树搜索。
- ACL使用比较和广义量词进行逻辑推理
本研究提出了一种基于组合范畴语法的组成性语义，并与基于自动定理证明的推理系统相结合，成功将英语中各种比较结构映射到语义表示中，本研究在包含比较、量词和数字的三个自然语言推理数据集上的实验证明该系统的表现优于之前的逻辑系统和最新的深度学习模型 - 学习生成定理以证明定理
为了解决自动定理证明中有限的人工编写定理和证明的问题，我们提出了一种学习神经生成器自动生成定理和证明来训练定理证明器的方法，并通过实验验证，证明该方法的合理性，并成功推动了 Metamath 自动定理证明的发展。
- 使用子图汇集技术提升图神经网络对逻辑公式的表达
本研究通过开发一种新型的嵌入逻辑公式的结构感知神经网络架构，成功地解决了图形化方法在逻辑公式表示时的局限性，并在两个标准数据集上进行了实证研究，取得了最先进的性能，为深度学习与自动定理证明的融合提供了新的思路。
- 在大型理论中学习推理，无需模仿
本文介绍如何在大型知识库的前提下进行自动定理证明，并通过深度强化学习技术中的基于词频 - 逆文档频率的查找开发出了一个混合陈述选择方法，以帮助探索并了解哪些前提适用于新的定理证明。实验表明，使用该方法进行训练的定理证明器优于仅以人类证明为基 - ICML通过与证明助手交互学习证明定理
本文提出了使用机器学习自动化证明助手交互的问题。研究人员通过构建 CoqGym 数据集和 ASTactic 模型，能够生成高效的策略程序并用于自动证明定理。
- TacticToe: 学习使用策略证明
本文介绍了使用机器学习和 Monte Carlo 树搜索等技术，在 HOL4 交互式定理证明器之上开发自动证明工具 TacticToe 并对其进行了实验评估，结果表明 TacticToe 能够证明 7164 个定理中的 66.4%。
- Holophrasm：用于高阶逻辑的神经自动定理证明器
使用深度学习自动证明定理的系统 Holophrasm，利用 Metamath 语言的形式化逻辑和神经网络增强的贪心算法，以及序列到序列模型进行行动枚举，可以证明 Metamath's set.mm 模块中 14% 的测试定理。
- DeepMath - 前提选择的深度序列模型
本研究使用神经序列模型探讨在自动定理证明的命题选择方面的有效性，提出了一个两级方法，能够在避免现有最先进模型的手工设计功能的同时在 Mizar 语料库上为 premise selection 任务提供良好结果。据我们所知，这是首次在大规模的 - 利用数百万引理的学习辅助定理证明
该研究实现并运用了一些适当的标准去分析 HOL Light 和 Flyspeck 等正式数学库中的引理图，从而提高了自动化定理证明的效率和准确性。
- 使用学习辅助的自动化 Flyspeck 推理
该论文结合 Flyspeck 项目中的数学知识与机器学习方法，提出一种能够自动回答数学问题的人工智能系统，并在评估中表现出较高的效率。该系统的实现涉及到 HOL Light 逻辑的转换以及机器学习的选择和集成。