使用学习辅助的自动化 Flyspeck 推理
本文提出 HOL4 证明助手的机器学习辅助自动推理和前提选择方法，从定理陈述中提取特征选取前提，通过 HOLyHammer 将其转换为不同格式，再经由 ATPs 处理。实验显示该系统在 HOL4 标准库上具有较高的性能。
Sep, 2015
HOL (y) Hammer 是一个基于 HOL Light 编码的在线人工智能 / 自动定理证明 (ATP) 服务，提供自动处理基于 HOL Light 的任意正式开发项目和攻击上传项目的任意猜想的功能。
Sep, 2013
提出了一个基于给定句子算法的自动定理证明器的新的内部指导方法，该方法使用先前证明中的正负例影响未处理子句的选择。为此，提出了一种基于幺半群结构的类型广义标签出现次数的朴素贝叶斯分类的有效方案。将这种方法在高阶逻辑证明器 Satallax 中完成，证明了该方案比不具有内部指导的 Satallax 可以解决更多问题，能够扩展现有的快速分类器。在 Flyspeck 项目的一个简单类型的高阶逻辑版本上评估了我们的方法，在没有内部指导的 Satallax 不能解决的 26% 的问题上可以解决。
May, 2016
使用 AI 自动化构建证明导向的程序，我们提供了一个包含 600K 行开源 F * 程序和证明的数据集，通过 AI 进行程序和证明的综合，使用细调小型语言模型和类型检索增强技术取得有希望的结果，为未来改进提供了方向。
May, 2024
自动定理证明器和形式证明助手是理论上能够证明任意难题的一般推理系统，但在实践中面临组合爆炸所以包括很多启发式算法和选择点来影响系统性能。机器学习预测器可以引导这些推理系统的工作。本文概述了几个自动推理和定理证明领域及目前对它们进行的学习和人工智能方法，包括前提选择、证明引导、协同推理和学习的 AI 系统以及符号分类问题。
Mar, 2024
使用深度学习自动证明定理的系统 Holophrasm，利用 Metamath 语言的形式化逻辑和神经网络增强的贪心算法，以及序列到序列模型进行行动枚举，可以证明 Metamath's set.mm 模块中 14% 的测试定理。
Aug, 2016
利用深度学习技术来辅助自动的定理证明，通过对 Mizar 库的证明进行数据训练和选择处理，改进 ATP 的证明搜索引导，从而大幅度减少证明搜索的步骤和提高定理的证明率。
Jan, 2017
本文提出了使用机器学习自动化证明助手交互的问题。研究人员通过构建 CoqGym 数据集和 ASTactic 模型，能够生成高效的策略程序并用于自动证明定理。
May, 2019