Jan, 2024

Graph2Tac: 数学定理证明中的数学概念的分层表示学习

PDF
TL;DR使用新的基于图的数据集进行 Coq 的机器学习，我们提出了 Graph2Tac（G2T）模型，通过考虑以往定义层次与当前目标之间的依赖关系，将新的数学概念整合到模型的知识库中。
mathematicsapplicationsai agentcoq proof assistantgraph-based dataset
发现论文，激发创造
  • 高阶逻辑和定理证明的图表示

    本文首次使用图神经网络 (GNNs) 实现高阶证明搜索，并证明 GNNs 能够提高此领域的最新成果。我们考虑了高阶逻辑的几种图形表示，并将它们与 HOList 基准进行了评估。

    May, 2019

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

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

    May, 2019

  • 战略家的大规模形式知识网络

    在这篇论文中，我们介绍了 Tactician's Web 平台，它提供了一个大型的、相互连接的、经过机器验证的数学知识网络，方便地用于机器学习、分析和证明工程。该平台构建在 Coq 证明助手之上，导出了一个包含广泛形式理论的数据集，以定义、定理、证明项、策略和证明状态的网络形式呈现，并提供了人类可读的文本形式。与 Coq 的紧密整合使得可以将证明代理作为实用工具提供给证明工程师。

    Jan, 2024

  • 概念的简洁表示

    通过基于范畴论的简洁概念表示，可以训练模型从而精确理解概念，并产生不变性属性以及层级分解，以验证每个部分来学习复杂概念或纠正误解。

    Mar, 2023

  • 基于自动正式化的数学和代码正确性研究：基础证明实验

    本研究介绍了一种基于 Universal Transformer 体系结构的语义解析方法，可以将基本数学证明转化为 Coq 互动定理证明器中的等效形式，以及将装饰有 Hoare 三元组的简单命令式代码翻译成 Coq 中的形式验证证明。通过人工和人工写作证明的有限领域的实验表明，这些模型对于训练期间未看到的中间长度和自然语言变化具有很好的泛化能力。

    Jan, 2023

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

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

    May, 2023

  • Coq 证明引导的机器学习：第一次实验

    本文介绍了如何使用机器学习从 Coq 系统中的证明自动学习证明依赖，并给出了该方法在 Coq 证明上的测试结果及对比，证明了其可行性。

    Oct, 2014

  • 图层次结构中的知识表示与更新

    提出了一种基于有向无环层次的数学理论来表示知识的方法，介绍了 sesqui-pushout 重写的应用以及 python 库 ReGraph 在此理论中的实现方法。

    Feb, 2020

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

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

    Feb, 2021

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

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

    Dec, 2023