本文介绍了一个以定理驱动的问答数据集 TheoremQA，用于评估人工智能模型应用定理解决具有挑战性的科学问题的能力。研究人员使用 16 个大型语言和代码模型评估 TheoremQA，并发现 GPT-4 在 Program-of-Thoughts Prompting 的帮助下解决这些问题的能力是无与伦比的，达到了 51％，而现有的所有开放源代码模型都低于 15％，仅仅超过了随机猜测的基线。

May, 2023

本文介绍了如何使用机器学习从 Coq 系统中的证明自动学习证明依赖，并给出了该方法在 Coq 证明上的测试结果及对比，证明了其可行性。

Oct, 2014

基于大规模合成数据，使用 Lean 4 proof 数据生成方法，我们的模型在定理生成和解决题目方面取得了卓越的成果，证明了合成数据对提高 LLMs 中的定理证明能力的潜力。

May, 2024

本文介绍了一种基于 Higher-Order Logic 证明的新数据集，旨在开发基于机器学习的定理证明策略并提出基于该数据集的各种机器学习任务，通过一些基于逻辑回归、卷积神经网络和循环神经网络的基准模型显示出将机器学习应用于 HOL 定理证明的前景。

Mar, 2017

本文提出了使用机器学习自动化证明助手交互的问题。研究人员通过构建 CoqGym 数据集和 ASTactic 模型，能够生成高效的策略程序并用于自动证明定理。

May, 2019

DS-Prover 是一个用于定理证明的创新动态抽样方法，通过根据剩余时间和总分配时间来调整探索和开发之间的平衡，以提高证明搜索过程的效率，并通过拆分简化和重写策略为具有单个前提的策略来扩充训练数据集，从而在 MiniF2F 和 ProofNet 两个标准数据集上实现了显著的性能提升。

Dec, 2023

FormAI 数据集利用动态零 - shot 提示技术构建，包含 11.2 万个 AI 生成的可以编译和独立运行的 C 程序，按漏洞类型进行了分类，并采用 SMT-based Bounded Model Checker 方法进行了验证，检测出漏洞并提供反例，用于评估各种静态和动态分析工具的效果以及用于训练大型语言模型和机器学习算法。

Jul, 2023

通过提出一种新的流程，我们利用合成数据来将自然语言数学问题转化为 Lean 4 语句，并相应地进行过滤，从而为解决 LLMs 在理解复杂数学问题和证明上的性能提供有用的训练数据。最终数据集包含约 57K 个正式 - 非正式问题对以及来自数学竞赛论坛的搜索证明和 21 个新的 IMO 问题。

Jun, 2024

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

Jun, 2023

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

Apr, 2024