Neural networks(NNs) have been widely used over the past decade at the core of intelligentsystems from sensing modules to learning-based controllers. They've also been deployed in dierent safety-critical domains including healthcare and transportation. However, recent work has shown that NNs are fragile and can make dangerous mistakes that are either unintentional or adversarial. As a consequence, formal verication of NNs holds the promise of providing safety guarantees on the behaviour of such systems. We focus our work on ReLU networks as it is the most widely used activation function. Exact formal verication of ReLU NNs was proved to be NP-hard due to the combinatorial nature of the problem, therefore all of the current verication methods use some relaxation of the problem. We propose a novel framework for formal verication of ReLU neural networks that can ensure that they satisfy some polytopic specications on the input and the output of the network. Our approach uses a relaxed convex program to mitigate the combinatorial complexity of the problem together with some optimization heuristics to eciently verify the satisfaction of the specication on a given network. We have implemented our algorithm in a toolkit, PeregriNN. To test PeregriNN, we run it on two test benches in dierent domains. First, we achieve SOTA results on verifying the adversarial robustness of dierent networks on the MNIST dataset. Second, we verify the safety of a neural network controlled autonomous robot in a structured environment.

Neural networks (NNs) have become the backbone of intelligent systems, with applications ranging from sensing modules to learning-based controllers. Their deployment in safety-critical domains such as healthcare and transportation underscores their significance. However, the fragility of NNs and their potential for dangerous mistakes, whether unintentional or adversarial, necessitates rigorous checks on their behavior. This thesis delves into the Formal Verification of NNs, a process that can provides formal guarantees on their behavior and ensures the reliability and robustness of these systems.

The cornerstone of this work is a novel algorithm, PeregriNN, that has advanced the Formal Verification of NNs. This algorithm has been used to verify various NN properties such as Adversarial Robustness, safety of autonomous systems, and in demonstrating the fairness of NNs by innovatively formulating the fairness property into a Formal Verification problem. Further, this thesis explores a new type of activation function that simplifies the formal verification process, albeit at the cost of increased training time. This exploration, coupled with a collaborative effort that led to the proposal of a polynomial approximation method for ReLU NNs to formally verify them, provides valuable insights into the balance between verification ease and computational efficiency. These methods offer promising approaches to the formal verification of neural networks, further enhancing the robustness and reliability of these systems. The thesis also extends the application of these theories and algorithms to the safety of autonomous systems with neural network controllers. This practical application underscores the real-world implications of formal verification in ensuring the safety and reliability of autonomous systems.

In summary, this thesis provides a comprehensive understanding of the formal verification of neural networks, underscoring the importance of algorithm development and its real-world applications. The findings from this study contribute significantly to this critical field of study, with implications for the fairness, safety, and robustness of NNs.