diff --git a/act/back_end/cli.py b/act/back_end/cli.py index 677b6cf41..6fff57420 100644 --- a/act/back_end/cli.py +++ b/act/back_end/cli.py @@ -17,6 +17,7 @@ import datetime import glob import json +import logging import os import statistics import sys @@ -32,6 +33,7 @@ _TF_MODES: tuple[str, ...] = ("interval", "hybridz") _SOLVERS: tuple[str, ...] = tuple(sorted(_VALID_SOLVERS)) +logger = logging.getLogger(__name__) def _strip_optional(tp: Any) -> Any: @@ -965,11 +967,13 @@ def main(): default=None, dest="solver", help=( - "Solver backend. Three alternative families:\n" + "Solver backend:\n" " 'gurobi' — commercial MILP/LP (license required). LP cascade.\n" " 'torchlp' — PyTorch-tensor LP (Adam + penalty + box projection,\n" " GPU-capable). LP cascade.\n" - " 'dual' — DualSolver, linear-relaxation dual certified bounds via\n" + " 'hybridz' — Hybrid Zonotope propagation with a standalone open-source\n" + " MILP verdict; automatically selects HybridzTF.\n" + " 'dual' — DualSolver, linear-relaxation dual certified bounds via\n" " backward propagation. No LP cascade (DualSolver is\n" " its own verification pipeline).\n" " 'auto' — try gurobi, fall back to torchlp.\n" @@ -993,8 +997,8 @@ def main(): "Forward-bounds transfer function: 'interval' or 'hybridz'. Selects " "the abstract interpretation used during analyze() to seed bounds " "for the LP cascade. Default: configured default (typically " - "'interval'). For dual certified bounds, use --solver dual instead " - "(dual is a solver, not a TF — see --solver help)." + "'interval'). The standalone hybridz solver selects HybridzTF " + "automatically; dual does not use this option." ), ) verify_group.add_argument( @@ -1295,10 +1299,20 @@ def main(): _ap.Namespace(device=backend_cfg.device, dtype=backend_cfg.dtype) ) - if args.tf_mode is not None: + tf_mode = args.tf_mode + if backend_cfg.solver == "hybridz": + if tf_mode is not None and tf_mode != "hybridz": + logger.warning( + "--solver hybridz requires the hybridz transformer; overriding " + "--tf-mode %s", + tf_mode, + ) + tf_mode = "hybridz" + + if tf_mode is not None: from act.back_end.analyze import initialize_tf_mode - initialize_tf_mode(args.tf_mode) + initialize_tf_mode(tf_mode) # Set the solver-mode global so verify_once / _verify_one_net can dispatch # dual ↔ LP-cascade without consulting the TF mode (refactor decoupled diff --git a/act/pipeline/cli.py b/act/pipeline/cli.py index 69d114b38..8b568a8c0 100644 --- a/act/pipeline/cli.py +++ b/act/pipeline/cli.py @@ -652,6 +652,19 @@ def cmd_fuzz(args): # ============================================================================ +def _effective_tf_modes(solver: str, requested_modes) -> list[str]: + modes = list(requested_modes or ["interval"]) + if solver != "hybridz": + return modes + if requested_modes is not None and modes != ["hybridz"]: + logger.warning( + "--solvers hybridz requires the hybridz transformer; overriding " + "--tf-modes %s", + " ".join(modes), + ) + return ["hybridz"] + + def _build_validator(args): from act.pipeline.verification.validate_verifier import VerificationValidator @@ -702,10 +715,15 @@ def _verify_and_validate_cell( """ from act.back_end.verifier import verify_once + verify_kwargs = ( + {"timelimit": getattr(args, "timeout", None)} + if solver == "hybridz" + else {} + ) if args.validate_soundness: - results, facts = verify_once(net, collect_facts=True) + results, facts = verify_once(net, collect_facts=True, **verify_kwargs) else: - results = verify_once(net) + results = verify_once(net, **verify_kwargs) facts = None statuses = [r.status.name for r in results] print(f" {cell_label if cell_label is not None else tag}: {statuses}") @@ -733,10 +751,8 @@ def _run_vnnlib_verify(args) -> bool: ``synthesize_models_from_specs`` → ``TorchToACT`` → ``verify_once``. Single-mode per invocation, matching the ``act.back_end --verify`` CLI - contract: uses the first element of ``--tf-modes`` (default - ``"interval"``) and ``--solvers`` (default ``"torchlp"``). Multi-mode - sweeps are the caller's job — invoke once per (tf-mode, solver) cell. - Dual ignores ``--tf-modes`` because it's a backward Solver. + contract. Multi-mode sweeps are the caller's job. Dual ignores + ``--tf-modes``; the standalone HybridZ solver selects HybridzTF. """ from act.front_end.vnnlib_loader.create_specs import VNNLibSpecCreator from act.front_end.model_synthesis import synthesize_models_from_specs @@ -749,8 +765,8 @@ def _run_vnnlib_verify(args) -> bool: if not args.category: raise ValueError("--verify vnnlib requires --category (e.g. --category acasxu_2023)") - tf_mode = (args.tf_modes or ["interval"])[0] solver = (args.solvers or ["torchlp"])[0] + tf_mode = _effective_tf_modes(solver, args.tf_modes)[0] set_solver_mode(solver) if solver != "dual": @@ -959,8 +975,8 @@ def _run_torchvision_verify(args) -> bool: if not args.dataset: raise ValueError("--verify torchvision requires --dataset (e.g. --dataset MNIST)") - tf_mode = (args.tf_modes or ["interval"])[0] solver = (args.solvers or ["torchlp"])[0] + tf_mode = _effective_tf_modes(solver, args.tf_modes)[0] set_solver_mode(solver) if solver != "dual": @@ -1036,14 +1052,13 @@ def _run_netfactory_verify(args) -> bool: if "gurobi" in solvers and not is_gurobi_available(): logger.warning("Skipping gurobi solver: gurobipy is not available.") solvers = [s for s in solvers if s != "gurobi"] - tf_modes = args.tf_modes or ["interval"] batch_sizes = _resolve_batch_sizes(getattr(args, "batch_sizes", None)) per_neuron_config = _per_neuron_config(args) errors_seen = False for name in networks: for solver in solvers: - for tf_mode in tf_modes: + for tf_mode in _effective_tf_modes(solver, args.tf_modes): for batch_size in batch_sizes: try: set_solver_mode(solver) @@ -1261,11 +1276,13 @@ def main(): # Single (tf, solver) per invocation; matrix sweeps by repeated calls. python -m act.pipeline --verify vnnlib --category acasxu_2023 --max-instances 3 --tf-modes interval --solvers torchlp python -m act.pipeline --verify vnnlib --category acasxu_2023 --max-instances 3 --tf-modes hybridz --solvers torchlp + python -m act.pipeline --verify vnnlib --category acasxu_2023 --max-instances 3 --solvers hybridz python -m act.pipeline --verify vnnlib --category acasxu_2023 --max-instances 3 --solvers dual # Run verifier on a TorchVision dataset-model pair end-to-end. python -m act.pipeline --verify torchvision --dataset MNIST --model simple_cnn --num-samples 2 --tf-modes interval --solvers torchlp python -m act.pipeline --verify torchvision --dataset MNIST --model simple_cnn --num-samples 2 --tf-modes hybridz --solvers torchlp + python -m act.pipeline --verify torchvision --dataset MNIST --model simple_cnn --num-samples 2 --solvers hybridz python -m act.pipeline --verify torchvision --dataset MNIST --model simple_cnn --num-samples 2 --solvers dual # Run unified two-level verifier validation after verification. @@ -1457,7 +1474,10 @@ def main(): "--timeout", type=float, default=None, - help="Timeout in seconds (default: from config.yaml)", + help=( + "Time budget in seconds for fuzzing, BaB, or standalone HybridZ " + "verification (default: component configuration)" + ), ) fuzz_group.add_argument( "--output", @@ -1531,13 +1551,20 @@ def main(): "--solvers", nargs="+", default=["gurobi", "torchlp"], - help="Solvers for Level 1 validation (default: gurobi torchlp)", + help=( + "Verification solvers: gurobi, torchlp, hybridz, or dual " + "(default: gurobi torchlp)" + ), ) validation_group.add_argument( "--tf-modes", nargs="+", - default=["interval"], - help="Transfer function modes for Level 2 bounds validation: interval, hybridz, dual (default: interval)", + default=None, + help=( + "Transfer function modes for bounds propagation: interval or " + "hybridz (default: interval); standalone hybridz selects HybridzTF " + "and dual ignores this option" + ), ) validation_group.add_argument( "--input-samples",