- Thor: 锤炼联合语言模型和自动定理证明器
该论文介绍了 Thor，一个集成语言模型和自动定理证明器的框架，它采用一种称为 “hammers” 的方法来选择前提，从而增加了语言模型在 PISA 数据集上的成功率并解决了相当一部分问题，同时比现有最佳方法在 MiniF2F 数据集上具有 - Gym-saturation: 一个用于饱和证明器的 OpenAI Gym 环境
`gym-saturation` 是一个基于 OpenAI Gym 的强化学习环境，用于证明定理，支持 TPTP 库中 CNF 形式的定理。它实现了 “给定子句” 算法，可以通过不同的代理来训练自己并作为一种自动定理证明器。
- 常识知识的选取策略
本研究介绍了基于词向量的向量选择策略，用于在具有常识知识的知识库上进行定理证明，并通过案例研究证明了其有效性。
- 利用语言模型进行定理证明的证明工件协同训练
本文介绍了 PACT 的一般方法，通过自我监督学习从内核级证明术语中提取丰富的数据，以协同常规战术预测目标，以提高定理证明的成功率。
- 逻辑神经网络
我们提出了一种新的框架，无缝提供神经网络（学习）和符号逻辑（知识和推理）的关键属性，每个神经元都有权重实值逻辑公式的组成部分，得到了高度可解释的分离表示，推理是全向的而不是集中在预定义的目标变量上，对应于逻辑推理，包括经典的一阶逻辑定理证明 - 视觉 - 文本蕴涵的多模态逻辑推理系统
该研究论文通过逻辑表征作为文本和图像的统一意义表征，并提出了一种无监督的多模态逻辑推断系统，可有效证明它们之间的推理关系，结合语义分析和定理证明，系统可以处理语义复杂的视觉 - 文本推断。
- GamePad: 定理证明学习环境
通过 GamePad 系统，探索机器学习方法在 Coq 证明助手中的应用，通过基线模型训练解决 “定位评估” 和 “策略预测” 任务，从而探索定理证明与人类监督交替的可能性。
- 强化学习定理证明
提出了一种定理证明算法，该算法使用几乎没有领域启发式来指导其连接风格的证明搜索，而是运行许多蒙特卡罗模拟，通过强化学习来指导以前的证明尝试。
- HolStep：高阶逻辑定理证明的机器学习数据集
本文介绍了一种基于 Higher-Order Logic 证明的新数据集，旨在开发基于机器学习的定理证明策略并提出基于该数据集的各种机器学习任务，通过一些基于逻辑回归、卷积神经网络和循环神经网络的基准模型显示出将机器学习应用于 HOL 定理 - 深度网络引导的证明搜索
利用深度学习技术来辅助自动的定理证明，通过对 Mizar 库的证明进行数据训练和选择处理，改进 ATP 的证明搜索引导，从而大幅度减少证明搜索的步骤和提高定理的证明率。
- ACLACL2 版本 6.2、6.3 和 6.4 的增强功能
本文介绍了自 2013 年 ACL2 研讨会以来对 ACL2 的改进，并涉及形式验证和定理证明方面的研究领域。