Skip to main content

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

Project description

pyNeVer

Neural networks Verifier (NeVer 2) 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 2 tool and can be easily installed using pip. The PyPI project page can be found at https://pypi.org/project/pyNeVer/ whereas the github repository can be found at https://github.com/NeVerTools/pyNeVer.

REQUIREMENTS AND INSTALLATION

pyNeVer depends on several packages, which should be installed automatically. The packages required for the correct execution are the following:

  • numpy
  • ortools
  • onnx
  • torch
  • torchvision
  • pysmt

All the above packages are available via pip.

To install pyNeVer, run the command:

pip install pynever

To run some examples, further packages may be required. If an example requires a specific package, it will be detailed in the example directory.

DOCUMENTATION

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

SUPPORTED INPUTS

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 utilities.py module.
The conversion.py provides the capabilities for the conversion of PyTorch and ONNX networks: therefore this kind of networks can be loaded using the respective frameworks and then converted to the internal representation used by pyNeVer. The properties for the verification and abstraction of the networks must be defined either in python code following the specification which can be found in the documentation, or via an SMT-LIB file compliant to the VNN-LIB standard. Examples of the python specification of the properties can be found in all the scripts in the directory examples/submissions/ATVA2021/.

EXAMPLES

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 pruning_example.py 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 acas_experiment.py from within the ATVA2021/ directory. The log files will be generated and will be saved in the logs/ directory.

CONTRIBUTORS

The main contributors of pyNeVer are Dario Guidotti and Armando Tacchella, further contributions are provided by Stefano Demarchi.

Students contributions:

  • Alessandro Drago - TensorFlow conversion

Project details


Download files

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

Source Distribution

pyNeVer-0.1.1.tar.gz (54.7 kB view details)

Uploaded Source

Built Distribution

pyNeVer-0.1.1-py3-none-any.whl (60.1 kB view details)

Uploaded Python 3

File details

Details for the file pyNeVer-0.1.1.tar.gz.

File metadata

  • Download URL: pyNeVer-0.1.1.tar.gz
  • Upload date:
  • Size: 54.7 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/4.0.2 CPython/3.9.18

File hashes

Hashes for pyNeVer-0.1.1.tar.gz
Algorithm Hash digest
SHA256 617bbd5a0d40e4d65048eef2760c30680ba41854f2d45ab9cb9c1d28cd488e60
MD5 f4db4bc08f013d7fa41336ee38b97c84
BLAKE2b-256 4ca8cb18e39a79295cd59b769d516fc01ca9de208171b855565bff622a1e8337

See more details on using hashes here.

File details

Details for the file pyNeVer-0.1.1-py3-none-any.whl.

File metadata

  • Download URL: pyNeVer-0.1.1-py3-none-any.whl
  • Upload date:
  • Size: 60.1 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/4.0.2 CPython/3.9.18

File hashes

Hashes for pyNeVer-0.1.1-py3-none-any.whl
Algorithm Hash digest
SHA256 12a42f95d3d8ae8d827cbf0cefc95938a2d9d310c02df27b5dbdea8596c8dc54
MD5 1e77b12c3bb57a33d760b87d4f81f068
BLAKE2b-256 fa33c20ad940d4222a21168daadb087879c85912f37776dc4ca184a5fd4e9bfa

See more details on using hashes here.

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page