Nov, 2024

自动化策略发明用于术语重写系统的结合性

HTML
PDF
TL;DR本文研究了术语重写系统的结合性，这是软件验证和编译优化中的一个重要性质。通过应用机器学习，我们开发了首个学习引导的自动结合性证明工具，并生成了一个大型随机数据集以分析术语重写系统的结合性。实验结果表明，该工具在新开发的策略下，不仅超越了现有的自动结合性证明工具CSI，还成功证明了一些之前没有自动证明的术语重写系统的结合性。
发现论文，激发创造
  • GamePad: 定理证明学习环境

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

    Jun, 2018

  • 基于集合自动机匹配的术语重写

    本文研究如何利用集合自动机来实现高效的术语重写过程，提出一种优化算法，用于外层重写线性左规则术语重写系统，证明其正确性，并展示了一些实现实验结果。

    Feb, 2022

  • 通过学习细化搜索策略来学习查找证明和定理 - 循环不变式合成的案例

    我们提出了一种新的自动定理证明方法，其中使用AlphaZero风格智能体自我训练来改进表达为非确定性程序的通用高级专家策略，同时具有类似的教师代理机自我训练来生成适当相关性和难度的任务以供学习者解决，利用最小领域知识来解决合成训练数据不可用或难以合成的问题，具体举例来说，我们考虑了用于命令程序的循环不变量合成，并使用神经网络来改进教师和求解策略。

    May, 2022

  • LeanDojo：具备检索增强语言模型的定理证明

    本文介绍了 LeanDojo：一个开源、可交互的证明环境，它从Lean中提取了证明中的数据及注释，提供了有价值的前提数据，以便于选取前提。 我们使用此数据，开发了 ReProver：第一个增加检索功能的基于LLM的证明程序。其成本低廉，只需要一台GPU进行一周的训练，并且可以有效地选择定理中的前提。我们构建了一个包含96962个定理和证明的新基准，并将其用于培训和评估。实验结果表明，相对于非检索基线和GPT-4，ReProver非常有效。我们发布了代码和数据集，以促进进一步的研究。

    Jun, 2023

  • 正则表达式推理挑战

    提出正则表达式推理（REI）作为代码/语言模拟的挑战，并对更广泛的机器学习社区提出。REI是一项监督式机器学习和程序综合任务，通过示例来找到最小的正则表达式。最近在GPU上实现了REI求解器，首次实现了用于复杂REI实例的快速最小表达式生成。以此为基础，我们生成并发布了REI的第一个大规模数据集，并设计和评估了几种初始启发式和机器学习基准方法。邀请社区参与并探索学习解决REI问题的机器学习方法。我们相信，在REI方面的进展直接转化为代码/语言模型。

    Aug, 2023

  • 通过数据增强和动态采样方法提升神经定理证明

    DS-Prover是一个用于定理证明的创新动态抽样方法，通过根据剩余时间和总分配时间来调整探索和开发之间的平衡，以提高证明搜索过程的效率，并通过拆分简化和重写策略为具有单个前提的策略来扩充训练数据集，从而在MiniF2F和ProofNet两个标准数据集上实现了显著的性能提升。

    Dec, 2023

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

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

    Apr, 2024

  • 迈向在Lean中进行定理证明的大型语言模型作为副驾驶

    该研究论文介绍了使用大型语言模型作为辅助工具的 Lean Copilot 框架，用于证明定理过程中的自动化，证明步骤建议、自动完成中间证明目标、选择相关前提条件等。实验证明了该方法较现有的基于规则的证明自动化方法在证明定理过程中对人类的辅助和自动化程度的有效性。

    Apr, 2024

  • miniCodeProps：证明代码属性的最小基准

    利用神经网络的数学定理证明、代码验证和自动化定理证明等领域的研究，提出了一个测试用例，旨在进一步发展形式验证代码的自动定理证明。

    Jun, 2024

  • ImProver：基于智能体的自动化证明优化

    本文针对现有形式证明在可读性、简洁性等方面的优化问题提出了新的解决方案。通过引入ImProver这一基于大型语言模型的智能体，本文实现了对形式证明的自动化优化，使得优化后的证明在长度、模块化程度及可读性等指标上显著提升。研究结果表明，该方法在多种数学定理的优化中表现出色，具有广泛的应用潜力。

    Oct, 2024