IGNNV (Information-Guided Neural Network Verifier) (in development)

This MATLAB tool (in development) provides reachability-analysis-based verification for neural networks. The verification process is under the guidance of available information, e.g., specifications, simulations, etc, in order to enhance scalability.

Related tools and software

The model-based reachability analysis for plants is based on The COntinuous Reachability Analyzer ([CORA] https://tumcps.github.io/CORA/)

Installation:

1. Install MATLAB.
2. Clone or download IGNNV from (https://github.com/xiangweiming/ignnv).
3. Run examples.

Features

1. This tool use specification-guided method to significantly enhance the scalability in safety verification.

Specification-guided partition for input space.

Specification-guided output set estimation.

Specification-guided verification for image recogination. It can verify that the neural networ is safe under any 3*3 attack at the left-above corner

2. This tool can do backward computation guided by specification for falsification.

Specification-guided falsification. Red area is the unsafe input set.

3. This tool use simulation-guided method to significantly enhance the scalability in reachable set computation.

Learning forward kinematics of a robotic arm model with two joints.

Uniform partition method generates 16384 intervals.

Simulation-guided partition method generates only 397 intervals.

Simulation-guided partition of input space.

4. This tool can compute the reachable set of learning-enabled control systems.

Adaptive cruise control system.

Reachable set computation adaptive cruise control system.

Reachablilty-based safety verification for adaptive cruise control system.

Magnetic levitation (Maglev) model.

Reachablilty-based safety verification for Maglev model.

Publications