Property certification and counterexample API

Prefer PropertyModelWrapper.certify_properties for ordinary use. These functions implement the same property certification workflow. Reports distinguish whole-domain certification, unresolved cells and witnessed violations; a negative relaxation bound alone does not establish a violation.

Certification

Explicit evaluation properties use fresh graphs and original boxes without changing the training specifications or stored partition. Lazy property datasets support full-box certification without refinement or complete solving; explicit properties are required for those operations.

Check general specifications over the full declared input regions.

Each original region remains covered during optional refinement. The method computes fresh bounds and can pass unresolved cells to alpha-beta-CROWN. Separate properties construct fresh graphs and do not change training specifications or the stored partition.

Parameters:

Name	Type	Description	Default
wrapper	PropertyModelWrapper	Model, bound options and input specifications.	required
method	str	Sound bound method: IBP, CROWN-IBP, CROWN or ALPHA-CROWN.	'CROWN'
refine	bool	Whether to subdivide unresolved cells within the refinement budget.	True
complete	bool	Whether to invoke alpha-beta-CROWN on unresolved requirements.	False
max_cells	int	Cell limit per original box; None uses the wrapper setting.	None
max_depth	int	Split-depth limit; None uses the wrapper setting.	None
results_path	str	Solver-artifact directory; required for complete verification.	None
timeout	float	Positive solver time limit in seconds per unresolved requirement.	60
properties	Sequence[PropertySpec]	Separate specifications to evaluate from their original boxes.	None

Returns:

Type	Description
dict	Whole-cover certified flag, per-property summaries, per-cell bounds and outcomes, method and elapsed seconds. A lazy property dataset instead returns aggregate counts and margins and requires refine=False and complete=False.

Source code in CTRAIN/eval/properties.py

def certify_properties(wrapper, method='CROWN', refine=True, complete=False,
                       max_cells=None, max_depth=None, results_path=None, timeout=60,
                       properties=None):
    """Check general specifications over the full declared input regions.

    Each original region remains covered during optional refinement. The method
    computes fresh bounds and can pass unresolved cells to alpha-beta-CROWN.
    Separate properties construct fresh graphs and do not change training
    specifications or the stored partition.

    Args:
        wrapper (PropertyModelWrapper): Model, bound options and input specifications.
        method (str): Sound bound method: IBP, CROWN-IBP, CROWN or ALPHA-CROWN.
        refine (bool): Whether to subdivide unresolved cells within the refinement budget.
        complete (bool): Whether to invoke alpha-beta-CROWN on unresolved requirements.
        max_cells (int, optional): Cell limit per original box; None uses the wrapper
            setting.
        max_depth (int, optional): Split-depth limit; None uses the wrapper setting.
        results_path (str, optional): Solver-artifact directory; required for complete
            verification.
        timeout (float): Positive solver time limit in seconds per unresolved requirement.
        properties (Sequence[PropertySpec], optional): Separate specifications to evaluate
            from their original boxes.

    Returns:
        (dict): Whole-cover certified flag, per-property summaries, per-cell
            bounds and outcomes, method and elapsed seconds. A lazy property
            dataset instead returns aggregate counts and margins and requires
            refine=False and complete=False.
    """
    from CTRAIN.bound.properties import CERTIFICATION_METHODS
    if method not in CERTIFICATION_METHODS or type(refine) is not bool or type(complete) is not bool:
        raise ValueError('Invalid certification method or flags')
    if wrapper.property_dataset is not None and properties is None:
        if refine or complete:
            raise ValueError('Lazy property datasets support full-box bounds without refinement '
                             'or complete verification; supply explicit properties for those modes')
        return certify_property_dataset(wrapper, method, results_path)
    max_cells = wrapper.max_cells if max_cells is None else max_cells
    max_depth = wrapper.max_depth if max_depth is None else max_depth
    if type(max_cells) is not int or max_cells < 1 or type(max_depth) is not int or max_depth < 0:
        raise ValueError('Invalid refinement budget')
    if complete and (results_path is None or not math.isfinite(timeout) or timeout <= 0):
        raise ValueError('Complete verification requires results_path and positive finite timeout')
    start = time.monotonic()
    specs, bounds = wrapper.properties, wrapper.bounds
    cells = list(wrapper.partition)
    if properties is not None:
        from CTRAIN.bound.properties import PropertyBounds
        specs = tuple(properties)
        if (not specs or any(not isinstance(p, PropertySpec) for p in specs)
                or len({p.name for p in specs}) != len(specs)):
            raise ValueError('Evaluation properties require nonempty specs with unique names')
        bounds = PropertyBounds(wrapper.verification_model, wrapper.verification_input_shape,
                                specs, wrapper.configuration['bound_opts'] or None)
        cells = initial_partition(specs)
    validate_partition(cells, specs)
    while True:
        rows, _ = evaluate_cells(bounds, cells, method, wrapper.property_batch_size)
        children = refine_partition(cells, rows, specs, wrapper.split_count,
                                    max_cells, max_depth) if refine else cells
        if len(children) == len(cells):
            break
        cells = children
    if complete:
        complete_cells(wrapper, cells, rows, results_path, timeout, specs)
    summaries = [dict(name=spec.name, certified=all(r['outcome'] == 'certified'
                    for r in rows if r['property'] == spec.name)) for spec in specs]
    return dict(certified=all(p['certified'] for p in summaries), properties=summaries,
                cells=rows, method=method, seconds=time.monotonic() - start)

