Proving properties of binary classification neural networks via Lukasiewicz logic

Neural networks are widely used in systems of artificial intelligence, but due to their black box nature, they have so far evaded formal analysis to certify that they satisfy desirable properties, mainly when they perform critical tasks. In this work, we introduce methods for the formal analysis of reachability and robustness of neural networks that are modeled as rational McNaughton functions by, first, stating such properties in the language of Lukasiewicz infinitely-valued logic and, then, using the reasoning techniques of such logical system. We also present a case study where we employ the proposed techniques in an actual neural network that we trained to predict whether it will rain tomorrow in Australia.