PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier

Neural Networks (NNs) have increasingly apparent safety implications commensurate with their proliferation in real-world applications: both unanticipated as well as adversarial misclassifications can result in fatal outcomes. As a consequence, techniques of formal verification have been recognized as crucial to the design and deployment of safe NNs. In this paper, we introduce a new approach to formally verify the most commonly considered safety specifications for ReLU NNs – i.e. polytopic specifications on the input and output of the network. Like some other approaches, ours uses a relaxed convex program to mitigate the combinatorial complexity of the problem. However, unique in our approach is the way we use a convex solver not only as a linear feasibility checker, but also as a means of penalizing the amount of relaxation allowed in solutions. In particular, we encode each ReLU by means of the usual linear constraints, and combine this with a convex objective function that penalizes the discrepancy between the output of each neuron and its relaxation. This convex function is further structured to force the largest relaxations to appear closest to the input layer; this provides the further benefit that the most “problematic” neurons are conditioned as early as possible, when conditioning layer by layer. This paradigm can be leveraged to create a verification algorithm that is not only faster in general than competing approaches, but is also able to verify considerably more safety properties; we evaluated PEREGRiNN on a standard MNIST robustness verification suite to substantiate these claims.

Semi-formal verification of closed-loop specifications in the concept design phase

The article addresses the semi-formal verification of behavioral specifications for subsystems consisting of physical parts and controllers, complemented by simulation-based integration testing. Since design errors in early phases tend to be particularly expensive, the method is tailored towards applicability in these phases. We verify behavioral specifications with proof-like credibility, or falsify them while providing a violation scenario that is reusable as a test case. The system is represented as a mixed logical dynamical (MLD) system, and specifications are expressed by a temporal logic with affine signal abstractions. The verification problem is converted into an equivalent mixed-integer linear feasibility problem solved using off-the-shelf solvers. An example illustrates the effectiveness of the method.