dnnv

A Framework for Deep Neural Network Verification

https://github.com/dlshriver/dnnv

Science Score: 64.0%

This score indicates how likely this project is to be science-related based on various indicators:

✓
CITATION.cff file
Found CITATION.cff file
✓
codemeta.json file
Found codemeta.json file
✓
.zenodo.json file
Found .zenodo.json file
○
DOI references
✓
Academic publication links
Links to: arxiv.org
✓
Committers with academic emails
1 of 8 committers (12.5%) from academic institutions
○
Institutional organization owner
○
JOSS paper metadata
○
Scientific vocabulary similarity
Low similarity (14.3%) to scientific vocabulary

Keywords

deep-neural-networks dnnv framework machine-learning neural-networks verification

Last synced: 4 months ago · JSON representation ·

Repository

A Framework for Deep Neural Network Verification

Basic Info

Host: GitHub
Owner: dlshriver
License: mit
Language: Python
Default Branch: main
Homepage: https://docs.dnnv.org
Size: 11.8 MB

Statistics

Stars: 56
Watchers: 5
Forks: 19
Open Issues: 9
Releases: 13

Topics

deep-neural-networks dnnv framework machine-learning neural-networks verification

Created about 6 years ago · Last pushed about 1 year ago

Metadata Files

Readme Contributing License Code of conduct Citation

Deep Neural Network Verification

A framework for verification and analysis of deep neural networks. You can read an overview of DNNV in our CAV 2021 paper DNNV: A Framework for Deep Neural Network Verification, or watch our presentation on YouTube.

Getting Started

For detailed instructions on installing and using DNNV, see our documentation.

Installation

DNNV requires python >=3.7,<3.10, and has been tested on linux. To install the latest stable version run:

bash $ pip install dnnv

bash $ pip install git+https://github.com/dlshriver/DNNV.git@main

We recommend installing DNNV into a python virtual environment.

Install any of the supported verifiers (Reluplex, planet, MIPVerify.jl, Neurify, ERAN, BaB, marabou, nnenum, verinet):

bash $ dnnv_manage install reluplex planet mipverify neurify eran bab marabou nnenum verinet

Several verifiers make use of the Gurobi solver. This should be installed automatically, but requires a license to be manually activated and available on the host machine. Academic licenses can be obtained for free from the Gurobi website.

After installing a verifier that requires Gurobi, the grbgetkey command can be found at .venv/opt/gurobi912/linux64/bin/grbgetkey.

Source Installation

First create and activate a python virtual environment.

bash $ python -m venv .venv $ . .venv/bin/activate

Then run the following commands to clone DNNV and install it into the virtual environment:

bash $ git clone https://github.com/dlshriver/DNNV.git $ cd DNNV $ pip install .

Verifiers can then be installed using the dnnv_manage tool as described above.

Make sure that the project environment is activated when using dnnv or the dnnv_manage tools.

Docker Installation

We provide a docker image with DNNV and all non-Gurobi dependent verifiers. To obtain and use the latest pre-built image of the main branch, run:

bash $ docker pull dlshriver/dnnv:latest $ docker run --rm -it dlshriver/dnnv:latest (.venv) dnnv@hostname:~$ dnnv -h

The latest version of the develop branch is available as dlshriver/dnnv:develop, and tagged releases are available as dlshriver/dnnv:vX.X.X where vX.X.X is the desired version number.

The docker image can also be built using the provided Dockerfile. The provided build file will install DNNV with all of the verifiers that do not require Gurobi. To build and run the docker image, run:

bash $ docker build . -t dlshriver/dnnv $ docker run --rm -it dlshriver/dnnv (.venv) dnnv@hostname:~$ dnnv -h

Usage

Properties are specified in our Python-embedded DSL, DNNP. A property specification can import python modules, and define variables. The only required component is the property expression, which must appear at the end of the file. An example of a local robustness property is shown below.

```python from dnnv.properties import *

N = Network("N") x = Image("path/to/image") epsilon = Parameter("epsilon", float, default=1.0)

Forall( x, Implies( ((x - epsilon) < x < (x + epsilon)), argmax(N(x_)) == argmax(N(x))), ), ) ```

