Aug, 2024

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

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

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

    May, 2018

  • GamePad: 定理证明学习环境

    通过GamePad系统，探索机器学习方法在Coq证明助手中的应用，通过基线模型训练解决“定位评估”和“策略预测”任务，从而探索定理证明与人类监督交替的可能性。

    Jun, 2018

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

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

    May, 2019

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

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

    May, 2019

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

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

    Feb, 2021

  • Draft, Sketch, and Prove: 用非正式证明指导形式化定理证明器

    本文介绍了一种名为DSP的方法，可以将非正式证明映射到正式证明草图并指导自动证明器，使其搜索更容易的子问题。实验证明语言模型能够产生结构良好的正式草图，并将其指导自动证明器，从而提高性能达到39.3%。

    Oct, 2022

  • 分解恩格玛：基于子目标的演示学习用于形式定理证明

    本文介绍了一个基于小目标的证明学习框架和扩散模型，成功地将证明的正确率从38.9％提高到45.5％，或者比长期的最先进方法提高了5倍的采样效率。

    May, 2023

  • 增强形式定理证明：一个用于训练Coq代码AI模型的综合数据集

    该研究论文介绍了一个专门设计用于提高大型语言模型在解释和生成Coq代码方面能力的全面数据集，通过亦包含源引用和许可信息的数千个Coq源代码文件，初步实验表明使用该数据集训练的模型在Coq代码生成方面具有显著的潜力。

    Mar, 2024

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

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

    Apr, 2024

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

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

    Aug, 2024