SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver (2019-05-24T00:00:00.000000Z)

TL;DR

This paper introduces a differentiable (smoothed) maximum satisfiability (MAXSAT) solver that can be integrated into the loop of larger deep learning systems and demonstrates that by integrating this solver into end-to-end learning systems, this approach shows promise in integrating logical structures within deep learning.

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) maximum satisfiability (MAXSAT) solver that can be integrated into the loop of larger deep learning systems. Our (approximate) solver is based upon a fast coordinate descent approach to solving the semidefinite program (SDP) associated with the MAXSAT problem. We show how to analytically differentiate through the solution to this SDP and efficiently solve the associated backward pass. We demonstrate that by integrating this solver into end-to-end learning systems, we can learn the logical structure of challenging problems in a minimally supervised fashion. In particular, we show that we can learn the parity function using single-bit supervision (a traditionally hard task for deep networks) and learn how to play 9x9 Sudoku solely from examples. We also solve a "visual Sudok" problem that maps images of Sudoku puzzles to their associated logical solutions by combining our MAXSAT solver with a traditional convolutional architecture. Our approach thus shows promise in integrating logical structures within deep learning.

Authors

Bryan Wilder

5 papers

Zico Kolter

3 papers

Po-Wei Wang

2 papers

TL;DR

Abstract

Authors

References33 items

Low-rank semidefinite programming for the MAX2SAT problem

Melding the Data-Decisions Pipeline: Decision-Focused Learning for Combinatorial Optimization

DeepLogic: Towards End-to-End Differentiable Logical Reasoning

DeepLogic: End-to-End Logical Reasoning

Lifted Relational Neural Networks: Efficient Learning of Latent Relational Structures

What game are we playing? End-to-end learning in normal and extensive form games

DeepProbLog: Neural Probabilistic Logic Programming

Differentiable Submodular Maximization

Recurrent Relational Networks for Complex Relational Reasoning

Learning a SAT Solver from Single-Bit Supervision

Tunneling Neural Perception and Logic Reasoning through Abductive Learning

A Semantic Loss Function for Deep Learning with Symbolic Knowledge

Recurrent Relational Networks

Learning Explanatory Rules from Noisy Data

The Mixing method: coordinate descent for low-rank semidefinite programming

The Mixing method: low-rank coordinate descent for semidefinite programming with diagonal constraints

Failures of Gradient-Based Deep Learning

OptNet: Differentiable Optimization as a Layer in Neural Networks

Task-based End-to-end Model Learning in Stochastic Optimization

Differentiable Learning of Logical Rules for Knowledge Base Reasoning

Harnessing Deep Neural Networks with Logic Rules

Neural-Symbolic Learning and Reasoning: Contributions and Challenges

Adam: A Method for Stochastic Optimization

The Power of Semidefinite Programming Relaxations for MAX-SAT

On the Rank of Extreme Matrices in Semidefinite Programs and the Multiplicity of Optimal Eigenvalues

Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming

Problems of distance geometry and convex properties of quadratic maps

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

Differentiable Learning of Submodular Models

Can neural networks crack sudoku?, 2016

GradientBased Learning Applied to Document Recognition

Gradient-based learning applied to document recognition

On the Rank of Extreme Matrices in Semideenite Programs and the Multiplicity of Optimal Eigenvalues

Field of Study

Venue Information

Name

Type

URL

Alternate Names