Networks

Networks are a key component to DNNP specifications. Without a network, there is no DNN verification problem. As such, DNNP provides several ways to facilitate working with networks within property specifications. This includes network inference, slicing, and composition. We explain each of these in more detail below.

These operations on Network objects enable DNNP specifications to be specified over production models, rather than models designed specifically for a given specification. DNNP allows models to be used, reduced, or combined to capture the exact semantics of the desired property without having to customize the network model for the specification being written.

Network Inference

First, and probably most importantly, is that networks can perform inference on inputs. Inference occurs when a network is applied to an input using the python call syntax, i.e., N(x). Inference can be either concrete or symbolic.

Concrete inference occurs when the inputs to the network are concrete values. This occurs when the exact value of the input is known at runtime, such as when it is explicitly defined in the specification (e.g., x = np.array([[0.0, 1.0, -1.0]])), or parameterized at runtime (e.g., x = np.load(Parameter("inputpath", str))). In this case, inference will compute the concrete output value for the given input.

Symbolic inference occurs when the input is non-concrete. Currently, DNNV only supports symbolic inference when the input is a Symbol object. Instances of symbolic inference are extracted during the property reduction process and translated to appropriate constraints for the specified verifier.

Network Slicing

In DNNP and DNNV, networks are represented as computation graphs, where nodes in the graph are operations and directed edges between nodes represent the data flow between operations. Some of these operations are Inputs, and others are tagged as outputs. DNNP introduces the concept of network slicing, which allows us to select a subgraph of the original network graph. Slicing enables verification at any point in the network, while using the same full network model as input to DNNV. For example, in a six layer network, we could define a property over the output of the third layer, such as some of the properties in Property Inference for Deep Neural Networks by Gopinath et al.

In DNNP, network slicing looks like N[start:end, output_index]. The second axis, output_index is optional, and can be used when a network has multiple tagged output operations to select a single operation as the output. This is not a common use case, and so in many cases, slicing will more resemble N[start:end]. Slicing will take all operations that are at least start positions from an Input operation (i.e., there is a path with at least start-1 operations between the operation and an Input) and at most end-1 positions from an Input, if both start and end are positive. A negative index will count backwards from the network outputs, rather than forwards from the inputs. A negative start value will select operations that are at most -start positions from an output operation (i.e., there is a path with at most -start-1 operations between the operation and an output), while a negative end value will select operations at least -end operations from an output. If start is not specified (e.g., N[:end]), then slicing will start from the input operations (i.e., N[0:end]). If end is not specified (e.g., N[start:]), then slicing will select the operations from the start index to the current output operations of the network.

Network Composition

Another potentially useful technique when specifying properties is network composition. This enables networks to be stacked such that the input to one model is the output of another. The following code composes the networks Ni and No into N, such that inference with N is equivalent to inference with Ni followed by the inference with No:

Ni = Network("Ni")
No = Network("Ni")
N = No.compose(Ni)

Forall(x, N(x) > 0)

One use case for composition is the use of generative models as input constraints to restrict inputs to a learned model of the input space, as introduced by Toledo et al.