Skip to main content

Package for the training, pruning and verification of neural networks.

Project description


Neural networks Verifier (NeVer) is a tool for the training, pruning and verification of neural networks. At present it supports sequential fully connected neural networks with ReLU and Sigmoid activation functions. pyNeVer is the corresponding python package providing all the main capabilities of the NeVer tool and can be easily installed using pip. The PyPI project page can be found at whereas the github repository can be found at


Given the characteristcs of PyTorch and ONNX we were not able to setup an auto-installation for these packages. Therefore the user is required to install the torch, torchvision and onnx packages indipendently. Guides on how to install such packages can be found at:

After the installation of the required packages pyNeVer can be installed using the command:

  • pip install pynever


The documentation related to the pyNeVer package can be found in the directory docs/pynever/ as html files.


At present the pyNeVer package supports only the abstraction and verification of fully connected neural networks with ReLU and Sigmoid activation functions. The training, pruning and conversion supports also batch normalization layers. A network with batchnorm layers following fully connected layers can be converted to a "pure" fully connected neural networks using the capabilities provided in the module.
The provides the capabilities for the conversion of PyTorch and ONNX networks: therefore these kind of networks can be loaded using the respective frameworks and then converted to the internal representation used by pyNeVer. At present the properties for the verification and abstraction of the networks must be defined in python code following the specification which can be found in the documentation. Examples of the specification of the properties can be found in all the scripts in the directory examples/submissions/ATVA2021/.


NB: All the scripts should be executed INSIDE the related directory!

  • The directory examples/ contains some examples of application of the pyNeVer package. In particular the jupyter notebook shows a graphical example of the application of the abstraction module for the reachability of a small network with bi-dimensional input and outputs.

  • The script show how to train and prune some small fully connected neural networks with relu activation function. It also show how it is possible to combine batch norm layer and fully connected layers to make the networks compliant with the requirements of the verification and abstraction modules.

  • The directory examples/submissions/ATVA2021 contains the experimental setup used for the experimental evaluation in our ATVA2021 paper. The experiments can be easily replicated by executing the python scripts from within the ATVA2021/ directory. The log files will be generated and will be saved in the logs/ directory.

Project details

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Files for pyNeVer, version 0.0.1a7
Filename, size File type Python version Upload date Hashes
Filename, size pyNeVer-0.0.1a7.tar.gz (46.7 kB) File type Source Python version None Upload date Hashes View

Supported by

AWS AWS Cloud computing Datadog Datadog Monitoring DigiCert DigiCert EV certificate Facebook / Instagram Facebook / Instagram PSF Sponsor Fastly Fastly CDN Google Google Object Storage and Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Salesforce Salesforce PSF Sponsor Sentry Sentry Error logging StatusPage StatusPage Status page