Integrating logical reasoning within deep learning architectures has been a goal of modern AI systems. In this paper, we propose a new direction this goal by introducing a differentiable (smoothed) maximum (MAXSAT) solver that can be integrated into the loop of larger learning systems. Our (approximate) solver is based upon a fast coordinate approach to solving the semidefinite program (SDP) associated with the problem. We show how to analytically differentiate through the solution this SDP and efficiently solve the associated backward pass. We demonstrate by integrating this solver into end-to-end learning systems, we can learn logical structure of challenging problems in a minimally supervised. In particular, we show that we can learn the parity function using-bit supervision (a traditionally hard task for deep networks) and learn to play 9x9 Sudoku solely from examples. We also solve a "visual Sudok" that maps images of Sudoku puzzles to their associated logical by combining our MAXSAT solver with a traditional convolutional. Our approach thus shows promise in integrating logical structures deep learning.
No takes yet. Share an insight, caveat, or question.
Wang et al. (2019) studied this question.