theorem proving | BriefGPT - AI 论文速递

关键词theorem proving

搜索结果 - 30

从内在动机学习形式数学
通过构造一个 agent，它能够自我产生推测和证明，我们探索了从自有公理中探索数学的方法。使用约束解码和类型导向综合的方法，我们在依赖类型理论中对数学领域进行公理化，从中采样有效的推测，同时使用相同的模型生成策略和价值函数来引导证明搜索，从
PDF4 days ago
DeepSeek-Prover: 通过大规模合成数据推进 LLMs 中的定理证明
基于大规模合成数据，使用 Lean 4 proof 数据生成方法，我们的模型在定理生成和解决题目方面取得了卓越的成果，证明了合成数据对提高 LLMs 中的定理证明能力的潜力。
PDFa month ago
迈向在 Lean 中进行定理证明的大型语言模型作为副驾驶
该研究论文介绍了使用大型语言模型作为辅助工具的 Lean Copilot 框架，用于证明定理过程中的自动化，证明步骤建议、自动完成中间证明目标、选择相关前提条件等。实验证明了该方法较现有的基于规则的证明自动化方法在证明定理过程中对人类的辅助
PDF3 months ago
深度学习在定理证明中的调查
该论文提供了一项深度学习在定理证明中的全面调研，包括现有方法的综述、数据集和策略的详细总结、评估指标和最先进技术的性能分析，以及未来研究的挑战和发展方向的批判性讨论。该调研旨在成为深度学习在定理证明中的基础参考，促进这个迅速发展领域的进一步
PDF3 months ago
ACLLeanReasoner: 用 Lean 增强复杂逻辑推理
利用 Lean 框架，将复杂的逻辑推理问题形式化为定理后进行求解，以减少逻辑不一致性的风险并提升处理复杂推理任务的能力，取得了在 FOLIO 数据集上的最先进表现，并在 ProofWriter 上接近该水平的成果。值得注意的是，这些结果是在
PDF3 months ago
增强形式定理证明：一个用于训练 Coq 代码 AI 模型的综合数据集
该研究论文介绍了一个专门设计用于提高大型语言模型在解释和生成 Coq 代码方面能力的全面数据集，通过亦包含源引用和许可信息的数千个 Coq 源代码文件，初步实验表明使用该数据集训练的模型在 Coq 代码生成方面具有显著的潜力。
PDF4 months ago
BAIT：交互证明（嵌入）架构的基准测试
人工智能在定理证明方面，尤其是在交互定理证明中，已经产生了许多基准和方法。本文介绍了 BAIT，一个公正而简化的比较学习方法在交互定理证明中的框架，通过对多个基准的深入比较，展示了 BAIT 的能力。我们发现结构感知变换器表现特别好，改进了
PDF4 months ago
ICLR重构：从证明中学习提取定理
通过使用 REFACTOR 方法，我们能够训练神经网络以模仿人类数学家在形式化数学定理证明中识别出的模块化和可重用的定理，从而提取出不同领域的新定理，这些新定理在证明过程中使用频率较高，并有助于缩短证明的长度，并最终使得在新定理重构的数据集
PDF4 months ago
统一合成定理与证明数据的 MUSTARD 方法
该研究论文提出了 MUSTARD，一个数据生成框架，通过三个步骤合成高质量和多样化的定理和证明数据，用于理解大型语言模型在数学推理和定理证明方面的能力。利用 MUSTARD 生成的数据进行 Fine-tuning，可以在自动定理证明和数学问
PDF5 months ago
EvoGPT-f: 用于基准测试形式数学语言的进化 GPT 框架
这篇论文通过 EvoGPT-f 回答了关于五种形式数学语言（Lean 3、Lean 4、Coq、HOL 4、HOL Light）和四种标记化方法（字符、词级、字节对编码和 StarCoder 标记器）之间的差异化机器学习能力的定量分析，为进
PDF5 months ago
基于约束求解的合成几何陈述和证明的自动补全方法
通过使用合一逻辑和约束求解，我们提出了一个框架，用于补充不完整的猜想和证明。该框架可以将具有缺失假设和不明确目标的猜想转化为正确的定理，并帮助完成草图式证明以使其适于人类阅读和机器检查。
PDF5 months ago
通过数据增强和动态采样方法提升神经定理证明
DS-Prover 是一个用于定理证明的创新动态抽样方法，通过根据剩余时间和总分配时间来调整探索和开发之间的平衡，以提高证明搜索过程的效率，并通过拆分简化和重写策略为具有单个前提的策略来扩充训练数据集，从而在 MiniF2F 和 Proof
PDF6 months ago
大型语言模型对数学的理解：源批评和推演
GPT-4 的研究调查发现，尽管该模型可以重复、改编和润色其之前见过的数学证明，然而它并未实际理解基本数学概念，而在形式语言中证明数学定理的任务与搜索引擎如 Google 的方法相当，而预测句子中的下一个词可能是一种错误的方法，往往会导致过
PDF8 months ago
LEGO 证明器：具有增长库的神经定理证明
LEGO-Prover 使用技能库，通过模块化构建证明以及生成新技能，提高了大型语言模型在定理证明中的能力，并进一步推进了数学领域的研究。
PDF9 months ago
LeanDojo：具备检索增强语言模型的定理证明
本文介绍了 LeanDojo：一个开源、可交互的证明环境，它从 Lean 中提取了证明中的数据及注释，提供了有价值的前提数据，以便于选取前提。我们使用此数据，开发了 ReProver：第一个增加检索功能的基于 LLM 的证明程序。其成本低
PDFa year ago
启发式规划的定理证明
本研究介绍了一种利用启发式算法解决定理证明和计划制定问题的方法，并将其应用于 situation calculus 中。该方法通过使用 A * 搜索算法排列一系列情境，并利用删除松弛法控制启发式规划器，获得较短的计划方案，并探索较少的状态。
PDFa year ago
反升级和泛化：一项调查
本文首次对 AU 研究及其应用进行了概述和分类，以及提供了一般框架，为现有和未来的发展分类。
PDFa year ago
通过定理证明对神经网络进行受限训练
本文提出了一种基于定理证明的方法，在神经网络的训练中规范和生成时间逻辑约束。通过 Isabelle 定理证明器的高阶逻辑，形式化嵌入线性时间逻辑，提出了一个损失函数，并使用 OCaml 版本制作的 PyTorch 模型进行了训练。结果表明，
PDF2 years ago
自然证明器：基于语言模型的数学证明生成
通过人工提供或查找背景参考条件，NaturalProver 能够生成数学证明，融合符号和自然语言，提高了下一步建议和生成证明的质量，在某些需要短证明的定理上具有证明能力，并且提供的下一步建议有超过 40% 的正确和有用率。
PDF2 years ago
Thor: 锤炼联合语言模型和自动定理证明器
该论文介绍了 Thor，一个集成语言模型和自动定理证明器的框架，它采用一种称为 “hammers” 的方法来选择前提，从而增加了语言模型在 PISA 数据集上的成功率并解决了相当一部分问题，同时比现有最佳方法在 MiniF2F 数据集上具有
PDF2 years ago