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(in_coef_mat=None, in_bias_mat=None, out_coef_mat=None, out_bias_mat=None)[source]

Bases: object

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

in_coef_mat[source]

Matrix of the coefficients for the input constraints.

Type:: torch.Tensor

in_bias_mat[source]

Matrix of the biases for the input constraints.

Type:: torch.Tensor

out_coef_mat[source]

Matrices of the coefficients for the output constraints.

Type:: list[torch.Tensor]

out_bias_mat[source]

Matrices of the biases for the output constraints.

Type:: list[torch.Tensor]

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, input_id='X', output_id='Y')[source]

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

Parameters:

input_id (str, Optional) – Identifier of the input node (default: ‘X’)
output_id (str, Optional) – Identifier of the output node (default: ‘Y’)
filepath (str) – Path to the SMT-LIB file to create

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.

Return type:

bool

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 if the network is safe, False otherwise

Return type:

bool

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:

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:

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:

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:

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