Output-property DSL API

The property guide explains strictness, Boolean composition, input coordinates and certification. The tutorial constructs and trains a complete example.

Represent input-output specifications through affine comparisons and Boolean formulas.

A PropertySpec associates an output formula with closed input boxes. Affine comparisons define satisfaction margins; conjunction and disjunction combine them using minimum and maximum. These formulas can be compiled into fixed computation graphs for auto_LiRPA bound propagation.

Outputs

Construct symbolic references to network output coordinates.

For example, y = Outputs() followed by And(y[0] >= -0.75, y[0] <= 0.75) defines an output-range property. Use And and Or to combine comparisons; Python's and, or and chained comparisons do not construct symbolic formulas.

Source code in CTRAIN/properties/__init__.py

class Outputs:
    """Construct symbolic references to network output coordinates.

    For example, y = Outputs() followed by And(y[0] >= -0.75, y[0] <= 0.75)
    defines an output-range property. Use And and Or to combine comparisons;
    Python's and, or and chained comparisons do not construct symbolic formulas.
    """
    def __getitem__(self, index):
        return OutputIndex(self, index)

Affine dataclass

Bases: _Symbolic

Represent an affine expression over network outputs.

The expression is the sum of coefficient-weighted outputs plus an offset. Arithmetic and comparison operators construct formulas without evaluating a network. Use Outputs()[i] to select an output coordinate.

Parameters:

Name	Type	Description	Default
coefficients	tuple	Unique nonnegative output indices paired with finite coefficients.	()
offset	float	Finite constant added to the weighted outputs.	0.0

Source code in CTRAIN/properties/__init__.py

@dataclass(frozen=True, eq=False)
class Affine(_Symbolic):
    """Represent an affine expression over network outputs.

    The expression is the sum of coefficient-weighted outputs plus an offset.
    Arithmetic and comparison operators construct formulas without evaluating a
    network. Use Outputs()[i] to select an output coordinate.

    Args:
        coefficients (tuple): Unique nonnegative output indices paired with finite coefficients.
        offset (float): Finite constant added to the weighted outputs.
    """
    coefficients: tuple = ()
    offset: float = 0.

    def __post_init__(self):
        coefficients = tuple(self.coefficients)
        if any(type(i) is not int or i < 0 for i, _ in coefficients) or len(
                {i for i, _ in coefficients}) != len(coefficients):
            raise ValueError('Affine coefficients require unique nonnegative output indices')
        object.__setattr__(self, 'coefficients', tuple((i, _number(v)) for i, v in coefficients))
        object.__setattr__(self, 'offset', _number(self.offset))

    def __add__(self, other):
        other = _affine(other)
        coefficients = dict(self.coefficients)
        for index, value in other.coefficients:
            coefficients[index] = coefficients.get(index, 0.) + value
        return Affine(tuple((i, _number(v)) for i, v in sorted(coefficients.items()) if v),
                      _number(self.offset + other.offset))

    __radd__ = __add__

    def __neg__(self):
        return self * -1

    def __sub__(self, other):
        return self + -_affine(other)

    def __rsub__(self, other):
        return _affine(other) - self

    def __mul__(self, constant):
        constant = _number(constant)
        return Affine(tuple((i, _number(v * constant)) for i, v in self.coefficients),
                      _number(self.offset * constant))

    __rmul__ = __mul__

    def __ge__(self, other):
        return Ge(self, other)

    def __le__(self, other):
        return Le(self, other)

    def __gt__(self, other):
        return Gt(self, other)

    def __lt__(self, other):
        return Lt(self, other)

    def tensors(self, output):
        """Return dense affine coefficients and offset in the output tensor's device and dtype."""
        n = output.shape[1]
        values = [0.] * n
        for index, value in self.coefficients:
            if not torch.jit.is_tracing() and index >= n:
                raise ValueError(f'Output index {index} is outside output width {n}')
            values[index] = value
        return output.new_tensor(values), output.new_tensor(self.offset)

    def evaluate(self, output):
        """Evaluate the affine expression on a batch of network outputs."""
        coefficients, offset = self.tensors(output)
        return torch.nn.functional.linear(output, coefficients.unsqueeze(0), offset.reshape(1))

evaluate(output)

Evaluate the affine expression on a batch of network outputs.

Source code in CTRAIN/properties/__init__.py

def evaluate(self, output):
    """Evaluate the affine expression on a batch of network outputs."""
    coefficients, offset = self.tensors(output)
    return torch.nn.functional.linear(output, coefficients.unsqueeze(0), offset.reshape(1))

tensors(output)

Return dense affine coefficients and offset in the output tensor's device and dtype.

Source code in CTRAIN/properties/__init__.py

