本文介绍了一个基于神经变换器的自动定理证明方法 Magnushammer，使用 PISA 基准测试，证明率达到 59.5％，超过了目前最成熟和最流行的基于符号的求解器 Sledgehammer 的 38.3％，并通过与基于语言模型的神经形式证明器相结合，将先前的最先进证明率从 57.0％提高到 71.0％。

Mar, 2023

本文提出 HOL4 证明助手的机器学习辅助自动推理和前提选择方法，从定理陈述中提取特征选取前提，通过 HOLyHammer 将其转换为不同格式，再经由 ATPs 处理。实验显示该系统在 HOL4 标准库上具有较高的性能。

Sep, 2015

本文介绍了 LeanDojo：一个开源、可交互的证明环境，它从 Lean 中提取了证明中的数据及注释，提供了有价值的前提数据，以便于选取前提。 我们使用此数据，开发了 ReProver：第一个增加检索功能的基于 LLM 的证明程序。其成本低廉，只需要一台 GPU 进行一周的训练，并且可以有效地选择定理中的前提。我们构建了一个包含 96962 个定理和证明的新基准，并将其用于培训和评估。实验结果表明，相对于非检索基线和 GPT-4，ReProver 非常有效。我们发布了代码和数据集，以促进进一步的研究。

Jun, 2023

本文介绍了一种用于 HOL4 TacticToe 的策略级自动化方法，将机器学习和翻译技术与自动定理证明辅助工具相结合，以探索不同的策略级证明路径，并且通过组合策略预测和前提选择，在 5 秒内重新证明了 7902 个 HOL4 定理中的 39％，效果显著。

Apr, 2018

本文探讨了基于 Transformer 的语言模型在自动定理证明中的应用，提出了基于语言模型的生成能够解决自动定理证明器与人类相比的主要限制之一 —— 原始数学术语的生成问题。我们提出了一个自动证明器和证明辅助工具 GPT-f，使用 Metamath 形式语言，并分析了其性能。 GPT-f 发现了新的简短证明，并被采纳为正式数学社区所接受，这是我们所知道的第一次基于深度学习的系统为正式数学社区做出的贡献。

Sep, 2020

通过人工提供或查找背景参考条件，NaturalProver 能够生成数学证明，融合符号和自然语言，提高了下一步建议和生成证明的质量，在某些需要短证明的定理上具有证明能力，并且提供的下一步建议有超过 40% 的正确和有用率。

May, 2022

LEGO-Prover 使用技能库，通过模块化构建证明以及生成新技能，提高了大型语言模型在定理证明中的能力，并进一步推进了数学领域的研究。

Oct, 2023

该论文提供了一项深度学习在定理证明中的全面调研，包括现有方法的综述、数据集和策略的详细总结、评估指标和最先进技术的性能分析，以及未来研究的挑战和发展方向的批判性讨论。该调研旨在成为深度学习在定理证明中的基础参考，促进这个迅速发展领域的进一步研究。

Apr, 2024

该研究论文介绍了使用大型语言模型作为辅助工具的 Lean Copilot 框架，用于证明定理过程中的自动化，证明步骤建议、自动完成中间证明目标、选择相关前提条件等。实验证明了该方法较现有的基于规则的证明自动化方法在证明定理过程中对人类的辅助和自动化程度的有效性。

Apr, 2024

LangPro 是一种自然语言自动证明器，使用基于专门设计的自然逻辑的分析表格方法，能够推导出前提和假设之间的语义关系，并在 FraCaS 和 SICK 文本蕴含数据集上达到了可与最先进技术相媲美的高结果。

Aug, 2017