Farzaneh Moradkhani

Abstract

Functional architectures of cyber-physical systems, like autonomous cars,increasingly comprise components that are generated by training and machine learning rather than by more traditional engineering approaches. The validation and functional verification of such systems, as necessary in safety-critical application domains, poses various unsolved challenges.

Commonly used computational structures underlying machine-learning, like deep neural networks, lack scalable automatic verification support. Verifying DNNs is a difficult problem. DNNs are large, non-linear, and non-convex, and verifying even simple properties about piecewise linear versions of  them is an NP-complete problem. DNN verification is experimentally beyond the reach of general-purpose tools such as linear programming (LP) solvers or existing satisfiability modulo theories (SMT) solvers, and thus far, dedicated tools have only been able to handle small networks. The difficulty in proving properties about DNNs is caused by the presence of non-linear activation function. A DNN is comprised of a set of layers of nodes, and the value of each node is determined by computing a linear combination of values from nodes in the preceding layer and then applying an activation function to the result. These activation functions can be non-linear and render the problem non-convex.

In my PhD thesis we focus on DNNs with activation functions beyond Rectified Linear Unit (ReLU). We are thus leaving the area of piecewise linear function supported by the majority of SMT solvers and specialized solver for DNNs, like Reluplex. A major part of this project is using the SMT Solver iSAT which aims at solving Boolean combinations of linear and non-linear constraint formulas (including transcendental functions), and therefore is suitable to verify safety properties of DNNs which contain of non-linear transfer functions