premise selection | BriefGPT

关键词premise selection

搜索结果 - 8

LeanDojo：具备检索增强语言模型的定理证明
本文介绍了 LeanDojo：一个开源、可交互的证明环境，它从 Lean 中提取了证明中的数据及注释，提供了有价值的前提数据，以便于选取前提。我们使用此数据，开发了 ReProver：第一个增加检索功能的基于 LLM 的证明程序。其成本低
PDFa year ago
利用紧凑的负例生成进行主动蕴含编码，构建解释树
本文旨在将 “依托树” 作为主要方法，探讨如何有效地在大量前提事实列表中有效地构建多级推理树，该方法以主动式前提选择步骤为序列，采用预训练的变形金刚模型迭代的微调来平衡语义关系的编码和解释逻辑建立模型，并在实验中得到了 20% 的有效性提升
PDF2 years ago
Thor: 锤炼联合语言模型和自动定理证明器
该论文介绍了 Thor，一个集成语言模型和自动定理证明器的框架，它采用一种称为 “hammers” 的方法来选择前提，从而增加了语言模型在 PISA 数据集上的成功率并解决了相当一部分问题，同时比现有最佳方法在 MiniF2F 数据集上具有
PDF2 years ago
在大型理论中学习推理，无需模仿
本文介绍如何在大型知识库的前提下进行自动定理证明，并通过深度强化学习技术中的基于词频 - 逆文档频率的查找开发出了一个混合陈述选择方法，以帮助探索并了解哪些前提适用于新的定理证明。实验表明，使用该方法进行训练的定理证明器优于仅以人类证明为基
PDF5 years ago
通过深度图嵌入进行定理证明的前提选择
该研究使用基于深度学习的方法，提出了一个新的思路来选择与证明相应的数学陈述。应用了一种新的嵌入方法，将高阶逻辑公式表示为一个不变于变量重命名的图，并在保留语法和语义信息的同时，全面地将图形嵌入到一个向量中，从而在 HolStep 数据集上实
PDF7 years ago
DeepMath - 前提选择的深度序列模型
本研究使用神经序列模型探讨在自动定理证明的命题选择方面的有效性，提出了一个两级方法，能够在避免现有最先进模型的手工设计功能的同时在 Mizar 语料库上为 premise selection 任务提供良好结果。据我们所知，这是首次在大规模的
PDF8 years ago
HOL4 的前提选择和外部证明器
本文提出 HOL4 证明助手的机器学习辅助自动推理和前提选择方法，从定理陈述中提取特征选取前提，通过 HOLyHammer 将其转换为不同格式，再经由 ATPs 处理。实验显示该系统在 HOL4 标准库上具有较高的性能。
PDF9 years ago
利用语料库分析和核方法进行数学前提选择
本论文提出了基于机器学习的前提选择方法，通过构建依赖关系知识库并提出核方法的前提选择算法，在大型数学理论证明中实现了 50％的性能提升。
PDF13 years ago