Neural Network Verification and Robust Training
CORA enables the formal verification of neural networks, both in open-loop and in closed-loop scenarios. Open-loop verification refers to the task where properties of the output set of a neural network are verified, e.g., correctly classified images given noisy input. In closed-loop scenarios, the neural network is used as a controller of a dynamic system and is neatly integrated in the reachability algorithms above, e.g., controlling a car while keeping a safe distance. Additionally, one can train verifiably robust neural networks in CORA.
Note: Neural networks require additional toolboxes to be installed, especially for importing them into CORA. Please check Section 1.3 in the CORA manual.
-
Open-Loop Verification
Open-loop verification refers to the task where properties of the output set of a neural network are verified, e.g. correctly classified images given noisy input. The neural network can be imported into CORA from various common neural network formats. CORA currently supports ONNX, NNet, YML, Sherlock, and the conversion for neural networks coming from the Deep Learning Toolbox. The code below shows an exemplary verification of a noisy MNIST image. The neural network file can be found at
./models/Cora/nn/mnist_sigmoid_6_200.onnxon GitHub.More information on open-loop verification using CORA can be found in Section 6 in the CORA manual.
Further examples can be found at
./examples/nnon GitHub.The verification algorithm conservatively propagates the input set through all layers and checks if the obtained output set with the given specifications. A visualization of this process is shown below: -
Closed-Loop Verification
In closed-loop scenarios, the neural network is used as controller of a dynamic system and is neatly integrated in the reachability algorithms of CORA. The code below considers a unicycle model of a car with the x and y coordinates on a two-dimensional plane, the velocity magnitude (speed), and steering angle as state variables. The specification is to steer the car into a given goal region.
More information on closed-loop verification using CORA can be found in Section 4.2.9 in the CORA manual.
Further examples can be found at
./examples/contDynamics/neurNetContrSyson GitHub. -
Robust Training
CORA also enables the training of verifiably robust neural networks both in the supervised and in the reinforcement learning setting. This is realized by integrating reachability analysis into the training process. In particular, we propagate zonotopes through a neural network and compute a set-based gradient based on the computed output set, target, and loss function. This is done efficiently in CORA by propagating the sets batch-wise through the network and every computation can be done on a GPU.
Supervised Setting:The training process in the supervised setting is visualized below:Reinforcement Learning:Robust training results in verifiably robust controllers. A comparison is visualized below:More information on closed-loop verification using CORA can be found in Section 6 in the CORA manual.