Property and task loss API

The property trainer combines a task loss with a property objective. See the property guide for margin semantics and strategy selection.

Property margin loss

property_loss accepts a batch of lower margins. Hinge loss sums deficits over obligations, then averages regions unless reduction='none'. Cross-entropy uses the padded-margin objective and ignores the hinge slack parameter. A training loss is distinct from a whole-domain certificate.

Penalise deficits in property satisfaction margins.

The hinge loss sums max(0, margin - lower_margin) over requirements and vanishes once each target margin is reached. Cross-entropy instead uses a zero-padded margin vector. Reduction averages over boxes unless set to none.

Source code in CTRAIN/train/certified/losses/properties.py

def property_loss(lower_bounds, margin=1e-3, *, loss='hinge', reduction='mean'):
    """Penalise deficits in property satisfaction margins.

    The hinge loss sums max(0, margin - lower_margin) over requirements and
    vanishes once each target margin is reached. Cross-entropy instead uses a
    zero-padded margin vector. Reduction averages over boxes unless set to none.
    """
    if not torch.isfinite(lower_bounds).all():
        raise FloatingPointError('Non-finite property bounds during training')
    if loss == 'cross_entropy':
        from CTRAIN.train.certified.losses.util import get_loss_from_bounds
        return get_loss_from_bounds(lower_bounds, torch.nn.CrossEntropyLoss(reduction='none'), reduction=reduction)
    if loss != 'hinge' or reduction not in ('mean', 'none'):
        raise ValueError('Invalid property loss or reduction')
    values = torch.relu(margin - lower_bounds).sum(dim=1)
    return values.mean() if reduction == 'mean' else values

Training strategies

The dispatcher receives explicit bound/model inputs and validated method options. The legacy get_property_training_loss(wrapper, ...) entry point delegates to it for compatibility.

Compute the selected training objective for a batch of property regions.

Each strategy reuses the shared satisfaction margins with its bound-based, adversarial, hybrid or regularised loss. The result is a scalar penalty for training; whole-region certification separately computes fresh sound bounds.

Source code in CTRAIN/train/certified/losses/property_methods.py

def compute_property_training_loss(bounds, spec_index, boxes, *, verification_model,
                                   training_method, training_options, margin, reference):
    """Compute the selected training objective for a batch of property regions.

    Each strategy reuses the shared satisfaction margins with its bound-based,
    adversarial, hybrid or regularised loss. The result is a scalar penalty for
    training; whole-region certification separately computes fresh sound bounds.
    """
    method, options = training_method, training_options
    def penalty(margins):
        return property_loss(margins, margin, loss=options['loss'])
    if method == 'CROWN-IBP':
        beta = options['beta']
        lower = bounds(spec_index, boxes, 'CROWN-IBP') if beta else None
        if beta < 1:
            ibp = bounds(spec_index, boxes, 'IBP')
            lower = ibp if beta == 0 else beta * lower + (1 - beta) * ibp
        return penalty(lower)
    if method in METHODS or method == 'GLS':
        bound_method = options['bound_method'] if method == 'GLS' else method
        return penalty(bounds(spec_index, boxes, bound_method,
                                      relu_upper_retention=options.get('relu_upper_retention', 1.)))
    alpha = options.get('alpha')
    if alpha == 1:
        return penalty(bounds(spec_index, boxes, 'IBP',
                                      relu_upper_retention=options['relu_upper_retention']))
    def point_margins(output, *, boolean=False):
        return bounds.point_margins(spec_index, output, boolean=boolean)
    lower, upper = box_endpoints(boxes, reference)
    nominal, half_width = (lower + upper) / 2, (upper - lower) / 2
    search = get_pgd_ptb(PerturbationLpNorm(norm=float('inf'), x_L=lower, x_U=upper),
                         nominal, options['pgd_region_factor'], eps=half_width)
    search_lower, search_upper = search.x_L, search.x_U
    attack = dict(restarts=options['pgd_restarts'], step_size=options['pgd_step_size'],
                  early_stopping=options['pgd_early_stopping'], device=nominal.device,
                  decay_factor=options['pgd_decay_factor'], decay_checkpoints=options['pgd_decay_checkpoints'],
                  loss_fn=lambda output, _: (property_loss(
                      point_margins(output),
                      loss='cross_entropy', reduction='none') if options['loss'] == 'cross_entropy'
                      else -point_margins(output).amin(1)),
                  is_success=lambda output, _: ~point_margins(output, boolean=True).all(1))
    if method == 'SABR':
        center, radius, _ = get_propagation_region(
            verification_model, nominal, None, options['subselection_ratio'],
            options['pgd_step_size'], options['pgd_steps'], options['pgd_restarts'],
            x_L=lower, x_U=upper, pgd_x_L=search_lower, pgd_x_U=search_upper,
            early_stopping=options['pgd_early_stopping'], decay_factor=options['pgd_decay_factor'],
            decay_checkpoints=options['pgd_decay_checkpoints'], loss_fn=attack['loss_fn'], is_success=attack['is_success'])
        sub_lower, sub_upper = torch.maximum(lower, center - radius), torch.minimum(upper, center + radius)
        subregions = [Box(lo, hi) for lo, hi in zip(sub_lower.detach(), sub_upper.detach())]
        return penalty(bounds(spec_index, subregions, 'IBP',
                                      relu_upper_retention=options['relu_upper_retention']))
    adversarial = pgd_attack(verification_model, nominal, None, search_lower, search_upper,
                             n_steps=options['pgd_steps'], **attack)
    output = verification_model(adversarial)
    adversarial_margins = point_margins(output)
    adversarial_loss = penalty(adversarial_margins)
    if method == 'PGD' or alpha == 0:
        return adversarial_loss
    if method == 'IBP-R':
        area = nominal.new_zeros(len(nominal))
        if options['rho']:
            raw = bounds.raw
            raw(nominal)
            ptb = PerturbationLpNorm(norm=float('inf'), x_L=lower, x_U=upper)
            compute_ibp_bounds(raw, options['relu_upper_retention'],
                x=(BoundedTensor(nominal, ptb),), method='IBP', bound_upper=True)
            area = relu_area(raw, nominal)
            if options['regularisation_mask']:
                area = area * point_margins(output.detach(), boolean=True).all(1)
        return adversarial_loss + options['rho'] * area.mean()
    lower_margins = bounds(spec_index, boxes, 'IBP',
                                  relu_upper_retention=options['relu_upper_retention'])
    robust_loss = penalty(lower_margins)
    if method == 'MTL-IBP':
        return _combine_mtl(alpha, robust_loss, adversarial_loss)
    if method == 'CC-IBP':
        return penalty(alpha * lower_margins + (1 - alpha) * adversarial_margins)
    return _combine_exp(alpha, robust_loss, adversarial_loss)

