A property specification defines the desired behavior of a DNN in a formal language. DNNV uses a custom DSL for writing property specifications, based on the Python programming language, which we call DNNP. In this section we will go over this language in detail and describe how properties can be specified in this DSL. To see some examples of common properties specified in this language, check here).
Because the property DSL extends from Python, it should support execution of arbitrary Python code. However, DNNV is still of a work-in-progress, so some expressions (such as star expressions) are not yet supported by our property parser. We are still working to fully support all Python expressions, but the current version supports the most common use cases, and can handle all of the DNN properties that we have tried.
The general structure of a property specification is as follows:
- A set of python module imports
- A set of variable definitions
- A property formula
Imports have the same syntax as Python import statements, and
they can be used to import arbitrary Python modules and packages.
This allows re-use of datasets or input pre-processing code.
For example, the Python package
numpy can be imported to
load a dataset.
Inputs can then be selected from the dataset, or statistics, such
as the mean data point, can be computed on the fly.
While not necessary for correctness, we recommend importing
dnnv.properties package as
from dnnv.properties import *,
which can enable autocompletion and type hints in many code editors.
After any imports, DNNP allows a sequence of assignments to define
variables that can be used in the final property specification.
i = 0, will define the variable
i to a
value of 0.
These definitions can be used to load data and configuration parameters,
or to alias expressions that may be used in the property formula.
For example, if the
torchvision.datasets package has been imported,
data = datasets.MNIST("/tmp") will define a variable
referencing the MNIST dataset from this package.
Parameter class can be used to declare
parameters that can be specified at run time. For example,
eps = Parameter("epsilon", type=float), will define the variable
eps to have type float and will expect a value to be specified at
run time. This value can be specified to DNNV with the option
Definitions can also assign expressions to variables to be used in the
property specification later.
x_in_unit_hyper_cube = 0 <= x <= 1 can be used to assign
an expression specifying that the variable
x is within the unit hyper cube
to a variable. This could be useful for more complex properties with a lot
of redundant sub expressions.
A network can be defined using the
N = Network("N"), specifies a network with the name N
(which is used at run time to concretize the network with a specific DNN model).
All networks with the same name refer to the same model.
Finally, the last part of the property specification is the property formula itself. It must appear at the end of the property specification. All statements before the property formula must be either import or assignment statements.
The property formula defines the desired behavior of the DNN in a subset of first-order-logic. It can make use of arbitrary Python code, as well as any of the expressions defined before it.
DNNP provides many functions to define expressions.
Forall(symbol, expression) can be used to specify that the
provided expression is valid for all values of the specified symbol.
And(*expression), specifies that all of the expressions
passed as arguments to the function must be valid.
And(expr1, expr2) can be
equivalently specified as
expr1 & expr2.
Or(*expression), specifies that at least one of
the expressions passed as arguments to the function must be valid.
Or(expr1, expr2) can be equivalently specified as
expr1 | expr2.
Implies(expression1, expression2), specifies that
expression1 is true, then
expression2 must also be true.
can be used to get the argmin or argmax value of a network’s output,
In property expressions, networks can be called like functions to get the outputs for the network for a given input. Networks can be applied to symbolic variables (such as universally quantified variables), as well as numpy arrays.
Currently DNNV only supports universally quantified properties over a single network input variable. Support for more complex properties is planned.