def tensors(self, output):
    """Return dense affine coefficients and offset in the output tensor's device and dtype."""
    n = output.shape[1]
    values = [0.] * n
    for index, value in self.coefficients:
        if not torch.jit.is_tracing() and index >= n:
            raise ValueError(f'Output index {index} is outside output width {n}')
        values[index] = value
    return output.new_tensor(values), output.new_tensor(self.offset)

Box dataclass

Define a closed input region through coordinatewise lower and upper endpoints.

Endpoints must be finite, ordered and have matching nonempty shapes. They are stored as detached float64 CPU tensors; bounding routines convert them to model coordinates with outward rounding.

Parameters:

Name	Type	Description	Default
lower	Tensor or sequence	Lower endpoint, excluding the batch dimension.	required
upper	Tensor or sequence	Upper endpoint with the same shape.	required

Source code in CTRAIN/properties/__init__.py

@dataclass(frozen=True, eq=False)
class Box:
    """Define a closed input region through coordinatewise lower and upper endpoints.

    Endpoints must be finite, ordered and have matching nonempty shapes. They
    are stored as detached float64 CPU tensors; bounding routines convert them
    to model coordinates with outward rounding.

    Args:
        lower (Tensor or sequence): Lower endpoint, excluding the batch dimension.
        upper (Tensor or sequence): Upper endpoint with the same shape.
    """
    lower: torch.Tensor
    upper: torch.Tensor

    def __post_init__(self):
        lower = torch.as_tensor(self.lower, dtype=torch.float64).detach().cpu().clone()
        upper = torch.as_tensor(self.upper, dtype=torch.float64).detach().cpu().clone()
        if lower.shape != upper.shape or lower.ndim < 1 or lower.numel() == 0 or not (
                torch.isfinite(lower).all() and torch.isfinite(upper).all() and (lower <= upper).all()):
            raise ValueError('Box endpoints must be finite, ordered, nonempty, and have matching shapes')
        object.__setattr__(self, 'lower', lower)
        object.__setattr__(self, 'upper', upper)

    def to_dict(self):
        """Return the input endpoints as lists for manifests and checkpoints."""
        return dict(lower=self.lower.tolist(), upper=self.upper.tolist())

to_dict()

Return the input endpoints as lists for manifests and checkpoints.

Source code in CTRAIN/properties/__init__.py

def to_dict(self):
    """Return the input endpoints as lists for manifests and checkpoints."""
    return dict(lower=self.lower.tolist(), upper=self.upper.tolist())

PropertySpec dataclass

Associate an output formula with the input regions where it must hold.

The specification requires the formula to hold for every input in every supplied box. Task examples and property regions are independent inputs to training.

Parameters:

Name	Type	Description	Default
name	str	Nonempty specification name, unique within a wrapper.	required
formula	Comparison or Junction	Affine or Boolean output formula.	required
domains	Iterable[Box]	Nonempty collection of closed input regions.	required

Source code in CTRAIN/properties/__init__.py

@dataclass(frozen=True, eq=False)
class PropertySpec:
    """Associate an output formula with the input regions where it must hold.

    The specification requires the formula to hold for every input in every
    supplied box. Task examples and property regions are independent inputs to
    training.

    Args:
        name (str): Nonempty specification name, unique within a wrapper.
        formula (Comparison or Junction): Affine or Boolean output formula.
        domains (Iterable[Box]): Nonempty collection of closed input regions.
    """
    name: str
    formula: object
    domains: tuple

    def __post_init__(self):
        domains = tuple(self.domains)
        if not isinstance(self.name, str) or not self.name or not isinstance(
                self.formula, (Comparison, Junction)) or not domains or any(
                not isinstance(d, Box) for d in domains):
            raise ValueError('PropertySpec requires a name, formula, and nonempty Box domains')
        object.__setattr__(self, 'domains', domains)

    def to_dict(self):
        """Return the specification name, formula and input boxes as serialisable data."""
        return dict(name=self.name, formula=self.formula.to_dict(),
                    domains=[d.to_dict() for d in self.domains])

to_dict()

Return the specification name, formula and input boxes as serialisable data.

Source code in CTRAIN/properties/__init__.py

def to_dict(self):
    """Return the specification name, formula and input boxes as serialisable data."""
    return dict(name=self.name, formula=self.formula.to_dict(),
                domains=[d.to_dict() for d in self.domains])

PropertyGraph

Bases: Module

Append a fixed satisfaction-margin computation to a network.

The composed graph shares the original network's trainable weights and adds no trainable parameters. Bounding its output gives a lower satisfaction margin over an input region.

Parameters:

