abCROWN integration API

See the complete-verification guide for a wrapper-based example and backend settings.

The shared evaluation guide explains screening, ONNX/VNNLIB export, saved result identity and continuation. Use the pinned dependencies from CTRAIN's installer rather than an unrelated auto_LiRPA installation. Bundled verifier source retains its upstream provenance and license.

Execute alpha-beta-CROWN queries and preserve certified, falsified and unresolved outcomes.

abcrown_eval(*args, **kwargs)

Run one alpha-beta-CROWN query with isolated temporary artifacts.

The arguments follow _abcrown_eval. Returns elapsed time and solver status; exceptions become unknown and explicit timeouts remain timeout outcomes.

Source code in CTRAIN/complete_verification/abCROWN/verify.py

def abcrown_eval(*args, **kwargs):
    """Run one alpha-beta-CROWN query with isolated temporary artifacts.

    The arguments follow _abcrown_eval. Returns elapsed time and solver status;
    exceptions become unknown and explicit timeouts remain timeout outcomes.
    """
    start = time.monotonic()
    with tempfile.TemporaryDirectory(prefix='ctrain-abcrown-instance-') as directory:
        try:
            return _abcrown_eval(*args, **kwargs, _work_dir=directory)
        except TimeoutError:
            return time.monotonic() - start, 'timeout'
        except Exception:
            traceback.print_exc()
            return time.monotonic() - start, 'unknown'

limited_abcrown_eval(work_dir=None, runner_path=None, *args, **kwargs)

Run alpha-beta-CROWN in a subprocess using the active Python interpreter.

Arguments are exchanged through isolated temporary files. An outer wall-time limit terminates the process group; process failures remain unknown rather than being interpreted as certificates. Returns elapsed time and status.

Source code in CTRAIN/complete_verification/abCROWN/verify.py

def limited_abcrown_eval(work_dir=None, runner_path=None, *args, **kwargs):
    """Run alpha-beta-CROWN in a subprocess using the active Python interpreter.

    Arguments are exchanged through isolated temporary files. An outer wall-time
    limit terminates the process group; process failures remain unknown rather
    than being interpreted as certificates. Returns elapsed time and status.
    """
    timeout = kwargs['timeout'] * 1.2
    runner_path = runner_path or str(Path(__file__).with_name('runner.py'))
    start = time.monotonic()
    with tempfile.TemporaryDirectory(dir=work_dir, prefix='ctrain-abcrown-') as directory:
        args_path = Path(directory) / 'args.pkl'
        result_path = Path(directory) / 'result.pkl'
        with args_path.open('wb') as file:
            pickle.dump((args, kwargs), file)
        try:
            process = subprocess.Popen([sys.executable, runner_path, str(args_path), str(result_path)], start_new_session=True)
            try:
                process.wait(timeout=timeout)
            except subprocess.TimeoutExpired:
                try:
                    os.killpg(process.pid, signal.SIGKILL)
                except ProcessLookupError:
                    pass
                process.wait()
                return time.monotonic() - start, 'timeout'
            if process.returncode != 0:
                return time.monotonic() - start, 'unknown'
            with result_path.open('rb') as file:
                return pickle.load(file)
        except (OSError, ValueError, EOFError, pickle.UnpicklingError):
            return time.monotonic() - start, 'unknown'

Execute one serialised alpha-beta-CROWN query in a separate Python process.

Configure alpha-beta-CROWN and express local robustness queries in VNNLIB.

get_abcrown_standard_conf(timeout=600, no_cores=28)

Construct the default alpha-beta-CROWN configuration.

The bundled configuration is parsed into a fresh dictionary and updated with the available device, branch-and-bound timeout and MIP worker count.

Parameters:

Name	Type	Description	Default
timeout	int	The timeout value for the BAB solver in seconds.	600
no_cores	int	The number of parallel solvers to use.	28

Returns:

Type	Description
dict	The updated standard configuration dictionary.

Source code in CTRAIN/complete_verification/abCROWN/util.py

def get_abcrown_standard_conf(timeout=600, no_cores=28):
    """Construct the default alpha-beta-CROWN configuration.

    The bundled configuration is parsed into a fresh dictionary and updated with
    the available device, branch-and-bound timeout and MIP worker count.

    Args:
        timeout (int, optional): The timeout value for the BAB solver in seconds.
        no_cores (int, optional): The number of parallel solvers to use.

    Returns:
      (dict): The updated standard configuration dictionary.
    """
    f = StringIO(STD_CONF)

    std_conf = yaml.load(f, Loader=Loader)

    device = 'cuda' if torch.cuda.is_available() else 'mps' if torch.backends.mps.is_available() else 'cpu'

    std_conf['general']['device'] = device
    std_conf['bab']['timeout'] = timeout
    std_conf['solver']['mip']['parallel_solvers'] = no_cores

    return std_conf

instances_to_vnnlib(indices, data, vnnlib_path, experiment_name, eps, eps_temp, data_min, data_max, no_classes)

Write one VNNLIB robustness query for each selected dataset input.

Parameters:

