SATNet: 使用可微可满足性求解器桥接深度学习与逻辑推理

ICMLMay, 2019

SATNet: 使用可微可满足性求解器桥接深度学习与逻辑推理

SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver

Po-Wei Wang, Priya L. Donti, Bryan Wilder, Zico Kolter

TL;DR本文提出了一种新的路线，即通过引入可微（平滑）的最大可满足性（MAXSAT）求解器，将逻辑推理纳入更大的深度学习系统的循环中，从而在端到端学习系统中学习有挑战性的问题的逻辑结构，表现出集成逻辑结构于深度学习的潜力。

Abstract

Integrating logical reasoning within deep learning architectures has been a major goal of modern AI systems. In this paper, we propose a new direction toward this goal by introducing a differentiable (smoothed) m

logical reasoning deep learning maxsat solver minimally supervised learning integrating logical structures

发现论文，激发创造

使用 SATNet 学习可靠的逻辑规则

通过可区分性学习生成可解释和可验证的逻辑规则，该方法通过最大可满足性求解器（SATNet）学习可解释的逻辑规则，并引入验证技术进行验证，从而实现了逻辑推理和深度学习的交互。

Oct, 2023

torchmSAT：一个 GPU 加速的最大可满足性问题的近似算法

利用机器学习技术将离散结构与组合优化算法集成，提出一种能够近似求解最大满足性问题的可微函数，设计了一种新颖的神经网络结构并借助后向传播逐步求解问题，通过利用 GPU 进行计算加速，论文实验证明这种方法在挑战性的最大满足性问题上优于两种现有求解器，并与另一种求解器在解决成本方面相当，而无需进行训练或使用底层 SAT 求解器，为基于神经网络 GPU 加速的新一代求解器铺平了道路。

Feb, 2024

利用深度学习构建带性能界限的随机局部搜索 SAT 求解器

利用图神经网络训练适用于布尔可满足性问题的 SLS 求解器，可显著提高性能，平均解决比例更高、步骤更少，具有性能保证。

Sep, 2023

评估 SATNet 解决符号基础问题的能力

SATNet 是一个奖 - winning 的 MAXSAT 求解器，可以用来推断逻辑规则并作为深度神经网络中的可微分层。本文通过展示，在缺乏标识个别数独数字图像及其逻辑表示的中间标签的情况下，SATNet 在视觉数独上彻底失败（0％的测试准确性），澄清了 SATNet 的能力。一般来说，这个失败可以归因于 SATNet 无法学会将符号分配给感知现象，也就是所谓的符号基础问题，这被认为是智能代理执行真实世界逻辑推理的先决条件。我们提出了基于 MNIST 的测试，作为符号基础问题的简单实例，可以作为可微分符号求解器的健全性检查。对于这个测试的 SATNet 的朴素应用导致性能比没有逻辑推理能力的模型更差。我们报告了 SATNet 失败的原因以及如何防止它们。

Dec, 2023

可扩展的深度学习与逻辑推理的耦合

本文介绍了一种可扩展的神经网络结构和损失函数，专门用于学习离散图形模型所表达的 NP-hard 解决问题的约束和标准，并在实践中证明其能够高效地从自然输入中学习如何解决 NP-hard 推理问题，具有数据效率，可解释性和后验控制。

May, 2023

SoLA：基于求解器层适应的 LLM 在逻辑推理中的应用

对大型语言模型（LLMs）在逻辑推理中所面临的挑战，以及利用工具学习改变问题求解的过程进行了探讨。本文提出了一种新颖的解算器层自适应（SoLA）方法，通过将解算器作为 LLMs 的新层，以不同的方式引导解决方案朝着可满足性发展。通过利用 MaxSAT 作为桥梁，定义正向和反向转移梯度，使最终模型能够收敛到满足的解决方案或证明不可满足性。通过验证 SoLA 在各种数据集上的性能，实证证明了其在大规模问题求解的效率上相对于现有的符号求解器（包括 Z3 和 Kissat）和工具学习方法的持续优势。

Feb, 2024

DeepSAT: 一种基于 EDA 驱动的 SAT 学习框架

提出了 DeepSAT 框架，使用 EDA 领域的知识来解决布尔可满足性问题（Boolean satisfiability），通过逻辑合成算法将 SAT 实例预处理为优化的与非图（AIGs），并利用 DAGNN 训练条件生成模型，在各种 SAT 实例上实现了显著的准确度提高。

May, 2022

使用 SATNet 学习对称规则

本文提出一个名为 SymSATNet 的 SATNet 变体，它利用给定的对称性来求解逻辑谜题，从而实现参数学习，旨在缩小依赖于输入输出对的规则的学习量，本质上改善了 SATNet 的性能。

Jun, 2022

基于采样的多模型优化的可导可满足性和可导答案集编程

本文介绍了 Differentiable SAT/ASP 方法，使用梯度下降分支机制采样不同模型进行多模型优化，其主要应用包括分布感知模型采样和富有表现力的可扩展概率逻辑编程，并提出了算法性能检测软件 DelSAT，实验表明该方法性能强劲，远优于与之相比的其他方法。

Dec, 2018

使用 MaxSAT 优化二进制决策图以进行分类

本文提出了基于 SAT 的方法学习最优二元决策图（BDD），以更好地实现可解释的机器学习模型，并给出了一种整合兼容子树的方法，该方法与现有方法相比在预测质量和可解释性方面具有明显的优势。

Mar, 2022