Advisory preservation

For models whose lowest score selects an action, use fixed source-model argmin labels sampled before repair. This empirical task loss does not certify advisory preservation. The ONNX/VNNLIB notebook shows the complete workflow.

Preserve source ACAS Xu advisories through cross-entropy on negated scores.

The lowest output score selects an advisory, so negating scores produces classification logits. Targets are integer source-model argmin advisories sampled before repair, with ties resolved by the first argmin. This empirical fidelity loss does not certify advisory preservation.

Parameters:

Name	Type	Description	Default
scores	Tensor	Repaired model costs of shape (batch, actions).	required
target	Tensor	Source advisory indices of shape (batch,), with dtype torch.long.	required

Returns:

Type	Description
Tensor	Mean cross-entropy over the batch.

Source code in CTRAIN/train/certified/losses/properties.py

def advisory_cross_entropy(scores, target):
    """Preserve source ACAS Xu advisories through cross-entropy on negated scores.

    The lowest output score selects an advisory, so negating scores produces
    classification logits. Targets are integer source-model argmin advisories
    sampled before repair, with ties resolved by the first argmin. This empirical
    fidelity loss does not certify advisory preservation.

    Args:
        scores (torch.Tensor): Repaired model costs of shape (batch, actions).
        target (torch.Tensor): Source advisory indices of shape (batch,), with dtype
            torch.long.

    Returns:
        (torch.Tensor): Mean cross-entropy over the batch.
    """
    return F.cross_entropy(-scores, target)

Independent arithmetic heads

mnist_addition_cross_entropy expects [batch, 39] logits split into digit, digit and sum heads of widths 10, 10 and 19, with [batch, 3] integer labels [a, b, a+b]. It averages cross-entropy across the three heads. See the arithmetic notebook.

Average cross-entropy for independently predicted digits and their sum.

Predictions concatenate heads of widths 10, 10 and 19; integer targets contain [a, b, a+b]. This task loss does not itself enforce arithmetic consistency.

Source code in CTRAIN/train/certified/losses/properties.py

def mnist_addition_cross_entropy(logits, target):
    """Average cross-entropy for independently predicted digits and their sum.

    Predictions concatenate heads of widths 10, 10 and 19; integer targets contain
    [a, b, a+b]. This task loss does not itself enforce arithmetic consistency.
    """
    if (logits.ndim != 2 or logits.shape[1] != 39
            or target.shape != (len(logits), 3) or target.dtype != torch.long):
        raise ValueError('Expected [batch,39] logits and [batch,3] long targets')
    heads = logits.split((10, 10, 19), dim=1)
    return torch.stack([F.cross_entropy(head, target[:, i])
                        for i, head in enumerate(heads)]).mean()