ML Newsnew | past | best | rss | submit about
SATNet: Bridging deep learning and logical reasoning with differentiable SAT (arxiv.org)
116 points by pizza on Jun 3, 2019 | hide | past | pdf | 17 comments on HN

In plain words: A smoothed logic solver plugs into a neural network's training loop, letting learning signals flow through it so the net can pick up logical rules. It learned the parity task from single-bit labels and 9x9 Sudoku from examples alone, tasks deep networks struggle with.

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

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.

Po-Wei Wang, Priya L. Donti, Bryan Wilder, Zico Kolter
arXiv:1905.12149 · cs.LG, cs.AI, stat.ML · submitted May 29, 2019
abstract · pdf · html · Accepted at ICML'19. The code can be found at https://github.com/locuslab/satnet

add comment on HN

mlevental on Jun 3, 2019 [–]
there's also this https://arxiv.org/abs/1812.11948
reply
phonicwheel on Jun 4, 2019 [–]
and there's also this: https://github.com/MatthiasNickles/delSAT
reply
viksit on Jun 4, 2019 [–]
Can someone comment on the deeper distinctions between this and DeepMinds ILP paper on learning explanatory rules from noisy data? AFAIK thats a special case of SAT?
reply
sanxiyn on Jun 4, 2019 | parent [–]
ILP and SAT are quite different. ILP is much higher level in that it can define new predicates and do recursion, which have no counterparts in SAT. On the other hand, SAT is much more scalable and can be applied to instances orders of magnitude larger. I think ILP's expressiveness and lack of scalability are related.
reply
YeGoblynQueenne on Jun 4, 2019 | parent [–]
To complement this.

Inductive Logic Progamming (ILP) is a class of machine learning algorithms that learn logic programs from examples and background knowledge (where background knowledge is a logic theory, i.e. another logic program, as ar the examples).

SAT is the boolean satisfiability problem, the problem of finding variable assignments to the variables of a boolean formula that make the formula true.

So the two are not similar and one is not an instance of the other.

The δILP paper describes a differentiable ILP system that learns logic programs with a differentiable logic representation.

Finally, the paper above (SATNet) describes a differentiable satisfiabiilty solver that can be incorporated in a neural network architecture to enable the nerual net to solve satisfiability problems and perform reasoning.

reply
samsara80 on Jun 5, 2019 | parent [–]
Looks like they (SATNet) are not incorporating a real (exact) SAT solver but their differentiable "SAT solver" is a MAXSAT estimator which gives an approximation of the maximum number of clauses that can be made true.
reply
YeGoblynQueenne on Jun 5, 2019 | parent [–]
Thanks. I should read this more carefully - I just skimmed it, to be honest.
reply
viksit on Jun 4, 2019 | parent [–]
To clarify - ILP meaning Inductive Logic Programming vs Integer Linear Programming?
reply
sanxiyn on Jun 4, 2019 | parent [–]
Inductive Logic Programming. DeepMind work in question is https://arxiv.org/abs/1711.04574.
reply
Loq on Jun 4, 2019 | parent [–]
ILP usually translates to SAT. You can see ILP as a high-level interface to SAT.
reply
YeGoblynQueenne on Jun 4, 2019 | parent [–]
I think you mean ILP as in Integer Linear Progamming. The quote above mentioned δILP which is "differentiable Inductive Logic Programming".
reply
Loq on Jun 6, 2019 | parent [–]
No.

I meant was ASP is a higher level 'interface' to SAT, sorry for the confusion. Work done at Imperial by Law and Evans in ILP compiles down to SAT solving via ASP. IDK if δILP goes to SAT.

reply
riskneutral on Jun 3, 2019 [–]
This seems like a promising direction.
reply
donpark on Jun 4, 2019 [–]
code: https://github.com/locuslab/satnet
reply
yters on Jun 3, 2019 [–]
Great, hopefully this'll get us past the halting problem.
reply
mpoteat on Jun 4, 2019 | parent [–]
The halting problem is formally proven to be undecidable.
reply
dllthomas on Jun 4, 2019 | parent [–]
In some senses we are past the halting problem once we accept that that we will sometimes be wrong or unable to answer. Insofar as it has anything to do with the halting problem, this seems just another way to do that. Might still be useful.
reply
About | RSS | RSS (all) | HN arXiv