May, 2023

Chronosymbolic Learning: 采用符号推理和归纳学习的高效 CHC 求解

PDF
TL;DR本论文提出了 Chronosymbolic Learning 这一基于数据驱动的框架，结合符号信息和数值数据点解决 Constrained Horn Clauses（CHC）系统，此工具在包含许多非线性整数算术实例的数据集上表现出比现有 CHC 求解器更高的性能。
constrained horn clausesdata-driven approachchronosymbolic learningnumerical data pointsbounded model checking
发现论文，激发创造
  • 使用 GNN 探索 Horn 子句的表示（扩展技术报告）

    本文提出了一种新的基于图的编程语义学习方法 - 关系超图神经网络（R-HyGNN），通过学习规约角色（Constrained Horn Clauses）的图形表示，提供了一种有效的语言无关的程序特征提取方式，并在 CHC-COMP 2021 基准上展示了一系列任务的准确性。

    Jun, 2022

  • 神经符号融合带来因果和可靠推理证明

    通过神经符号一体化方法，结合 LLMs 和符号求解器，实现了确定性执行性质的推理证明，提高了准确性和证明相似度。

    Nov, 2023

  • 符号表示对于背景下少样本推理学习的影响

    本研究的主要目标是使用预先训练的语言模型来进行推理，特别是在推理时使用解释以增强上下文学习。作者将神经符号方法重新引入到这个任务中，并将语言模型作为逻辑程序员，以在知识库中迭代推理。实验结果表明，相对于上下文学习策略， LMLP 在演绎和长度归纳基准测试中表现得更加优秀。

    Dec, 2022

  • 用角 - ICE 学习方法合成不变量和契约

    本研究基于 Horn implication counterexamples (Horn-ICE) 设计了学习算法，提出了一种决策树学习算法，可以从 Horn-ICE 样本中学习并在多项式时间内工作。使用统计启发式学习小树的方法，以满足样本。实验结果表明，我们算法的实现可以高效地为各种顺序和并发程序学习充分的归纳式不变量和契约。

    Dec, 2017

  • 通过符号化推理保持逻辑的准确性

    提出了一种基于大型语言模型的新型符号化思维链 (SymbCoT) 框架，通过将符号表达和逻辑规则与语言模型集成，以增强其逻辑推理能力，并在 5 个标准数据集上通过深入评估展示了显著的性能提升。

    May, 2024

  • 机器学习与赫布兰宇宙

    本文介绍了一种基于机器学习和 Herbrand 定理的方法，选取有限的 Herbrand universe 中的正确实例，以便将一阶逻辑问题转化成命题问题，并证明了该方法在多种数学问题中具有高准确性。

    Oct, 2022

  • Logic-LM: 使用符号求解器增强大型语言模型进行可靠的逻辑推理

    Logic-LM 是一种将大型语言模型与符号推理相结合的框架，通过首先使用大型语言模型将自然语言问题转化为符号形式，然后进行确定性符号求解，以及自我精炼阶段来修正符号形式，在 ProofWriter、PrOntoQA、FOLIO 和 LogicalDeduction 等四个逻辑推理数据集上的结果表明，与仅使用大型语言模型相比，我们的方法可以显著提高逻辑推理的性能。

    May, 2023

  • 约束神经网络用于解释式启发式创建优化计算代数系统

    我们提出了一种利用机器学习技术进行符号计算研究的新方法。我们解释了如何将人类设计的在圆柱代数分解中选择变量顺序的启发式方法表示为受限神经网络。这使我们能够使用机器学习方法进一步优化这个启发式方法，得到与原始人类设计相似复杂度的新网络和新启发式。我们将其作为一种事前可解释性方法用于计算机代数开发。

    Apr, 2024

  • 大型语言模型的符号能力研究

    研究证实，大型语言模型在处理基于符号的任务时面临符号复杂度上升的挑战，强调了需要专门的训练、内存和架构调整以提高它们在符号推理任务中的熟练度。

    May, 2024

  • 在真实图像上实现符号推理：标定概念和操作

    提出了 Calibrating Concepts and Operations（CCO）方法，旨在通过学习概念嵌入矢量和操作校准器解决真实图像数据中长尾概念分布和推断步骤不平等重要性的问题，并在真实世界数据集 GQA 上大幅提升神经符号方法的性能。

    Oct, 2021