Name	Type	Description	Default
model	Module	Network whose outputs the formula references.	required
formula	Comparison or Junction	Output specification to compile.	required
relu	bool	Whether to express minimum and maximum through ReLU operations.	False
output_width	int	Number of network outputs; required when it cannot be inferred from the last layer.	None

Source code in CTRAIN/properties/__init__.py

class PropertyGraph(nn.Module):
    """Append a fixed satisfaction-margin computation to a network.

    The composed graph shares the original network's trainable weights and adds
    no trainable parameters. Bounding its output gives a lower satisfaction
    margin over an input region.

    Args:
        model (torch.nn.Module): Network whose outputs the formula references.
        formula (Comparison or Junction): Output specification to compile.
        relu (bool): Whether to express minimum and maximum through ReLU operations.
        output_width (int, optional): Number of network outputs; required when it cannot be
            inferred from the last layer.
    """
    def __init__(self, model, formula, relu=False, output_width=None):
        super().__init__()
        self.model, self.formula, self.relu = model, formula, relu
        if output_width is None:
            last = model[-1] if isinstance(model, nn.Sequential) else model
            output_width = getattr(last, 'out_features', None)
        if type(output_width) is not int or output_width < 1:
            raise ValueError('Supply output_width for a custom verification graph')
        reference = next(model.parameters(), None)
        if reference is None:
            reference = next(model.buffers(), torch.zeros(()))
        self.compiled = _CompiledFormula(formula, output_width, reference, relu)

    def forward(self, inputs):
        """Evaluate the network and return its compiled satisfaction margin."""
        return self.compiled(self.model(inputs))

forward(inputs)

Evaluate the network and return its compiled satisfaction margin.

Source code in CTRAIN/properties/__init__.py

def forward(self, inputs):
    """Evaluate the network and return its compiled satisfaction margin."""
    return self.compiled(self.model(inputs))

OutputIndex(output, index)

Return an affine expression selecting one network output.

Parameters:

Name	Type	Description	Default
output	Outputs	Symbolic output collection.	required
index	int	Nonnegative output coordinate.	required

Returns:

Type	Description
Affine	Expression with coefficient one at the selected coordinate.

Source code in CTRAIN/properties/__init__.py

def OutputIndex(output, index):
    """Return an affine expression selecting one network output.

    Args:
        output (Outputs): Symbolic output collection.
        index (int): Nonnegative output coordinate.

    Returns:
        (Affine): Expression with coefficient one at the selected coordinate.
    """
    if not isinstance(output, Outputs) or type(index) is not int or index < 0:
        raise ValueError('OutputIndex requires Outputs and a nonnegative integer index')
    return Affine(((index, 1.),))

Ge(lhs, rhs, scale=1.0)

Construct lhs >= rhs with satisfaction margin (lhs - rhs) / scale.

Source code in CTRAIN/properties/__init__.py

def Ge(lhs, rhs, scale=1.):
    """Construct lhs >= rhs with satisfaction margin (lhs - rhs) / scale."""
    return Comparison(_affine(lhs) - rhs, scale=scale)

Le(lhs, rhs, scale=1.0)

Construct lhs <= rhs with satisfaction margin (rhs - lhs) / scale.

Source code in CTRAIN/properties/__init__.py

def Le(lhs, rhs, scale=1.):
    """Construct lhs <= rhs with satisfaction margin (rhs - lhs) / scale."""
    return Ge(rhs, lhs, scale)

Gt(lhs, rhs, scale=1.0)

Construct lhs > rhs with satisfaction margin (lhs - rhs) / scale.

Source code in CTRAIN/properties/__init__.py

def Gt(lhs, rhs, scale=1.):
    """Construct lhs > rhs with satisfaction margin (lhs - rhs) / scale."""
    return Comparison(_affine(lhs) - rhs, strict=True, scale=scale)

Lt(lhs, rhs, scale=1.0)

Construct lhs < rhs with satisfaction margin (rhs - lhs) / scale.

Source code in CTRAIN/properties/__init__.py

def Lt(lhs, rhs, scale=1.):
    """Construct lhs < rhs with satisfaction margin (rhs - lhs) / scale."""
    return Gt(rhs, lhs, scale)

And(*children)

Construct a conjunction of at least two output formulas.

Source code in CTRAIN/properties/__init__.py

def And(*children):
    """Construct a conjunction of at least two output formulas."""
    return Junction('and', tuple(children))

Or(*children)

Construct a disjunction of at least two output formulas.

Source code in CTRAIN/properties/__init__.py

def Or(*children):
    """Construct a disjunction of at least two output formulas."""
    return Junction('or', tuple(children))

load_vnnlib_property is documented in the loader reference. For lower-level integrations, see property bounds, certification and counterexample search, and task/property losses.