To check whether property holds for some network using the ERAN verifier, run:

bash $ dnnv property.dnnp --network N network.onnx --eran

Additionally, if the property defines parameters, using the Parameter keyword, they can be specified on the command line using the option --prop.PARAMETER_NAME, where PARAMETER_NAME is the name of the parameter. For the property defined above, a value for epsilon can be provided with a command line option as follows:

bash $ dnnv property.dnnp --network N network.onnx --eran --prop.epsilon=2.0

To save any counter-example found by the verifier, use the option --save-violation /path/to/array.npy when running DNNV. This will save any violation found as a numpy array at the path specified, which is useful for viewing counter-examples to properties and enables additional debugging and analysis later.

Example Problems

We have made several DNN verification benchmarks available in DNNP+ONNX format in dlshriver/dnnv-benchmarks. This repo includes the ACAS Xu benchmark, ready to run with DNNV!

Acknowledgements

This material is based in part upon work supported by the National Science Foundation under grant number 1900676 and 2019239.

Owner

Name: David Shriver
Login: dlshriver
Kind: user
Location: Pittsburgh, PA

Website: dlshriver.com
Repositories: 6
Profile: https://github.com/dlshriver

Citation (CITATION.cff)

cff-version: 1.2.0
message: "If you use this software, please cite it as below."
authors:
- family-names: "Shriver"
  given-names: "David"
  orcid: "https://orcid.org/0000-0003-0208-6517"
  website: "https://davidshriver.me"
title: "DNNV"
version: 0.6.0
doi: 10.5281/zenodo.4699410
date-released: 2022-08-02
url: "https://github.com/dlshriver/dnnv"
preferred-citation:
  type: conference-paper
  authors:
  - family-names: "Shriver"
    given-names: "David"
    orcid: "https://orcid.org/0000-0003-0208-6517"
    website: "https://davidshriver.me"
  - family-names: "Elbaum"
    given-names: "Sebastian"
    orcid: "https://orcid.org/0000-0001-9592-1352"
  - family-names: "Dwyer"
    given-names: "Matthew"
    orcid: "https://orcid.org/0000-0002-1937-1544"
  doi: "10.1007/978-3-030-81685-8_6"
  title: "DNNV: A Framework for Deep Neural Network Verification"
  conference:
    name: "Computer Aided Verification"
  collection-title: "Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I"
  editors:
  - family-names: "Silva"
    given-names: "Alexandra"
  - family-names: "Leino"
    given-names: "K. Rustan M."
  publisher: "Springer International Publishing"
  volume: 12759
  start: 137 # First page number
  end: 150 # Last page number
  month: 7
  year: 2021

GitHub Events

Total

Issues event: 1
Create event: 1

Last Year

Issues event: 1
Create event: 1

Committers

Last synced: almost 3 years ago

All Time

Total Commits: 321
Total Committers: 8
Avg Commits per committer: 40.125
Development Distribution Score (DDS): 0.218

Top Committers

Name	Email	Commits
David Shriver	d**c@v**u	251
David Shriver	d**r@o**m	50
Felipe Toledo	f**5@g**m	6
dependabot[bot]	4**]@u**m	4
Samuel Teuber	s**l@s**g	4
David Shriver	d**r@c**t	3
Joe Scott	3**t@u**m	2
Meriel Stein	m**n@g**m	1

Committer Domains (Top 20 + Academic)

cox.net: 1 samweb.org: 1 virginia.edu: 1

Issues and Pull Requests

Last synced: 4 months ago

All Time

Total issues: 31
Total pull requests: 76
Average time to close issues: 27 days
Average time to close pull requests: 4 days
Total issue authors: 22
Total pull request authors: 8
Average comments per issue: 3.35
Average comments per pull request: 0.63
Merged pull requests: 73
Bot issues: 0
Bot pull requests: 2

Past Year

Issues: 1
Pull requests: 0
Average time to close issues: N/A
Average time to close pull requests: N/A
Issue authors: 1
Pull request authors: 0
Average comments per issue: 0.0
Average comments per pull request: 0
Merged pull requests: 0
Bot issues: 0
Bot pull requests: 0

View more stats

Top Authors

Issue Authors

