Verification

To solve a verification problem pyNeVer can define the specifications to verify and instantiate verification algorithms to try and prove that these specifications hold.

Properties

This module defines neural network verification properties. The most general representation defines a single input property expressed as a linear combination of input variables, while the output property is a list of linear inequalities.

class pynever.strategies.verification.properties.NeverProperty(input_matrix=None, input_bias=None, out_matrix_list=None, out_bias_list=None)[source]

Bases: object

An abstract class used to represent a generic property for a NeuralNetwork.

in_matrix[source]

Matrix of the coefficients for the input constraints.

Type:: torch.Tensor

in_bias[source]

Matrix of the biases for the input constraints.

Type:: torch.Tensor

out_matrix_list[source]

Matrices of the coefficients for the output constraints.

Type:: list[torch.Tensor]

out_bias_list[source]

Matrices of the biases for the output constraints.

Type:: list[torch.Tensor]

get_variables_dict()[source]

This method creates a dictionary with keys ‘Input’ and ‘Output’ which map to the corresponding lists of variables

Returns:: The variables names in a dictionary mapping ‘Input’ and ‘Output’
Return type:: dict[str, list[str]]

to_numeric_bounds()[source]

This method creates a HyperRectangleBounds object from the property specification. If the property is already a hyper rectangle it just initializes the object, otherwise it returns the hyper rectangle approximation of the input property.

Returns:: The hyper rectangle approximation of the input property
Return type:: HyperRectangleBounds

to_star()[source]

This method creates the input star based on the property specification

Returns:: The input star
Return type:: Star

to_smt_file(filepath)[source]

This method builds the SMT-LIB representation of the NeVerProperty, expressing the variables and the matrices as constraints in the corresponding logic

Parameters:: filepath (str) – Path to the SMT-LIB file to create

static create_infix_constraints(variables, coefs)[source]

Procedure to create a list of string infix constraints starting from the coefficients and biases

Parameters:

variables (list[str]) – The list of variable names
coefs (LinearFunctions) – The linear function coefficients

Returns:

The list of infix constraints

Return type:

list[str]

class pynever.strategies.verification.properties.VnnLibProperty(filepath)[source]

Bases: NeverProperty

A class used to represent a VNN-LIB property. It directly loads the property from a .vnnlib file.

class pynever.strategies.verification.properties.LocalRobustnessProperty(sample, epsilon, n_outputs, label, max_output)[source]

Bases: NeverProperty

TODO

sample: torch.Tensor epsilon: float label: str max_output: bool

Algorithms

This module contains the classes used to implement the different verification strategies. Following the strategy pattern, the class VerificationStrategy is the abstract class providing a verify method that requires a neural network and a property. The concrete classes SSLPVerification and SSBPVerification implement the verification strategies based on starsets and symbolic bounds propagation, respectively.

class pynever.strategies.verification.algorithms.VerificationStrategy(parameters)[source]

Bases: ABC

An abstract class used to represent a Verification Strategy.

parameters[source]

Parameters to guide the verification algorithm

Type:: VerificationParameters

logger[source]

Custom logger for the verification package

Type:: Logger

abstractmethod verify(network, prop)[source]

Verify that the neural network of interest satisfies the property given as argument using a verification strategy determined in the concrete children.

Parameters:

network (NeuralNetwork) – The neural network to train.
prop (NeverProperty) – The property which the neural network must satisfy.

Returns:

True is the neural network satisfies the property, False otherwise. If False, also returns a counterexample

Return type:

tuple[bool, torch.Tensor | None]

class pynever.strategies.verification.algorithms.SSLPVerification(params)[source]

Bases: VerificationStrategy

Class used to represent the SSLP (Star Sets with Linear Programming) verification strategy.

counterexample_stars[source]

List of Star objects containing a counterexample

Type:: list[Star]

layers_bounds[source]

Bounds obtained through bounds propagation to support verification

Type:: dict

verify(network, prop)[source]

Entry point for the verification algorithm for a network and a property

Parameters:

network (NeuralNetwork) – The network model in the internal representation
prop (NeverProperty) – The property specification

Returns:

True is the neural network satisfies the property, False otherwise. If False, also returns a counterexample

Return type:

tuple[bool, torch.Tensor | None]

class pynever.strategies.verification.algorithms.SSBPVerification(parameters)[source]

Bases: VerificationStrategy

Class used to represent the SSBP (Star Sets with Bounds Propagation) verification strategy. It uses star propagation with Symbolic Bounds Propagation and an abstraction-refinement loop for better readability, structure and functionality.

network[source]

The neural network to verify

Type:: NeuralNetwork

prop[source]

The property specification

Type:: NeverProperty

init_search(network, prop)[source]

Initialize the search algorithm and compute the starting values for the bounds and the star.

Parameters:

network (NeuralNetwork) – The neural network in use
prop (NeverProperty) – The property specification

Returns:

The starting values for the star and the bounds.

Return type:

