pyNeVer 1.2.6

API for the design, training and verification of neural networks.

pyNeVer

---

Neural networks Verifier (NeVer 2) is a tool for the design, training and verification of neural networks. It supports feed-forward and residual neural networks with ReLU and 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 as an API, run the command:

pip install pynever

To run pyNeVer as a standalone tool you should clone this repository and create a conda environment

git clone https://github.com/nevertools/pyNeVer
cd pyNeVer

conda env create -f environment.yml
conda activate pynever

Command-line interface

To verify VNN-LIB specifications on ONNX models we provide two scripts: one for single instances and another one for multiple instances. To verify a single instance run

python never2_launcher.py [-o OUTPUT] [-t TIMEOUT] model.onnx property.vnnlib {sslp|ssbp}

For multiple instances collected in a CSV file run

python never2_batch.py [-o OUTPUT] [-t TIMEOUT] instances.csv {sslp|ssbp}

• The -o option should be used to specify the output CSV file to save results, otherwise it will be generated in the same directory
• The -t option specifies the timeout for each run
• sslp and ssbp are the two algorithms employed by NeVer2:
  • SSLP (Star-set with Linear Programming) is our first algorithm based on star sets presented in this paper.
  • SSBP (Star-set with Bounds Propagation) enhances SSLP with an abstraction-refinement search and symbolic interval propagation. This is the algorithm used in VNNCOMP 2024.

API

In the notebooks directory there are four Jupyter Notebooks that illustrate how to use pyNever as an API to design, train and verify neural networks.

• The first notebook covers the classes and methods to build networks
• The second notebook covers the learning strategy to train and test a network
• The third notebook explains how to build a safety specification to define a verification problem
• The fourth notebook explains our verification algorithms and covers how to instantiate and execute verification

Supported layers

At present the pyNeVer package supports abstraction and verification of fully connected and convolutional neural networks with ReLU activation functions.

Training and conversion support all the layers supported by VNN-LIB.

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.

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

To contribute to this project, start by looking at the CONTRIBUTING file!

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,
	author = {Demarchi, S. and Guidotti, D. and Pulina, L. and Tacchella, A.},
	journal = {Soft Computing},
	number = {19},
	pages = {11647-11665},
	title = {{NeVer2}: learning and verification of neural networks},
	volume = {28},
	year = {2024}
}

@inproceedings{demarchi2024improving,
	author = {Demarchi, S. and Gimelli, A. and Tacchella, A.},
	booktitle = {{ECMS} International Conference on Modelling and Simulation},
	title = {Improving Abstract Propagation for Verification of Neural Networks},
	year = {2024}
}

@inproceedings{demarchi2022formal,
	author = {Demarchi, S. and Guidotti, D. and Pitto, A. and Tacchella, A.},
	booktitle = {{ECMS} International Conference on Modelling and Simulation},
	title = {Formal Verification of Neural Networks: {A} Case Study About Adaptive Cruise Control},
	year = {2022}
}

@inproceedings{guidotti2021pynever,
    author={Guidotti, D. and Pulina, L. and Tacchella, A.},
    booktitle={International Symposium on Automated Technology for Verification and Analysis},
    title={pynever: A framework for learning and verification of neural networks},
    year={2021},
}