通过与证明助手交互学习证明定理
自动定理证明器和形式证明助手是理论上能够证明任意难题的一般推理系统，但在实践中面临组合爆炸所以包括很多启发式算法和选择点来影响系统性能。机器学习预测器可以引导这些推理系统的工作。本文概述了几个自动推理和定理证明领域及目前对它们进行的学习和人工智能方法，包括前提选择、证明引导、协同推理和学习的 AI 系统以及符号分类问题。
Mar, 2024
为了解决自动定理证明中有限的人工编写定理和证明的问题，我们提出了一种学习神经生成器自动生成定理和证明来训练定理证明器的方法，并通过实验验证，证明该方法的合理性，并成功推动了 Metamath 自动定理证明的发展。
Feb, 2020
通过 GamePad 系统，探索机器学习方法在 Coq 证明助手中的应用，通过基线模型训练解决 “定位评估” 和 “策略预测” 任务，从而探索定理证明与人类监督交替的可能性。
Jun, 2018
使用新的基于图的数据集进行 Coq 的机器学习，我们提出了 Graph2Tac（G2T）模型，通过考虑以往定义层次与当前目标之间的依赖关系，将新的数学概念整合到模型的知识库中。
Jan, 2024
该论文表明，通过使用现有的证明助理，可以以与建立证明助理自身的信任和可审计性原则相一致的方式，构建对自然语言表达的规范的支持。我们在 Lean 证明助理内实现了一种方式，以可扩展的正式英语子集提供规范，并自动将其翻译成正式的命题。我们的方法是可扩展的（对语法结构没有永久限制），模块化的（允许在库中分发有关新词的信息），并且生成解释了每个词的解释方式以及如何使用句子结构来计算含义的证明证书。我们将原型应用于从一本流行教材中翻译各种正式规范的英文描述；在仅需进行小幅修改的情况下，借助一个适度的词汇表，所有规范都能被正确翻译。
Oct, 2023
该研究论文介绍了一个专门设计用于提高大型语言模型在解释和生成 Coq 代码方面能力的全面数据集，通过亦包含源引用和许可信息的数千个 Coq 源代码文件，初步实验表明使用该数据集训练的模型在 Coq 代码生成方面具有显著的潜力。
Mar, 2024
本文介绍如何在大型知识库的前提下进行自动定理证明，并通过深度强化学习技术中的基于词频 - 逆文档频率的查找开发出了一个混合陈述选择方法，以帮助探索并了解哪些前提适用于新的定理证明。实验表明，使用该方法进行训练的定理证明器优于仅以人类证明为基础的证明器，并可以接近于用模仿和强化学习相结合进行训练的证明器的性能。我们还通过多次实验来理解我们的探索方法背后的假设重要性，并解释了我们的设计选择。
May, 2019