GuantingPan (3)
cherrywoods (3)
MaxSally (3)
khedher1984 (2)
urays (2)
AWbosman (2)
ChristopherBrix (1)
dlshriver (1)
MarcelBulpr (1)
nathzi1505 (1)
mhmd97z (1)
preritt (1)
samysweb (1)
j29scott (1)
pat676 (1)

Pull Request Authors

dlshriver (61)
Felipetoledo4815 (5)
dependabot[bot] (2)
j29scott (2)
MarcelBulpr (2)
takluyver (2)
samysweb (2)
MissMeriel (1)

Top Labels

Issue Labels

bug (6) question (1)

Pull Request Labels

enhancement (13) bug (11) dependencies (3) documentation (1)

Packages

Total packages: 1
Total downloads:
- pypi 289 last-month

Total dependent packages: 0
Total dependent repositories: 3
Total versions: 22
Total maintainers: 1

pypi.org: dnnv

dnnv - deep neural network verification

Documentation: https://dnnv.readthedocs.io/en/latest/
License: MIT License
Latest release: 0.6.0
published over 3 years ago

Versions: 22
Dependent Packages: 0
Dependent Repositories: 3
Downloads: 289 Last month

Rankings

Stargazers count: 8.9%

Dependent repos count: 9.0%

Forks count: 9.1%

Dependent packages count: 10.0%

Average: 10.4%

Downloads: 15.0%

Maintainers (1)

dlshriver

Last synced: 5 months ago

Dependencies

docs/requirements.txt pypi

furo *
sphinx *

requirements.txt pypi

black *
coverage *
furo *
lark *
mypy *
numpy >=1.20,<1.22
onnx >=1.8,<1.11
onnxruntime *
psutil *
pytest *
scikit-image >=0.18,<0.19
scipy *
sphinx *
tensorflow >=2.2,<2.8
torch *
torchvision *

third_party/VeriNet/src/Pipfile pypi

cython *
ipykernel *
llvmlite ==0.32.1
matplotlib *
numba ==0.47.0
numpy *
onnx *
scipy *
torch ==1.4.0
torchvision ==0.5.0
tqdm *

third_party/VeriNet/src/Pipfile.lock pypi

appnope ==0.1.0
backcall ==0.2.0
cycler ==0.10.0
cython ==0.29.21
decorator ==4.4.2
ipykernel ==5.3.2
ipython ==7.16.1
ipython-genutils ==0.2.0
jedi ==0.17.1
jupyter-client ==6.1.5
jupyter-core ==4.6.3
kiwisolver ==1.2.0
llvmlite ==0.32.1
matplotlib ==3.2.2
numba ==0.47.0
numpy ==1.19.0
onnx ==1.7.0
parso ==0.7.0
pexpect ==4.8.0
pickleshare ==0.7.5
pillow ==7.2.0
prompt-toolkit ==3.0.5
protobuf ==3.12.2
ptyprocess ==0.6.0
pygments ==2.6.1
pyparsing ==2.4.7
python-dateutil ==2.8.1
pyzmq ==19.0.1
scipy ==1.5.1
six ==1.15.0
torch ==1.4.0
torchvision ==0.5.0
tornado ==6.0.4
tqdm ==4.47.0
traitlets ==4.3.3
typing-extensions ==3.7.4.2
wcwidth ==0.2.5

.github/workflows/main.yml actions

actions/cache v3 composite
actions/checkout v3 composite
actions/setup-python v3 composite
codecov/codecov-action v3 composite

Dockerfile docker

ubuntu focal build

dnnv

Science Score: 64.0%

Keywords

Repository

Basic Info

Statistics

Topics

Metadata Files

README.md

Deep Neural Network Verification

Getting Started

Installation

Source Installation

Docker Installation

Usage

Example Problems

Acknowledgements

Owner

Citation (CITATION.cff)

GitHub Events

Total

Last Year

Committers

All Time

Top Committers

Committer Domains (Top 20 + Academic)

Issues and Pull Requests

All Time

Past Year

Top Authors

Issue Authors

Pull Request Authors

Top Labels

Issue Labels

Pull Request Labels

Packages

pypi.org: dnnv

Rankings

Maintainers (1)

Dependencies