Mar, 2024

学习引导的自动推理：简要调查

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

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

    May, 2018

  • 建立对自动推理的信任

    自从上世纪 40 年代起，计算机的自动推理逐渐成为科学研究中越来越重要的工具。现阶段，通过机器学习技术从大量数据中推导出的规则成为了一种互补的方法，并在积极发展中。然而，我们对于为何应该相信这些系统以及通过其帮助获得的结果的问题，在科学哲学家的讨论中却一直未引起从业者的足够关注。本研究关注独立评审，作为对科学的信任的重要来源，并确定了影响自动推理系统可评审性的特征。同时，探讨通过技术和社会措施相结合的途径来增强推理系统的评审性和可信度。

    Aug, 2023

  • 从机器学习到机器推理

    通过代数操作简单的学习系统来建立推理能力，而非试图在机器学习系统和复杂的推理机制之间建立联系。

    Feb, 2011

  • 基于规则的定理证明器：中学证明入门

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

    Mar, 2023

  • 通过与证明助手交互学习证明定理

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

    May, 2019

  • 深度网络引导的证明搜索

    利用深度学习技术来辅助自动的定理证明，通过对 Mizar 库的证明进行数据训练和选择处理，改进 ATP 的证明搜索引导，从而大幅度减少证明搜索的步骤和提高定理的证明率。

    Jan, 2017

  • 对抗性学习实现对任意逻辑的推理

    本研究提出了一种 Monte-Carlo 模拟系统，利用强化学习能够在任何逻辑领域中进行工作，而无需任何人为知识或问题集。

    Apr, 2022

  • 在大型理论中学习推理，无需模仿

    本文介绍如何在大型知识库的前提下进行自动定理证明，并通过深度强化学习技术中的基于词频 - 逆文档频率的查找开发出了一个混合陈述选择方法，以帮助探索并了解哪些前提适用于新的定理证明。实验表明，使用该方法进行训练的定理证明器优于仅以人类证明为基础的证明器，并可以接近于用模仿和强化学习相结合进行训练的证明器的性能。我们还通过多次实验来理解我们的探索方法背后的假设重要性，并解释了我们的设计选择。

    May, 2019

  • 深度学习在定理证明中的调查

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

    Apr, 2024

  • 学习生成定理以证明定理

    为了解决自动定理证明中有限的人工编写定理和证明的问题，我们提出了一种学习神经生成器自动生成定理和证明来训练定理证明器的方法，并通过实验验证，证明该方法的合理性，并成功推动了 Metamath 自动定理证明的发展。

    Feb, 2020