提出了一种新型的神经定理证明器，通过仅考虑最高证明分数相关的证明路径，可以在以前无法应用的知识库上进行推理和学习。

Jul, 2018

本文提出了一种名为Conditional Theorem Provers（CTPs）的方法，它是Neural Theorem Provers（NTPs）的扩展，可以通过基于梯度的优化学习出最优规则选择策略以实现可解释性和可扩展性，并且在大规模任务中表现优异。CTPs在CLUTRR数据集上取得了表现最优结果，并在标准基准测试中展现了比其他神经符号模型更好的链接预测结果。

Jul, 2020

本文介绍了 PACT 的一般方法，通过自我监督学习从内核级证明术语中提取丰富的数据，以协同常规战术预测目标，以提高定理证明的成功率。

Feb, 2021

miniF2F是一个Olympiad级别的数学问题数据集，用于在神经定理证明中提供统一的跨系统基准。使用GPT-f作为神经定理证明的基线调用miniF2F，并提供了性能分析。

Aug, 2021

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

Jun, 2023

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

Oct, 2023

通过使用神经符号计算来全面利用LLMs和符号化证明器，本文探索了以逻辑推理任务，特别是符合自然语言的任务为基础的解决方案。

Oct, 2023

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

Dec, 2023

利用神经网络的数学定理证明、代码验证和自动化定理证明等领域的研究，提出了一个测试用例，旨在进一步发展形式验证代码的自动定理证明。

Jun, 2024

传统基于语言模型的定理证明假设在足够数量的形式证明数据上训练后，模型将学会证明定理。研究观察到非形式证明中蕴含的丰富信息对于学习证明定理是有用的。因此，使用回顾性的真实策略生成合成思考来训练语言模型，Lean-STaR框架通过在每个证明步骤的预测策略之前直接生成思考来提升模型的证明定理能力，并通过专家迭代进一步微调模型。在Lean定理证明环境中，Lean-STaR在miniF2F-test基准上取得了最先进的结果，显著优于基准模型（$43.4% ightarrow 46.3%，$ Pass@64），同时对增强思考对定理证明过程的各个方面的影响进行了分析，提供了洞察力。

Jul, 2024