介绍了在中学引入自动推理系统面临的几个瓶颈，讨论了一个基于推理规则和自动方法的实现并使用其进行几何猜想的证明，旨在介绍几何定理的形式证明，以激发学生的兴趣。

Mar, 2023

自动定理证明器和形式证明助手是理论上能够证明任意难题的一般推理系统，但在实践中面临组合爆炸所以包括很多启发式算法和选择点来影响系统性能。机器学习预测器可以引导这些推理系统的工作。本文概述了几个自动推理和定理证明领域及目前对它们进行的学习和人工智能方法，包括前提选择、证明引导、协同推理和学习的 AI 系统以及符号分类问题。

Mar, 2024

该论文对经典规划的重组技术的大量研究进行了系统综述，旨在提供该领域的整体视图，并促进未来的研究。作为一个有形的结果，我们提供了现有技术分类的定性比较，这可以帮助研究人员获得它们的优点和缺点的概述。

Jan, 2023

本研究介绍了一种基于 Universal Transformer 体系结构的语义解析方法，可以将基本数学证明转化为 Coq 互动定理证明器中的等效形式，以及将装饰有 Hoare 三元组的简单命令式代码翻译成 Coq 中的形式验证证明。通过人工和人工写作证明的有限领域的实验表明，这些模型对于训练期间未看到的中间长度和自然语言变化具有很好的泛化能力。

Jan, 2023

本研究介绍了一种利用启发式算法解决定理证明和计划制定问题的方法，并将其应用于 situation calculus 中。该方法通过使用 A * 搜索算法排列一系列情境，并利用删除松弛法控制启发式规划器，获得较短的计划方案，并探索较少的状态。实验表明，该方法可以应用于较大规模的问题。

Mar, 2023

提出了一种定理证明算法，该算法使用几乎没有领域启发式来指导其连接风格的证明搜索，而是运行许多蒙特卡罗模拟，通过强化学习来指导以前的证明尝试。

May, 2018

自动形式化研究级数学的一个方法是将任务分解为更容易和可接近的子任务：未链接的形式化、实体链接和类型调整。同时，本文还提出了一个用于未链接的形式化的基准数据集 arXiv2Formal，其中包含了从 arXiv.org 的论文中选取的 50 个定理的 Lean 定理证明器的形式化。欢迎社区为该数据集的未来版本做出贡献。

Oct, 2023

本研究探讨在数学中的程序抽象结构，定案例研究并且说明通过 Peano 定理证明环境和可重用抽象的能力，加上恰当的教学大纲，是保障自动化数学推理的长期文化传播的有效方法。

Nov, 2022

本文基于 Cui 等人的研究，探索了用于广义规划的 sound abstraction 的自动验证，并提出了基于模型理论的 sound 和 complete abstraction 的定义。本文还提出了可验证 sound abstraction 的充分条件，并开发了处理计数和传递闭包的方法来实现其验证。最后，本文实现了一个 sound abstraction 验证系统，并在几个领域进行了实验。

May, 2022

该论文提出了一种将概率论和第一阶逻辑相结合的方法，在有限域内具有 Herbrand 解释的情况下，定义了概率证明定理及其推广问题，然后提出了能够同时拥有图模型推理和一阶定理证明的完整能力的方法，并开发了一种高效算法。实验表明，当逻辑结构存在时，该算法远优于目前已有的方法。

Feb, 2012