theorem prover | BriefGPT - AI 论文速递

关键词theorem prover

搜索结果 - 10

递归证明定理
POETRY 使用逐级递归的方式在 Isabelle 定理证明机中证明定理，通过在每一级搜索可验证的证明草图并专注于解决当前级别的定理或猜想，从而解决了自动定理证明中的挑战。
PDFa month ago
LINC: 将语言模型与一阶逻辑证明器相结合的神经符号化逻辑推理方法
通过使用神经符号计算来全面利用 LLMs 和符号化证明器，本文探索了以逻辑推理任务，特别是符合自然语言的任务为基础的解决方案。
PDF8 months ago
一种新的自动形式化方法
自动形式化研究级数学的一个方法是将任务分解为更容易和可接近的子任务：未链接的形式化、实体链接和类型调整。同时，本文还提出了一个用于未链接的形式化的基准数据集 arXiv2Formal，其中包含了从 arXiv.org 的论文中选取的 50
PDF9 months ago
依赖类型高阶逻辑中的定理证明 —— 扩展预印本
介绍了 DHOL 的依赖类型扩展是如何保留了 HOL 的风格和概念框架，并且使用 DHOL 定理证明器实现了从 DHOL 到 HOL 的翻译，进而获得 DHOL 的定理证明器。
PDFa year ago
自然语言推理问题中使用语言模型进行知识获取
本文通过在逻辑单词谜题上比较使用 ChatGPT 和 GPT-4 直接解决问题和提取问题文本事实并使用定理证明器解决两种方法，并得出后者是正确的方法来研究了利用大语言模型解决自然语言问题需要一些非平凡的推理。
PDFa year ago
利用大型语言模型实现数学形式化辅助工具
本研究使用大型语言模型 (Codex) 探讨将使用自然语言书写的数学（即定义，定理陈述和证明）转化为可以被程序检查正确性的形式语言的能力，并发现对于 120 个定理，Codex 可以在本科水平上以近 75％的准确率进行短数学陈述的形式化。同
PDF2 years ago
MMCheckINN：Imandra 中的宽范围神经网络验证（扩展版）
本文介绍了如何使用 Imadra 编程语言和定理证明器来设计开发适用于神经网络验证的 CheckINN 库。
PDF2 years ago
Budge：一种编程语言和定理证明器
基于哥德尔编号和质因数分解的简单编程语言，配合具有显式作用域的循环和定理证明器，可以表示和工作于形式系统。编程语言和定理证明器之间可以相互表示，并提供实例程序和它们的求值。
PDF2 years ago
ICLRIsarStep: 高层次数学推理的基准测试
本文提出了一种用于高级数学推理的数据集，研究了神经序列到序列模型的推理能力。实验结果表明，该任务具有挑战性，但神经模型能够捕捉到非平凡的数学推理，提出的分层 Transformer 的性能也好于基准 Transformer。
PDF4 years ago
一阶 MDP 的近似线性规划
本文提出了一种基于线性规划的解决方法，通过将价值函数在一组一阶基函数的线性表示中计算适当的权值，解决了一阶马尔科夫决策过程中与特定领域实例无关的解决方案。并将该解决方法应用于电梯调度方面，具有丰富的特征空间和多标准加性奖励，证明了其优于许多
PDF12 years ago