This page lists our software packages for the verification of systems using neural networks.
Neural System Verify is a software package for performing reachability analysis on neural agent-environment systems implemented by ReLU feed-forward neural networks. Further information can be found in the corresponding paper (published at KR 2018).
Recurrent Neural System Verify is an extension of NSVerify to handle recurrent neural networks. Further information can be found in the corresponding paper (published at AAAI 2019).
VeriNet is a symbolic interval propagation based verification algorithm for feed-forward neural networks. Further information can be found in the paper (To appear at ECAI20).
VErification of NeUral Systems is a state-of-the-art sound and complete verification toolkit for ReLU-based feed-forward neural networks. It can be used to check reachability and local adversarial robustness properties. VENUS implements a MILP-based verification method whereby it leverages dependency relations between the ReLU nodes to prune the search tree that needs to be considered during branch-and-bound. It additionally implements methods based on symbolic interval propagation and input domain splitting. Further information can be found in the corresponding paper (published at AAAI 2020).
Neural Agent operating on a Non-deterministic Environment System Verify is a software package for performing MILP-based verification for agent-environment systems where the agent is controlled by ReLU-activated feed-forward neural networks, the environment is non-deterministic with branching temporal evolutions, and specifications are expressed in a bounded variant of CTL.