Skip to main content

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

Project description

pyNeVer

PyPI - Version PyPI - Python Version


Neural networks Verifier (NeVer 2) is a tool for the design, training and verification of neural networks. It supports sequential fully connected and convolutional neural networks with ReLU and Sigmoid activation functions. pyNeVer is the corresponding python package providing all the main capabilities of NeVer 2 and can be easily installed using pip.

Installation and setup

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

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

To install pyNeVer, just 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.

Supported inputs

At present the pyNeVer package supports only the abstraction and verification of fully connected and convolutional neural networks with ReLU and Sigmoid activation functions. The training 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 package 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

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

All the examples described below are guaranteed to work until Release v0.1.1a4. After this release, changes in the interface structure may add inconsistencies between test scripts and API, so the old examples will be removed and new examples will be created in future releases.

  • 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 Stefano Demarchi, under the supervision of Professors Armando Tacchella and Luca Pulina.
A significant contribution for the participation in VNN-COMP 2024 was the help of Elena Botoeva.

Other contributors:

  • Andrea Gimelli - Bound propagation integration
  • Pedro Henrique Simão Achete - Command-line interface and convolutional linearization
  • Karim Pedemonte - Design and refactoring

Publications

If you use NeVer2 or pyNeVer in your work, please kindly cite our papers. Here you can find the list of BibTeX entries.

@article{demarchi2024never2,
  title={NeVer2: Learning and Verification of Neural Networks},
  author={Demarchi, Stefano and Guidotti, Dario and Pulina, Luca and Tacchella, Armando},
  journal={Soft Computing},
  year={2024}
}

@inproceedings{demarchi2022formal,
  title={Formal Verification Of Neural Networks: A Case Study About Adaptive Cruise Control.},
  author={Demarchi, Stefano and Guidotti, Dario and Pitto, Andrea and Tacchella, Armando},
  booktitle={ECMS},
  pages={310--316},
  year={2022}
}

@inproceedings{guidotti2021pynever,
  title={pynever: A framework for learning and verification of neural networks},
  author={Guidotti, Dario and Pulina, Luca and Tacchella, Armando},
  booktitle={Automated Technology for Verification and Analysis: 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18--22, 2021, Proceedings 19},
  pages={357--363},
  year={2021},
  organization={Springer}
}

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-1.0.0.tar.gz (89.0 kB view details)

Uploaded Source

Built Distribution

pyNeVer-1.0.0-py3-none-any.whl (103.9 kB view details)

Uploaded Python 3

File details

Details for the file pynever-1.0.0.tar.gz.

File metadata

  • Download URL: pynever-1.0.0.tar.gz
  • Upload date:
  • Size: 89.0 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/5.1.1 CPython/3.9.19

File hashes

Hashes for pynever-1.0.0.tar.gz
Algorithm Hash digest
SHA256 3a532064f06601312a1f9c8fc25f17dfb5702ebc252543fa144cee47272e7d33
MD5 f1353436b0cdfd4b990f85542f26683c
BLAKE2b-256 91c1277101b170bd120d6919072fa1aa08152975dff2d525281bc1fc2319963f

See more details on using hashes here.

File details

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

File metadata

  • Download URL: pyNeVer-1.0.0-py3-none-any.whl
  • Upload date:
  • Size: 103.9 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/5.1.1 CPython/3.9.19

File hashes

Hashes for pyNeVer-1.0.0-py3-none-any.whl
Algorithm Hash digest
SHA256 480d935960126b95201f79067ed58fddff61647ff5d417a0006e2be2f8130757
MD5 788b90d2332164084afe139e760ce3b2
BLAKE2b-256 58d536780aab40aa032a6a7fe925f5b021add27d9a7b6c272c0073b9c9327cf1

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