Chapter 28. Effective Reasoning over Neural Networks Using Łukasiewicz Logic

In this chapter, we present a research line whose aim is to represent neural networks in Łukasiewicz Infinitely-valued Logic (Ł∞) so that one might reason about such neural networks by means of logical machinery. We focus on a class of neural networks with inputs and outputs in the unit interval [0,1] concentrating the study on the ones that compute piecewise linear functions, which is not a strong constraint since such functions may densely approximate any continuous function. For that, we introduce the concept of representation modulo satisfiability, that enlarges the representational power of Ł∞. We derive an algorithm for building such representations, which terminates in polynomial time as long as the input is given in a suitable format. As applications of representation modulo satisfiability, we proceed by showing how properties of neural networks, such as reachability and robustness, may be encoded in Ł∞, giving rise to formal verification techniques. Finally, we present a case study where some formal verifications are performed in real-world neural network.