Károly Zsolnai-Fehér explains NeuroSAT, a neural network trained to solve Boolean satisfiability problems using only yes/no labels. It learns to find actual solutions, not just verify them, and generalizes to harder problems than it saw during training, though traditional solvers built over decades still match its performance.
Dear fellow scholars, this is two minute papers with please meet Neural set. The name of this technique tells us what it is about. The neural part means that it is a neural network based learning method, and the set part means that it is able to solve satisfiability problems. This is a family of problems where we are given a logic formula and we have to decide whether these variables can be chosen in a way such that this expression comes out true. That of course sounds quite nebulous. So let's have a look at a simple example. This formula says that F is true if A is true and at the same time not B is true. So if we choose A to be true and B as false, this expression is also true. Or in other words, this problem is satisfied. Getting a good solution for set is already great for solving many problems involving logic. And however, the more interesting part is that it can help us solve an enormous set of other problems. For instance, ones that involve graphs describing people in social networks and many others that you see here. This can be done by performing something that mathematicians like to call polynomial time reduction or car production. Which means that many other problems that seem completely different can be converted into a set problem. In short, if you can solve SAT well, you can solve all of these problems well. This is one of the amazing revelations I learned about during my mathematical curriculum. The only problem is that when trying to solve big and complex SAT problems, we can often not do much better than random guessing, which for some of the most nasty cases takes so long that it practically is never going to finish. And get this. Interestingly, this work presents us with a neural network that is able to solve problems of this form, but not like this tiny, tiny baby problem, but much bigger ones. And this really shouldn't be possible. Here's why. To train a neural network, we require training data. The input is a problem definition and the output is whether this problem is satisfiable. And we can stop right here, because here lies our problem. This doesn't really make any sense because we just said that it is difficult to solve big set problems. And here comes the catch. This neural network learns from set problems that are small enough to be solved by traditional handcrafted methods. We can create arbitrarily many training examples with these solvers, albeit these are all small ones. And that's not it. There are three key factors here that make this technique really work. One, it learns from only single bit supervision. This means that the output that we talked about is only yes or no. It isn't shown the solution itself. That's all the algorithm learns from two when we request a solution from the neural network, it not only tells us the same binary yes, no answer, but but it can go beyond that. And when the problem is satisfiable, it will almost always provide us with the exact solution. It is not only able to tell us whether the problem can be solved, but it almost always provides a possible solution as well. That is indeed remarkable. This image may be familiar from the thumbnail and here you can see how the neural network's inner representation of how these variables change over time as it sees a satisfiable or unsatisfiable problem, and how it comes to its own conclusions. And three when we ask the neural network for a solution, it is able to defeat problems that are larger and more difficult than the ones it has trained on. So this means that we train it on simple problems that we can solve ourselves, and using these as training data, we will be able to solve much harder problems and that we can't solve ourselves. This is crucial because otherwise this neural network would only be as good as the handcrafted algorithm used to train it. Which, in other words, is not useful at all. Isn't this amazing? I will note that there are handcrafted algorithms that are able to match and often outperform neural set. However, this took decades of research work to invent. Whereas this is a learning based technique that just looks at as little information as the problem definition and whether it is satisfiable and it is able to come up with a damn good algorithm by itself. What a time to be alive. This video has been kindly supported by my friends at AAM Research. Make sure to check them out through the link in the video description. Thanks for watching and for your generous support and I'll see you next time.