Name	Type	Description	Default
indices	list of int	List of indices of the data instances to be converted.	required
data	Dataset	Dataset containing the data instances.	required
vnnlib_path	str	Path where the VNN-LIB files will be saved.	required
experiment_name	str	Name of the experiment for documentation purposes.	required
eps	float	Epsilon value for the adversarial robustness property.	required
eps_temp	float	Temporary epsilon value used for domain calculation.	required
data_min	float	Minimum value for data normalisation/clamping.	required
data_max	float	Maximum value for data normalisation/clamping.	required
no_classes	int	Number of classes in the classification task.	required

Returns:

Type	Description
list of str	List of file paths to the generated VNN-LIB files.

Source code in CTRAIN/complete_verification/abCROWN/util.py

def instances_to_vnnlib(indices, data, vnnlib_path, experiment_name, eps, eps_temp, data_min, data_max, no_classes):
    """Write one VNNLIB robustness query for each selected dataset input.

    Args:
        indices (list of int): List of indices of the data instances to be converted.
        data (torch.utils.data.Dataset): Dataset containing the data instances.
        vnnlib_path (str): Path where the VNN-LIB files will be saved.
        experiment_name (str): Name of the experiment for documentation purposes.
        eps (float): Epsilon value for the adversarial robustness property.
        eps_temp (float): Temporary epsilon value used for domain calculation.
        data_min (float): Minimum value for data normalisation/clamping.
        data_max (float): Maximum value for data normalisation/clamping.
        no_classes (int): Number of classes in the classification task.

    Returns:
      (list of str): List of file paths to the generated VNN-LIB files.
    """
    vnnlib_list_test = []
    for idx in indices:
        x, ground_truth = data[idx]
        ground_truth = torch.as_tensor(ground_truth).cpu().numpy()
        x = torch.as_tensor(x).cpu()
        eps_temp = torch.as_tensor(eps_temp).cpu()
        data_min = torch.as_tensor(data_min).cpu()
        data_max = torch.as_tensor(data_max).cpu()
        print(f'idx_{idx}_eps_{eps}')
        # Record the results: vnn-lib specification.
        filename = os.path.join(vnnlib_path, f"idx_{idx}-eps{eps}.vnnlib")
        comment = f"Adversarial robustness property for {experiment_name}. l_inf radius: {eps}, " \
                f"Test Image {idx}."
        comment = ' '.join(comment.splitlines()).strip()
        # ground_truth = np.argmax(ground_truth)
        domain = torch.stack(
            [(x - eps_temp).clamp(data_min, data_max),
            (x + eps_temp).clamp(data_min, data_max)], dim=-1)
        write_adversarial_robustness_vnnlib(filename, comment, domain, ground_truth, n_classes=no_classes)
        vnnlib_list_test.append(filename)

    return vnnlib_list_test

write_adversarial_robustness_vnnlib(filename, initial_comment, input_domain, ground_truth, n_classes=10)

Write a clipped input box and a classification counterexample query as VNNLIB.

The output assertion asks whether any competing class can match or exceed the ground-truth score. An unsatisfiable query therefore certifies strict classification margins throughout the supplied box.

Parameters:

Name	Type	Description	Default
filename	str	The name of the file to write the vnnlib specification to.	required
initial_comment	str	A comment to include at the top of the vnnlib file.	required
input_domain	Tensor	A tensor representing the input domain, i.e. lower and upper bounds per input, with shape (n, 2), where n is the number of input variables.	required
ground_truth	int	The index of the ground truth class.	required
n_classes	int	The number of output classes.	10

Source code in CTRAIN/complete_verification/abCROWN/util.py

def write_adversarial_robustness_vnnlib(filename, initial_comment, input_domain, ground_truth, n_classes=10):
    """Write a clipped input box and a classification counterexample query as VNNLIB.

    The output assertion asks whether any competing class can match or exceed
    the ground-truth score. An unsatisfiable query therefore certifies strict
    classification margins throughout the supplied box.

    Args:
        filename (str): The name of the file to write the vnnlib specification to.
        initial_comment (str): A comment to include at the top of the vnnlib file.
        input_domain (torch.Tensor): A tensor representing the input domain, i.e. lower and
            upper bounds per input, with shape (n, 2), where n is
            the number of input variables.
        ground_truth (int): The index of the ground truth class.
        n_classes (int, optional): The number of output classes.
    """

    with open(filename, "w") as f:
        f.write(f"; {initial_comment}\n")

        # Declare input variables.
        f.write("\n")
        linearized_domain = input_domain.view(-1, 2)
        for i in range(linearized_domain.shape[0]):
            f.write(f"(declare-const X_{i} Real)\n")
        f.write("\n")

        # Declare output variables.
        for i in range(n_classes):
            f.write(f"(declare-const Y_{i} Real)\n")
        f.write("\n")

        # Define input constraints.
        f.write(f"; Input constraints:\n")
        for i in range(linearized_domain.shape[0]):
            f.write(f"(assert (<= X_{i} {linearized_domain[i, 1]}))\n")  # UB
            f.write(f"(assert (>= X_{i} {linearized_domain[i, 0]}))\n")  # LB
            f.write("\n")
        f.write("\n")

        # Define output constraints, providing an unnecessary "and" to ease parsing in vnn-comp-21.
        f.write(f"; Output constraints (encoding the conditions for a property counter-example):\n")
        f.write(f"(assert (or\n")
        for i in range(n_classes):
            if i != ground_truth:
                f.write(f"\t(and (<= Y_{ground_truth} Y_{i}))\n")
        f.write(f"))\n")
        f.write("\n")