Learning First-Order Symbolic Representations for Planning from the Structure of the State Space
Universidad Simón Bolívar（西蒙·玻利瓦尔大学）；ICREA（加泰罗尼亚高等研究院）；Universitat Pompeu Fabra（庞培法布拉大学）
开发灵活的人工智能系统的主要障碍之一是基于数据的学习者和基于模型的求解者之间的分裂。求解器，如经典的规划是非常灵活的，可以处理各种问题的实例和目标，但需要一阶的符号模型。另一方面，基于数据的学习器是鲁棒的，但不产生这样的表示。在这项工作中，我们解决这个分裂，显示如何使用的规划者的一阶符号表示可以从非符号输入，编码的状态空间的结构。表示学习问题被公式化为在一个共同但未知的一阶域上推断规划实例的问题，该一阶域解释了所观察到的状态空间的结构。这意味着推断出一个完整的一阶表示（即一般动作模式，关系符号和对象），它解释了观察到的状态空间结构。推理问题被转换为两级组合搜索，其中外层搜索一小组超参数的值，内层通过SAT求解，搜索一阶符号模型。该框架产生一般和正确的一阶表示的标准问题，如夹具，Blocksworld，和河内输入图编码的平面状态空间结构的一个实例。
2020-02-20 cs.AI
Differentiable Symbolic Planning: A Neural Architecture for Constraint Reasoning with Learned Feasibility
Sithara Inc.（Sithara公司）
本文提出可微符号规划（DSP），通过神经架构实现离散符号推理并保持全可微性，结合通用认知内核（UCK）在约束推理基准中取得高准确率。
2026-02-19 cs.AI cs.LG
Benchmarking Symbolic Execution Using Constraint Problems -- Initial Results
IIT Kanpur（印度理工学院坎普尔分校）；National University of Singapore（新加坡国立大学）
符号执行是一种功能强大的bug发现和程序测试技术。它可以成功地发现真实代码中的bug。核心推理技术使用约束求解、路径探索和搜索，这些也是用于解决组合问题的相同技术，例如，有限域约束满足问题。我们提出CSP实例作为更具挑战性的基准来评估符号执行中核心技术的有效性。我们将CSP基准转换为适合测试符号执行工具的推理能力的C程序。从一个单一的CSP P，我们转换P取决于转换选择到不同的C程序。使用KLEE、Tracer-X和LLBMC工具进行的初步测试显示，转换和求解器选择在运行时存在很大差异。我们的C基准测试有效地显示了现有符号执行工具的局限性。这项工作的动机是，我们相信这种形式的基准可以刺激符号执行引擎中改进的核心推理的开发和工程。
2020-01-22 cs.AI cs.SE
A Model-Agnostic SAT-based Approach for Symbolic Explanation Enumeration
CRIL（朗斯计算机科学实验室）；Univ. Artois（阿图瓦大学）；CNRS（法国国家科学研究中心）
在本文中，我们提出了一个通用的不可知的方法，允许生成不同的和互补类型的符号解释的符号解释的模型不可知SAT为基础的方法。更准确地说，我们通过分析特征和输出之间的关系来生成解释，以局部解释单个预测。我们的方法使用一个命题编码的预测模型和SAT为基础的设置生成两种类型的符号解释，这是充分的理由和反事实。在图像分类任务上的实验结果表明了该方法的可行性及其在提供充分理由和反事实解释方面的有效性。
2022-08-15 cs.AI
ASTERYX : A model-Agnostic SaT-basEd appRoach for sYmbolic and score-based eXplanations
Univ. Artois（阿尔图瓦大学）；CNRS（法国国家科学研究中心）；CRIL（计算机科学与基础信息实验室）
在实践中越来越多地使用机器学习技术的复杂性不断增加，这就需要解释这些模型的预测和决策，这些模型通常被用作黑箱。可解释的人工智能方法要么是基于数值特征的，旨在量化每个特征在预测中的贡献，要么是提供某些形式的符号解释（如反事实）的符号解释。本文提出了一种通用的不可知论的方法，名为ASTERY X允许生成符号解释和分数为基础的。我们的方法是声明性的，它是基于编码的模型被解释在一个等效的符号表示，后者用于生成特别是两种类型的符号解释，这是充分的理由和反事实。然后，我们将分数与一些属性相关联，这些分数反映了解释和特征w.r.t的相关性。我们的实验结果表明，所提出的方法的可行性和有效性，在提供符号和分数为基础的解释。
2022-06-23 cs.AI
SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers
University of Toronto（多伦多大学）
本研究提出SAT-RL强化学习框架，训练大型语言模型与Z3等符号求解器交互，通过合成数据、监督预热及工具感知奖励提升逻辑推理性能，在域内外任务均获显著效果。
2026-10-14 cs.AI cs.SC
When Do Symbolic Solvers Enhance Reasoning in Large Language Models?
University College London（伦敦大学学院）；University of Oxford（牛津大学）
本文研究符号求解器如何在大语言模型中增强推理，发现其在需要有限隐式推理但具有充足搜索空间的问题中表现优异，尤其在约束满足问题中提升显著。
2025-12-02 cs.AI
Identifying Good Rules for Efficient SAT Encodings of Single-Constant Multiplication Using Machine Learning
研究单常数乘法问题的高效SAT编码，提出神经符号框架，用图神经网络预测运算符类型，利用置信分数修剪搜索选择，实验表明该方法能大幅提升编码的可扩展性与效率，减少时间、内存及分支。
2026-07-24 cs.AI
AS2 -- Attention-Based Soft Answer Sets: An End-to-End Differentiable Neuro-Soft-Symbolic Reasoning Architecture
Clemson University（克莱姆森大学）
AS2提出一种端到端可微的神经-软符号推理架构，通过软连续近似替代离散求解器，实现约束满足反馈的可微传递，提升在视觉数独和MNIST加法任务中的性能。
2026-11-05 cs.AI
Adaptive Selection of Symbolic Languages for Improving LLM Logical Reasoning
本文提出一种自适应选择符号语言的方法，通过在翻译前为不同自然语言逻辑推理问题匹配最优符号语言（一阶逻辑、逻辑编程或布尔可满足性），显著提升了LLM的逻辑推理性能。
2025-10-12 cs.AI
Position: Certified Correctness in Neural Constraint Reasoning Requires Symbolic Integration
本文针对神经约束推理在分布偏移下易出现约束违反的问题，提出需优先将神经方法与符号方法双向集成，通过多智能体认证推理框架实现计算效率与可证正确性。
2026-08-18 cs.AI
Differentiable Fuzzy $\mathcal{ALC}$: A Neural-Symbolic Representation Language for Symbol Grounding
National Key Laboratory for Novel Software Technology, Nanjing University（计算机软件新技术全国重点实验室，南京大学）
神经符号计算旨在将强大的神经学习和合理的符号推理集成到一个框架中，以便利用这两种看似无关（甚至可能是矛盾的）AI范式的互补优势。神经-符号计算的核心挑战是将神经学习和符号推理的公式化统一到一个具有公共语义的单一框架中，也就是说，在神经模型和逻辑理论之间寻求一种联合表示，这种联合表示可以支持神经模型学习的基本基础，也可以坚持逻辑理论的语义。在本文中，我们提出了可微模糊$\mathcal{ALC}$（DF- $\mathcal{ALC}$）的这个角色，作为一个神经符号表示语言与所需的语义。DF- $\mathcal{ALC}$统一了描述逻辑$\mathcal{ALC}$和神经模型，用于符号基础;特别是，它通过可区分的概念和角色嵌入将$\mathcal{ALC}$知识库注入神经模型。我们定义了一个层次损失的约束，神经模型学习的接地必须与$\mathcal{ALC}$知识库的语义一致。我们发现，仅仅通过最大化可满足性来捕捉接地的语义并不能合理地修改接地。我们进一步定义了一个基于规则的DF适应符号接地问题的损失。实验结果表明，基于规则丢失的DF- $\mathcal{ALC}$能够以无监督学习的方式提高图像目标检测器的性能，即使在资源不足的情况下也能有效地提高检测器的性能。
2022-12-01 cs.AI
PACE: A Neuro-Symbolic Framework for Plausible and Actionable Counterfactual Explanations
University of Klagenfurt（克拉根福大学）；Norwegian University of Life Sciences（挪威生命科学大学）
提出PACE框架，结合神经网络预测与符号推理，生成符合领域约束的可操作反事实解释，在Adult Income数据集上验证了可行性与可解释性的平衡。
2026-09-14 cs.AI
Eidoku: A Neuro-Symbolic Verification Gate for LLM Reasoning via Structural Constraint Satisfaction
Independent Researcher（独立研究者）
Eidoku通过结构约束满足方法有效检测LLM推理中的结构不一致幻觉，提供神经符号验证机制。
2025-12-19 cs.AI cs.LO
Coachable Agents for Interactive Gameplay
Sony AI, Zurich, Switzerland（索尼AI，苏黎世，瑞士）；Sony AI, North America (various locations)（索尼AI，北美（多地））；Sony AI, Tokyo, Japan（索尼AI，东京，日本）
提出结合通用价值函数近似器与精心选择的训练场景、学习算法和数据增强的框架，使智能体在复杂领域（如《地平线：西之绝境》、《GT赛车》和类人机器人）中实时展现不同风格，同时保持主任务性能。
2026-11-09 cs.AI cs.LG
Deciphering Raw Data in Neuro-Symbolic Learning with Provable Guarantees
Nanjing University（南京大学）
本文提出一种刻画知识库监督信号的新方法并建立可学习性判定准则，首次从理论上解释神经符号混合系统何时成功或失败，并通过基准实验验证其有效性。
2024-01-23 cs.AI cs.LG
Learning How to Cube
Yale University（耶鲁大学）；AWS Agentic AI（AWS智能体AI）
本文提出一种神经符号后训练框架，通过MCTS数据整理管道和符号启发式方法，使4B参数模型在SAT竞赛基准上取得53的pass@5分数，超越了Claude-Sonnet-4等前沿LLM。
2026-11-10 cs.AI cs.LG cs.LO
Symbol Correctness in Deep Neural Networks Containing Symbolic Layers
School of Computing and Information Systems, University of Melbourne（墨尔本大学计算与信息系统学院）
本文提出符号正确性概念，作为神经符号深度神经网络（NS-DNN）中神经层预测符号与真实符号一致性的原则，证明其对可解释性和迁移学习必要，并揭示训练权衡。
2024-02-06 cs.AI cs.LG
Graph Neural Networks Meet Neural-Symbolic Computing: A Survey and Perspective
UFRGS（里约热内卢联邦大学）；City, University of London（伦敦城市大学）；University of Siena（锡耶纳大学）；Université Côte d’Azur（蔚蓝海岸大学）；Rice University（莱斯大学）
神经符号计算现在已经成为学术和工业研究实验室感兴趣的主题。图神经网络在关系和符号领域有着广泛的应用，在组合优化、约束满足、关系推理等科学领域有着广泛的应用。一般来说，需要改进人工智能系统的可解释性，可解释性和信任度，这需要有原则的方法，正如神经符号计算所建议的那样。在本文中，我们回顾了使用GNN作为神经符号计算模型的最新技术。这包括GNN在几个领域的应用，以及它与神经符号计算当前发展的关系。
2021-06-12 cs.AI cs.CL cs.LG
Semantic Strengthening of Neuro-Symbolic Learning
最近提出了许多神经符号方法，其目标通常是将符号知识添加到神经网络的输出层。理想情况下，这种损失最大化了神经网络的预测满足基础域的概率。不幸的是，这种类型的概率推理通常在计算上是不可行的。因此，神经符号的方法通常诉诸于模糊近似的概率目标，牺牲声音的概率语义，或采样是很少可行的。我们首先假设约束分解以网络学习的特征为条件来处理这个问题。我们迭代地加强我们的近似，恢复之间的依赖关系的约束最负责降低近似的质量。这对应于计算以网络的学习特征为条件的约束对之间的互信息，并且可以被解释为两个分布的梯度对齐程度的度量。我们将展示如何有效地计算易处理的电路。我们在三个任务上测试我们的方法：预测魔兽争霸中的最小成本路径，预测最小成本完美匹配，以及解决数独难题，观察到它在基线上有所改进，同时避开了棘手问题。
2023-02-28 cs.AI cs.LG
Model-Free Reinforcement Learning for Symbolic Automata-encoded Objectives
University of Southern California（南加州大学）；AIT Austrian Institute of Technology GmbH（奥地利技术研究院有限公司）
针对强化学习依赖状态奖励易致策略不满足任务目标或不安全的问题，提出用符号自动机编码目标，定义非稀疏势能奖励提升收敛性，且能保证策略满足规范。
2022-02-24 cs.AI cs.LO cs.RO
Interpreting Neural Network Judgments via Minimal, Stable, and Symbolic Corrections
MIT（麻省理工学院）；Google Brain（谷歌大脑）
我们提出了一种新的算法来生成最小的，稳定的，符号化的输入校正，这将导致具有ReLU激活的神经网络改变其输出。我们认为，这样的校正是一个有用的方式来提供反馈给用户时，网络的输出是不同于所需的输出。我们的算法通过求解一系列线性约束满足问题来产生这样的校正。该技术进行评估的三个神经网络模型：一个预测申请人是否会支付抵押贷款，一个预测是否一阶定理可以有效地证明由求解器使用一定的数学，最后一个判断是否是一个准确的绘制一只猫的规范图纸。
2018-08-30 cs.AI cs.LG stat.ML
A Semantic Loss Function for Deep Learning with Symbolic Knowledge
University of California, Los Angeles（加州大学洛杉矶分校）；Peking University（北京大学）
本文开发了一种在深度学习中使用符号知识的新方法。从第一原理出发，我们推导出一个语义损失函数，它在神经输出向量和逻辑约束之间架起桥梁。这个损失函数捕获神经网络在多大程度上接近于满足其输出的约束。实验结果表明，该方法能有效地指导学习者在半监督多类分类问题上取得（接近）最新水平的分类结果。此外，它显著提高了神经网络预测结构化对象（如排名和路径）的能力。这些离散的概念非常难以学习，并且受益于深度学习和符号推理方法的紧密集成。
2018-06-08 cs.AI cs.LG cs.LO
NSP: A Neuro-Symbolic Natural Language Navigational Planner
University of Florida（佛罗里达大学）；Florida International University（佛罗里达国际大学）
针对自然语言路径规划中符号方法难处理自由文本、神经方法缺性能保障的问题，提出神经符号框架NSP，结合LLM推理与符号规划及反馈自校正，有效路径率达90.1%且路径更短。
2024-09-13 cs.AI cs.CL cs.HC
Techniques for Symbol Grounding with SATNet
McGill University（麦吉尔大学）；NVIDIA（英伟达）；Mila – Quebec AI Institute（米拉-魁北克人工智能研究所）
许多专家认为，人工智能的未来受到该领域将符号逻辑推理集成到深度学习架构中的能力的限制。最近提出的可微MAXSAT求解器SATNet在与传统神经网络集成并解决视觉推理问题的能力上是一个突破。例如，它可以纯粹从图像示例中学习数独规则。尽管SATNet取得了成功，但它被证明屈服于神经符号系统中的一个关键挑战，即符号基础问题：在没有明确监督的情况下，无法将视觉输入映射到符号变量（“标签泄漏”）。在这项工作中，我们提出了一个自我监督的预训练管道，使SATNet能够克服这一限制，从而扩大了SATNet架构可以解决的问题的类别，包括根本没有中间标签的数据集。我们证明，我们的方法允许SATNet达到完全的准确性，即使有一个更难的问题设置，防止任何标签泄漏。我们还引入了一种校对方法，进一步提高了SATNet架构的性能，击败了Visual Sudoku上的最先进技术。
2021-06-16 cs.AI cs.LG stat.ML
Semantic Referee: A Neural-Symbolic Framework for Enhancing Geospatial Semantic Segmentation
Örebro University（厄勒布鲁大学）；Aalto University（阿尔托大学）
理解为什么机器学习算法可能失败通常是人类专家的任务，人类专家使用领域知识和上下文信息来发现数据或算法中的系统缺陷。在本文中，我们提出了一个语义裁判，它能够提取从深度机器学习框架中出现的错误的定性特征，并提出纠正建议。语义裁判依赖于本体论推理的空间知识，以表征错误的空间与环境的关系。使用语义，推理机作为监督者与学习算法交互。在本文中，提出的方法之间的相互作用的神经网络分类器和语义裁判显示如何提高性能的语义分割的卫星图像数据。
2019-04-30 cs.AI cs.CV cs.LG
A Neural Symbolic Model for Space Physics
Qiuzhen College, Tsinghua University（清华大学求真学院）；Institute for Artificial Intelligence, Peking University（北京大学人工智能研究院）；School of Earth and Space Sciences, Peking University（北京大学地球与空间科学学院）；Max-Planck Institute for Solar System Research（马克斯·普朗克太阳系研究所）；Institute of Space Sciences, Shandong University（山东大学空间科学研究院）；Yau Mathematical Sciences Center, Tsinghua University（叶中天数学科学中心）；Beijing Institute of Mathematical Sciences and Applications（北京数学科学应用研究所）；Department of Mathematical Sciences, Tsinghua University（清华大学数学科学系）；Department of Electronic Engineering, Tsinghua University（清华大学电子工程系）；Institute for AI Industry Research, Tsinghua University（人工智能产业研究院）
本研究提出神经符号模型PhyE2E，通过分解符号回归、结合大模型训练与优化算法提升物理公式发现性能，在空间物理多场景应用中验证了有效性，还改进了NASA旧公式并取得多项新发现。
2025-10-29 astro-ph.EP astro-ph.IM astro-ph.SR
