Sep, 2022

基于模块化强化学习的自动定理证明器项目建议

HTML
PDF
TL;DR建议建立一个强化学习证明独立组件：演绎系统（环境），证明状态表示（代理如何看待环境）和代理训练算法。为此，我们为OpenAI Gym环境的饱和证明器提供了一个基于Vampire的环境，并展示了使用gym-saturation和流行的强化学习框架（Ray RLlib）的原型。最后，我们讨论了将此正在进行的工作完成到一个竞争性自动定理证明器的计划。
发现论文，激发创造
  • 强化学习定理证明

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

    May, 2018

  • HOList: 面向高阶定理证明机器学习的环境

    我们提供了一个基于HOL Light定理证明器的开源框架，可以用作强化学习环境；并提出了一个基于深度强化学习的自动定理证明器DeepHOL，它在基准测试中取得了强大的初步结果。

    Apr, 2019

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

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

    May, 2019

  • Gym-saturation: 一个用于饱和证明器的OpenAI Gym环境

    `gym-saturation` 是一个基于 OpenAI Gym 的强化学习环境，用于证明定理，支持 TPTP 库中 CNF 形式的定理。它实现了“给定子句”算法，可以通过不同的代理来训练自己并作为一种自动定理证明器。

    Mar, 2022

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

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

    Apr, 2022

  • 基于高效不变名称的图神经网络表示的自动定理证明集成方法

    使用强化学习和集成方法，借助改进的图神经网络和改良的公式表示方法，成功地构建了一种名称不变的公式表示方法，显着提高了自动定理证明的性能和泛化能力。

    May, 2023

  • gym-饱和：用于饱和证明器的体育馆环境（系统描述）

    这项工作描述了之前发布的Python软件包gym-saturation的新版本：这是一个基于给定子句算法和强化学习的OpenAI Gym环境集合。我们提供了两种不同求解器（Vampire和iProver）的使用示例，并将证明状态表示与强化学习分离，并提供了使用已知的ast2vec Python代码嵌入模型作为一阶逻辑表示的示例。此外，我们还展示了环境包装器如何将求解器转化为类似多臂赌博机问题的问题。我们使用Ray RLlib实现了两种强化学习算法（Thompson抽样和Proximal Policy Optimization），以展示我们软件包新版本的实验易用性。

    Sep, 2023

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

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

    Mar, 2024

  • DeepSeek-Prover-V1.5：利用证明助手反馈提升强化学习和蒙特卡洛树搜索

    本研究提出了DeepSeek-Prover-V1.5，一个用于Lean 4的开源语言模型，针对定理证明进行了优化，解决了训练和推理过程中的效率问题。创新性地采用了来自证明助手反馈的强化学习方法，并引入RMaxTS变体，以多样化的证明路径生成为目标。结果显示该模型在中学和本科水平的基准测试中取得了显著的成绩提升，展示了其在推理任务中的潜在影响。

    Aug, 2024

  • QEDCartographer：使用无奖励强化学习自动化形式验证

    本研究解决了手动编写形式验证证明的困难，从而限制了其在实际应用中的实用性。提出的QEDCartographer工具结合监督学习与强化学习，有效地探索证明空间，克服了形式验证中稀疏奖励的问题。实验证明，该工具自动证明的定理比例达21.4%，显著优于传统基于监督学习的工具，展示了强化学习在提升证明合成工具搜索机制方面的潜力。

    Aug, 2024