# pyNeVer
[](https://pypi.org/project/pynever)
[](https://pypi.org/project/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_
* _multipledispatch_
To install __pyNeVer__ as an API, run the command:
```bash
pip install pynever
```
To run __pyNeVer__ as a standalone tool you should clone this repository and create a conda environment
```bash
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](https://www.vnnlib.org) specifications on ONNX models we provide two scripts: one for single instances and another one for multiple instances.
To verify a single instance run
```bash
python never2_launcher.py [-o OUTPUT] [-t TIMEOUT] model.onnx property.vnnlib {sslp|ssbp}
```
For multiple instances collected in a CSV file run
```bash
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](https://link.springer.com/article/10.1007/s00500-024-09907-5).
* 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](examples/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](examples/notebooks/00%20-%20Networks.ipynb) covers the classes and methods to build networks
- The [second notebook](examples/notebooks/01%20-%20Training.ipynb) covers the learning strategy to train and test a network
- The [third notebook](examples/notebooks/02%20-%20Safety%20specifications.ipynb) explains how to build a safety specification to define a verification problem
- The [fourth notebook](examples/notebooks/03%20-%20Verification.ipynb) 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](https://easychair.org/publications/paper/Qgdn).
The [conversion](pynever/strategies/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](https://www.vnnlib.org) 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__ - Bounds propagation integration
* __Pedro Henrique Simão Achete__ - Command-line interface and convolutional linearization
* __Karim Pedemonte__ - Design and refactoring
* __Marco Sanfilippo__ - VNN-LIB parser
To contribute to this project, start by looking at the [CONTRIBUTING](CONTRIBUTING.md) 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},
}
```
Raw data
{
"_id": null,
"home_page": null,
"name": "pyNeVer",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.11",
"maintainer_email": "Stefano Demarchi <stefano.demarchi@edu.unige.it>, Andrea Gimelli <andrea.gimelli@edu.unige.it>",
"keywords": "artificial intelligence, formal verification, neural networks",
"author": null,
"author_email": "Dario Guidotti <dguidotti@uniss.it>, Stefano Demarchi <stefano.demarchi@edu.unige.it>",
"download_url": "https://files.pythonhosted.org/packages/2e/85/c585e05a3c8b63ce3ff298c9682437e1e1f112d1b1ad2510dffd90bf1b10/pynever-1.3.0.tar.gz",
"platform": null,
"description": "# pyNeVer\n\n[](https://pypi.org/project/pynever)\n[](https://pypi.org/project/pynever)\n\n-----\n\nNeural networks Verifier (__NeVer 2__) is a tool for the design, training and verification of neural networks.\nIt supports feed-forward and residual neural networks with ReLU and activation functions.\n__pyNeVer__ is the corresponding python package providing all the main capabilities of __NeVer 2__\nand can be easily installed using pip. \n\nInstallation and setup\n----------------------\n\n__pyNeVer__ depends on several packages, which are all available via pip and should be installed automatically. \nThe packages required for the correct execution are the following:\n\n* _numpy_\n* _ortools_\n* _onnx_\n* _torch_\n* _torchvision_\n* _multipledispatch_\n\nTo install __pyNeVer__ as an API, run the command:\n```bash\npip install pynever\n```\n\nTo run __pyNeVer__ as a standalone tool you should clone this repository and create a conda environment\n```bash\ngit clone https://github.com/nevertools/pyNeVer\ncd pyNeVer\n\nconda env create -f environment.yml\nconda activate pynever\n```\n\nCommand-line interface\n----------------------\nTo verify [VNN-LIB](https://www.vnnlib.org) specifications on ONNX models we provide two scripts: one for single instances and another one for multiple instances.\nTo verify a single instance run\n```bash\npython never2_launcher.py [-o OUTPUT] [-t TIMEOUT] model.onnx property.vnnlib {sslp|ssbp}\n```\n\nFor multiple instances collected in a CSV file run\n```bash\npython never2_batch.py [-o OUTPUT] [-t TIMEOUT] instances.csv {sslp|ssbp}\n```\n* The -o option should be used to specify the output CSV file to save results, otherwise it will be generated in the same directory\n* The -t option specifies the timeout for each run\n* sslp and ssbp are the two algorithms employed by _NeVer2_:\n * SSLP (Star-set with Linear Programming) is our first algorithm based on star sets presented in [this paper](https://link.springer.com/article/10.1007/s00500-024-09907-5).\n * 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.\n\nAPI\n---------------------\nIn the [notebooks](examples/notebooks) directory there are four Jupyter Notebooks that illustrate how to use _pyNever_ as an API to design, train and verify neural networks.\n\n- The [first notebook](examples/notebooks/00%20-%20Networks.ipynb) covers the classes and methods to build networks\n- The [second notebook](examples/notebooks/01%20-%20Training.ipynb) covers the learning strategy to train and test a network\n- The [third notebook](examples/notebooks/02%20-%20Safety%20specifications.ipynb) explains how to build a safety specification to define a verification problem\n- The [fourth notebook](examples/notebooks/03%20-%20Verification.ipynb) explains our verification algorithms and covers how to instantiate and execute verification\n\nSupported layers\n----------------------\n\nAt present the __pyNeVer__ package supports abstraction and verification of fully connected and convolutional \nneural networks with ReLU activation functions.\n\nTraining and conversion support all the layers supported by [VNN-LIB](https://easychair.org/publications/paper/Qgdn).\n\nThe [conversion](pynever/strategies/conversion) package provides the capabilities for the conversion of PyTorch and ONNX\nnetworks: therefore this kind of networks can be loaded using the respective frameworks and then converted to the\ninternal representation used by __pyNeVer__. \n\nThe properties for the verification and abstraction of the networks must be defined either in python code following\nthe specification which can be found in the documentation, or via an SMT-LIB file compliant to the \n[VNN-LIB](https://www.vnnlib.org) standard.\n\nContributors\n----------------------\n\nThe main contributors of pyNeVer are __Dario Guidotti__ and __Stefano Demarchi__, under the supervision of Professors\n__Armando Tacchella__ and __Luca Pulina__. \nA significant contribution for the participation in VNN-COMP 2024 was\nthe help of __Elena Botoeva__.\n\n_Other contributors_:\n\n* __Andrea Gimelli__ - Bounds propagation integration\n* __Pedro Henrique Sim\u00e3o Achete__ - Command-line interface and convolutional linearization\n* __Karim Pedemonte__ - Design and refactoring\n* __Marco Sanfilippo__ - VNN-LIB parser\n\nTo contribute to this project, start by looking at the [CONTRIBUTING](CONTRIBUTING.md) file!\n\nPublications\n----------------------\n\nIf you use __NeVer2__ or __pyNeVer__ in your work, **please kindly cite our papers**. Here you can find \nthe list of BibTeX entries.\n\n```\n@article{demarchi2024never2,\n\tauthor = {Demarchi, S. and Guidotti, D. and Pulina, L. and Tacchella, A.},\n\tjournal = {Soft Computing},\n\tnumber = {19},\n\tpages = {11647-11665},\n\ttitle = {{NeVer2}: learning and verification of neural networks},\n\tvolume = {28},\n\tyear = {2024}\n}\n\n@inproceedings{demarchi2024improving,\n\tauthor = {Demarchi, S. and Gimelli, A. and Tacchella, A.},\n\tbooktitle = {{ECMS} International Conference on Modelling and Simulation},\n\ttitle = {Improving Abstract Propagation for Verification of Neural Networks},\n\tyear = {2024}\n}\n\n@inproceedings{demarchi2022formal,\n\tauthor = {Demarchi, S. and Guidotti, D. and Pitto, A. and Tacchella, A.},\n\tbooktitle = {{ECMS} International Conference on Modelling and Simulation},\n\ttitle = {Formal Verification of Neural Networks: {A} Case Study About Adaptive Cruise Control},\n\tyear = {2022}\n}\n\n@inproceedings{guidotti2021pynever,\n author={Guidotti, D. and Pulina, L. and Tacchella, A.},\n booktitle={International Symposium on Automated Technology for Verification and Analysis},\n title={pynever: A framework for learning and verification of neural networks},\n year={2021},\n}\n```\n",
"bugtrack_url": null,
"license": null,
"summary": "API for the design, training and verification of neural networks.",
"version": "1.3.0",
"project_urls": {
"Documentation": "https://neuralverification.org/pynever",
"Homepage": "https://neuralverification.org",
"Issues": "https://github.com/nevertools/pynever/issues",
"Repository": "https://github.com/nevertools/pynever.git"
},
"split_keywords": [
"artificial intelligence",
" formal verification",
" neural networks"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "c734e76904ae561f2c150a2665313d4106efc70a5f1ca6ceaa027dcc7e0ee48a",
"md5": "c5f555a2fbf583d0a37c4b080a99f059",
"sha256": "2d80ac8e6b6aa42de8c494692eb2d94c3754c4d7263ef93195a2783eec18b275"
},
"downloads": -1,
"filename": "pynever-1.3.0-py3-none-any.whl",
"has_sig": false,
"md5_digest": "c5f555a2fbf583d0a37c4b080a99f059",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.11",
"size": 1107340,
"upload_time": "2025-07-22T11:48:33",
"upload_time_iso_8601": "2025-07-22T11:48:33.600811Z",
"url": "https://files.pythonhosted.org/packages/c7/34/e76904ae561f2c150a2665313d4106efc70a5f1ca6ceaa027dcc7e0ee48a/pynever-1.3.0-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "2e85c585e05a3c8b63ce3ff298c9682437e1e1f112d1b1ad2510dffd90bf1b10",
"md5": "62fa0a7521c7f9a40f1d772d51a7884f",
"sha256": "53fa64a3b510b97b71d52502b5c2c40a675a196e0cd0902418fa7f51100828d8"
},
"downloads": -1,
"filename": "pynever-1.3.0.tar.gz",
"has_sig": false,
"md5_digest": "62fa0a7521c7f9a40f1d772d51a7884f",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.11",
"size": 1220943,
"upload_time": "2025-07-22T11:48:34",
"upload_time_iso_8601": "2025-07-22T11:48:34.771402Z",
"url": "https://files.pythonhosted.org/packages/2e/85/c585e05a3c8b63ce3ff298c9682437e1e1f112d1b1ad2510dffd90bf1b10/pynever-1.3.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-07-22 11:48:34",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "nevertools",
"github_project": "pynever",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"lcname": "pynever"
}
JSON
