Training Neural Networks using SAT solvers
We propose an algorithm to explore the global optimization method, using SAT
solvers, for training a neural net. Deep Neural Networks have achieved great
feats in tasks like-image recognition, speech recognition, etc. Much of their
success can be attributed to the gradient-based optimisation methods, which
scale well to huge datasets while still giving solutions, better than any other
existing methods. However, there exist learning problems like the parity
function and the Fast Fourier Transform, where a neural network using
gradient-based optimisation algorithm can not capture the underlying structure
of the learning task properly. Thus, exploring global optimisation methods is
of utmost interest as the gradient-based methods get stuck in local optima. In
the experiments, we demonstrate the effectiveness of our algorithm against the
ADAM optimiser in certain tasks like parity learning. However, in the case of
image classification on the MNIST Dataset, the performance of our algorithm was
less than satisfactory. We further discuss the role of the size of the training
dataset and the hyper-parameter settings in keeping things scalable for a SAT
solver.