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.
Metadata: arXiv. Abstracts retain their original authors’ rights.
In the conversation
Original HN comments, with labels from simple text rules. A label describes the whole comment and may miss context or irony. Read the discussion to make up your own mind. About the labels
SATnet is an interesting paper, in this regard. It's built on a theory of backpropping through the semi-definite programming relaxation of a MAXSAT problem, to learn the MAXSAT problem associated with a class of training examples. It gets good results: learns to solve sudoku puzzles with only binary feedback on its performance (i.e. "that's the solution" or "that's not the solution", no partial feedback on partially-correct solutions). They say it's the first time a neural net has been able to do that. On the other hand, if you look at the coefficient matrix they learn for the MAXSAT problem, it doesn't correspond to any logical proposition because the overwhelming…
Read the full comment
majority of the learned coefficients are close to 0, whereas in the representation of a MAXSAT problem, the coefficients must be -1, 0 or 1, where 0 means the corresponding variable doesn't occur.
Is it a major result? Well I'm certainly impressed. Do we understand what the network is doing? I don't think we do... I'm still glad to have read the paper, though. I don't know what standard you would hold researchers to, to let through results like SATnet but reject spray-and-pray results which only look good because of offline multiple sampling. If you could require a lab notebook of authors, detailing every step of development, that might work.
https://arxiv.org/abs/1905.12149
There are architectures with layers which can approximate MAXSAT [1] (or rather, an SDP relaxation thereof), but I doubt this is what OP was referring to.
[1]: https://arxiv.org/abs/1905.12149
You might be interested in the line of work around differentiable relaxations of formal solvers that was kicked off by Zico Kolter et al. They add a Max=SAT solver as a differentiable layer. This allows the neat trick of solving handwritten Sudoku puzzles by composing a ConvNet with the differentiable Max-SAT layer.
[1] https://arxiv.org/abs/1905.12149
Recent work has demonstrated substantial gains on many NLP tasks and benchmarks by pre-training on a large corpus of text followed by fine-tuning on a specific task.
Despite their massive size, successful deep artificial neural networks can exhibit a remarkably small difference between training and test performance.