Formal Verification of Neural Networks
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.
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.onnx on 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/nn on GitHub.
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/neurNetContrSys on GitHub.