5 ms·
SATNet: Bridging deep learning and logical reasoning with differentiable SAT
- mlevental 7y agothere's also this https://arxiv.org/abs/1812.11948 https://arxiv.org/abs/1812.11948
- riskneutral 7y agoThis seems like a promising direction.
- yters 7y agoGreat, hopefully this'll get us past the halting problem.
- mpoteat 7y agoThe halting problem is formally proven to be undecidable.
- dllthomas 7y agoIn 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.
- viksit 7y agoCan 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?
- sanxiyn 7y agoILP 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.
- viksit 7y agoTo clarify - ILP meaning Inductive Logic Programming vs Integer Linear Programming?
- sanxiyn 7y agoInductive Logic Programming. DeepMind work in question is https://arxiv.org/abs/1711.04574 https://arxiv.org/abs/1711.04574.
- Loq 7y agoILP usually translates to SAT. You can see ILP as a high-level interface to SAT.
- YeGoblynQueenne 7y agoI think you mean ILP as in Integer Linear Progamming. The quote above mentioned δILP which is "differentiable Inductive Logic Programming".
- Loq 7y agoNo. 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.
- YeGoblynQueenne 7y agoTo 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.
- donpark 7y agocode: https://github.com/locuslab/satnet https://github.com/locuslab/satnet
- phonicwheel 7y agoand there's also this: https://github.com/MatthiasNickles/delSAT https://github.com/MatthiasNickles/delSAT