Aug, 2024

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

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

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

    Jan, 2017

  • 强化学习定理证明

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

    May, 2018

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

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

    May, 2019

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

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

    May, 2019

  • 利用语言模型进行定理证明的证明工件协同训练

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

    Feb, 2021

  • LEGO证明器：具有增长库的神经定理证明

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

    Oct, 2023

  • 借鉴失败：使用试错数据对直觉命题逻辑证明进行微调的LLM

    通过从失败的搜索路径中学习，我们展示了训练模型的益处。我们与仅使用正确路径训练的模型进行比较，并发现前者以更少的搜索次数解决了更多未见过的定理。

    Apr, 2024

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

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

    Apr, 2024

  • DeepSeek-Prover: 通过大规模合成数据推进LLMs中的定理证明

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

    May, 2024

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

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

    Aug, 2024