tuple[ExtendedStar, HyperRectangleBounds, VerboseBounds]

get_bounds()[source]

This method gets the bounds of the neural network for the given property of interest. The bounds are computed based on a strategy that allows to plug and play different bound propagation algorithms

Returns:: The collection of the bounds computed by the Bounds Manager
Return type:: VerboseBounds

compute_intersection(star, nn_bounds)[source]

This method computes the intersection between a star and the output property using the intersection algorithm specified by the parameters

Parameters:

star (ExtendedStar) – The ExtendedStar object containing the star to intersect
nn_bounds (VerboseBounds) – The bounds obtained through bounds propagation

Returns:

The result of the intersection. If True, a counterexample is returned too.

Return type:

tuple[bool, torch.Tensor]

get_next_target(star, nn_bounds)[source]

This method computes the next refinement target for the verification algorithm based on the strategy specified by the parameters.

Parameters:

star (ExtendedStar) – The ExtendedStar object containing the star to refine
nn_bounds (VerboseBounds) – The bounds obtained through bounds propagation.

Returns:

The next refinement target and the extended star to refine. If no more refinement is needed, None is returned.

Return type:

tuple[RefinementTarget | None, ExtendedStar]

verify(network, prop)[source]

Entry point for the abstraction-refinement search algorithm

Parameters:

network (NeuralNetwork) – The network model in the internal representation
prop (NeverProperty) – The property specification

Returns:

True if the network is safe, False otherwise. If the result is False and the search is complete it also returns a counterexample

Return type:

tuple[bool, torch.Tensor | None]

Parameters

This module contains the classes used to define verification parameters for different strategies. The class VerificationParameters is the abstract class from which derive the concrete classes SSLPVerificationParameters and SSBPVerificationParameters.

class pynever.strategies.verification.parameters.VerificationParameters[source]

Bases: ABC

This class is the abstract base for defining the verification parameters related to a specific verification algorithm

class pynever.strategies.verification.parameters.SSLPVerificationParameters(heuristic='complete', neurons_to_refine=None)[source]

Bases: VerificationParameters

This class defines the parameters for the SSLP verification algorithm.

heuristic[source]

The verification heuristic (complete, mixed or approximate)

Type:: str

neurons_to_refine[source]

The number of neurons to refine in the mixed setting

Type:: int

class pynever.strategies.verification.parameters.SSBPVerificationParameters(heuristic=RefinementStrategy.INPUT_BOUNDS_CHANGE, bounds=BoundsBackend.SYMBOLIC, bounds_direction=BoundsDirection.FORWARDS, intersection=IntersectionStrategy.ADAPTIVE, timeout=60)[source]

Bases: VerificationParameters

This class defines the parameters for the SSBP verification algorithm.

heuristic[source]

The refinement heuristic to apply

Type:: RefinementStrategy

bounds[source]

The bounds backend structure to use

Type:: BoundsBackend

bounds_direction[source]

The direction to compute the bounds

Type:: BoundsDirection

intersection[source]

The intersection strategy to use

Type:: IntersectionStrategy

timeout[source]

The timeout in seconds

Type:: int

Enumerators

This module defines utility enumerators suppoorting the SSBP verification algorithm

class pynever.strategies.verification.ssbp.constants.RefinementTarget(layer_id, neuron_idx)[source]

Bases: object

This class represents the refinement target for the verification.

layer_id[source]

Identifier of the target layer

Type:: str

neuron_idx[source]

Index of the target neuron

Type:: int

to_pair()[source]

Procedure to convert the object to a tuple

Returns:: A tuple representation of the object
Return type:: tuple[str, int]

class pynever.strategies.verification.ssbp.constants.NeuronSplit(value)[source]

Bases: Enum

This class is used as an enumerator to distinguish the two outputs of a neuron split (positive or negative)

class pynever.strategies.verification.ssbp.constants.BoundsDirection(value)[source]

Bases: Enum

This class is used as an enumerator to choose the direction of the bounds computation (forwards or backwards)

class pynever.strategies.verification.ssbp.constants.BoundsBackend(value)[source]

Bases: Enum

This class is used as an enumerator to represent different bounds propagation strategies.

symbolic bounds propagation from the Venus2 verifier

class pynever.strategies.verification.ssbp.constants.RefinementStrategy(value)[source]

Bases: Enum

This class is used as an enumerator to represent different refinement strategies.

sequential refinement refines each neuron in the order they appear in the network
lowest approx selects the neuron that contributes with the lowest approximation
lowest approx - current layer selects the neuron that contributes with the lowest approximation in the layer
input bounds change selects the neuron that contributes most to change the input bounds when refined

class pynever.strategies.verification.ssbp.constants.IntersectionStrategy(value)[source]

Bases: Enum

This class is used as an enumerator to represent different intersection strategies.

star with LP propagates the star abstraction and uses an LP to check for an intersection
adaptive uses different (precise or approximate) intersection checks based on the state of the search