Compute fresh full-box bounds for every region in a lazy property dataset.

Returns aggregate certification counts and lower margins without materialising all endpoints or consuming the dataset's random sampling stream. Detailed cell refinement and complete verification use explicit property boxes.

Source code in CTRAIN/eval/properties.py

def certify_property_dataset(wrapper, method='CROWN', results_path=None):
    """Compute fresh full-box bounds for every region in a lazy property dataset.

    Returns aggregate certification counts and lower margins without materialising
    all endpoints or consuming the dataset's random sampling stream. Detailed
    cell refinement and complete verification use explicit property boxes.
    """
    start = time.monotonic()
    report = evaluate_property_dataset(wrapper.bounds, wrapper.property_dataset, method,
                                       wrapper.property_batch_size)
    report.update(properties=[dict(name=wrapper.properties[0].name, certified=report['certified'])],
                  property_dataset=wrapper.configuration['property_dataset'],
                  method=method, seconds=time.monotonic() - start)
    if results_path is not None:
        import json
        directory = Path(results_path)
        directory.mkdir(parents=True, exist_ok=True)
        (directory / 'results.json').write_text(json.dumps(report, indent=2, allow_nan=False))
    return report

Counterexample search

find_counterexample searches one declared box for an input that violates the formula's Boolean semantics, including strictness and ties. It returns the checked input as a CPU Python list, or None if no violation was found. An unsuccessful search is not a certificate. Model modes, buffers and existing parameter gradients are preserved.

Search an input box for a concrete violation of the output formula.

Projected gradient-sign steps minimise the satisfaction margin. Returns a violating input as a list, or None when no violation was found. The search uses inward-rounded endpoints and preserves caller modes and gradient flags.

Source code in CTRAIN/eval/properties.py

def find_counterexample(model, formula, box, steps=30):
    """Search an input box for a concrete violation of the output formula.

    Projected gradient-sign steps minimise the satisfaction margin. Returns a
    violating input as a list, or None when no violation was found. The search
    uses inward-rounded endpoints and preserves caller modes and gradient flags.
    """
    reference = next(model.parameters(), None)
    if reference is None:
        reference = next(model.buffers(), torch.zeros(()))
    lower, upper = box.lower.to(reference), box.upper.to(reference)
    # Attack points must be inside the declared box, not its outward dtype enclosure.
    lower = torch.where(lower.double() < box.lower.to(lower.device),
                        torch.nextafter(lower, torch.full_like(lower, float('inf'))), lower)
    upper = torch.where(upper.double() > box.upper.to(upper.device),
                        torch.nextafter(upper, torch.full_like(upper, -float('inf'))), upper)
    if (lower > upper).any():
        return None
    with preserve_model_state(model), torch.enable_grad():
        model.eval()
        point = ((lower + upper) / 2).unsqueeze(0)
        for _ in range(steps + 1):
            point = point.detach().requires_grad_(True)
            output = model(point)
            if not formula.evaluate(output).all():
                return point.detach().cpu()[0].tolist()
            margin = formula.margin(output)
            if not margin.requires_grad:
                break
            gradient = torch.autograd.grad(margin.sum(), point, allow_unused=True)[0]
            if gradient is None:
                break
            point = torch.maximum(lower, torch.minimum(upper,
                point - .1 * (upper - lower) * gradient.sign()))
    return None