Skip to content

feat(hybridz): complete frontend solver integration #99

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Kaijie-liu wants to merge 1 commit into from
Closed

feat(hybridz): complete frontend solver integration #99

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 20 additions & 6 deletions act/back_end/cli.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
import datetime
import glob
import json
import logging
import os
import statistics
import sys
Expand All @@ -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:
Expand Down Expand Up @@ -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"
Expand All @@ -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(
Expand Down Expand Up @@ -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
Expand Down
55 changes: 41 additions & 14 deletions act/pipeline/cli.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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}")
Expand Down Expand Up @@ -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
Expand All @@ -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":
Expand Down Expand Up @@ -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":
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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",
Expand Down Expand Up @@ -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",
Expand Down
Loading