From ffd93aba08acce8a58ca3c2f71d2b05fa30ff12b Mon Sep 17 00:00:00 2001 From: guanqin-123 Date: Fri, 28 Aug 2026 10:02:40 +1000 Subject: [PATCH 01/10] refactor(back_end): retire 13 uncollected self-tests behind two CI gates bab.py carried 14 self-tests behind a hand-rolled `__main__` runner and onnx_converter.py one stray `test_onnx_conversion`. Per-test coverage attribution (each test run alone, import-only baseline subtracted, then differenced against a 27-case e2e union built by expanding every loop axis in act-bab.yml) showed which of them still protect anything. Deleted -- zero residual coverage, no assertion the e2e union lacks: test_imports, test_random_branching, test_random_bounding Deleted -- assertion is vacuous or unreachable from production: _test_bab_kbatch_status_parity: k=1/2/4/8 all end at nodes=32, exhausted_budget_nodes=True. The statuses agree because the budget ran out, not because K-batching preserves results. test_split_subproblems: the fixture leaves incremental_alpha, eta, split_signs and parent_margins as None, so `_clone_dict_tensors` only ever takes its `is not None` short-circuit. Degrading the clone to an alias would not fail this test. test_config_yaml_roundtrip: BaBConfig.from_yaml/to_yaml have no production caller -- BaB config is built via BaBConfig(**merged) at config.py:606/790/861. The test was keeping dead code alive. test_random_branching_with_mask: nothing in production passes unstable_mask to compute_scores (bab.py:1952 passes bounds_dict and nu_per_layer, :1964 passes none; branching.py:91 is a docstring), so RandomBranching's neuron-split branch is unreachable. test_subproblem_batch, test_babnode_compat: accessor smoke tests. Migrated to CI, then deleted: _test_bab_budget_exhaustion_returns_unknown -> "BaB soundness -- budget exhaustion returns UNKNOWN". Same two assertions against a real torchlp solver on mlp_plain_3x8, which unlike bab_deep survives presolve and enters BaB. Every other step in this workflow asserts throughput; this is the first to assert the verifier does not claim more than it proved. _test_bab_oom_fails_loud -> an inline AST check in act-bab.yml. A real OOM cannot be raised deterministically in CI, so the invariant is now checked structurally: no try/except may wrap setup_and_solve_batch or solve_batch. This covers every call site rather than the single path the fixture reached, and guards against the `except (ValueError, RuntimeError, ...): return None` idiom already present at bab.py:289 spreading to the solve path. An ast-grep rule was rejected first -- its `$$$` form missed the case where the assignment is the last statement in the try block. Not migrated: _test_bab_k_fluctuates asserts a performance property, not a soundness one, and K-batch width is not exposed in metadata. `_k_log` itself is kept: it is documented diagnostic API. Kept: _test_check_violations_batched_per_kind and its scalar-params sibling. Adding --bab to the range/margin/unsafe netfactory run absorbs only 7 of their 33 residual lines; the other 26 are broadcast shapes ((1,width), (n_batch,width), batched d) that real nets never emit. Both recompute the expected mask independently via argmax/einsum and compare with torch.equal, so a broadcasting bug surfaces as a failed assert rather than a silently wrong CERTIFIED. codecov project target 74% -> 75%: deleting test_onnx_conversion drops 41 uncovered statements; the `__main__` blocks and pragma'd self-tests were already outside the denominator, so nothing else moves. Pure deletion in both modules (0 insertions), plus five test-only imports (os, tempfile, BabNode, split_subproblems, RandomBranching) dropped alongside their last callers. bab.py self-tests: 2 passed. The inline gate was exercised by parsing the workflow and running the extracted shell: green on bab.py and verifier.py, red on a positive control that includes the case where the guarded call is the last statement in the try block. lsp clean; act.back_end.bab exports unchanged. --- .codecov.yml | 2 +- .github/workflows/act-bab.yml | 58 ++++ act/back_end/bab/bab.py | 285 ------------------ act/front_end/vnnlib_loader/onnx_converter.py | 42 --- 4 files changed, 59 insertions(+), 328 deletions(-) diff --git a/.codecov.yml b/.codecov.yml index 264d2aab9..1ed8aedaf 100644 --- a/.codecov.yml +++ b/.codecov.yml @@ -14,7 +14,7 @@ coverage: status: project: default: - target: 74% + target: 75% threshold: 1% informational: false patch: diff --git a/.github/workflows/act-bab.yml b/.github/workflows/act-bab.yml index d7c6e040e..2d929798c 100644 --- a/.github/workflows/act-bab.yml +++ b/.github/workflows/act-bab.yml @@ -45,6 +45,41 @@ jobs: python -m pip install --upgrade pip pip install coverage torch onnx onnx2torch "onnx-simplifier" "onnxsim==0.6.5" pandas numpy scipy pyyaml tqdm psutil + # ── Solve path must not swallow solver exceptions ────────────────── + # Replaces the former _test_bab_oom_fails_loud self-test. That test only + # covered the one path reachable from its fixture; this covers every + # call site. A real OOM cannot be triggered deterministically in CI, so + # the invariant is checked structurally instead of at runtime. + - name: BaB soundness — no exception swallowing on the solve path + run: | + cd ${{ github.workspace }} + python - act/back_end/bab/bab.py act/back_end/verifier.py <<'PY' + import ast, sys + GUARDED = {"setup_and_solve_batch", "solve_batch"} + failed = False + for arg in sys.argv[1:]: + tree = ast.parse(open(arg).read()) + for node in ast.walk(tree): + if not isinstance(node, ast.Try): + continue + hits = set() + for stmt in node.body: + for sub in ast.walk(stmt): + if isinstance(sub, ast.Call): + fn = sub.func + name = fn.attr if isinstance(fn, ast.Attribute) else getattr(fn, "id", None) + if name in GUARDED: + hits.add(name) + if hits: + failed = True + print(f"{arg}:{node.lineno}: solver call {sorted(hits)} sits inside try/except") + if failed: + print("\nA swallowed solver exception turns resource exhaustion into " + "'not provable'. If an unproven lane is then pruned, BaB reports " + "CERTIFIED for a box it never solved. Let it propagate.") + sys.exit(1 if failed else 0) + PY + # ── BaB module unit tests ────────────────────────────────────────── - name: BaB module run: | @@ -231,6 +266,29 @@ jobs: coverage run -p -m act.back_end --verify --network act/back_end/examples/nets/layer_testing_bab_deep.json \ --solver dual --method planar --device cpu --dtype float64 + # =================================================================== + # Soundness gate: a BaB run that exhausts its node budget with unproven + # sub-boxes left in the pool MUST report UNKNOWN, never CERTIFIED. Every + # other step here asserts throughput (node counts, exit codes); this is + # the only one asserting the verifier does not claim more than it proved. + # + # layer_testing_bab_deep is certified by presolve and never branches, so + # it cannot exhaust anything -- mlp_plain_3x8 is the net that survives + # presolve and enters BaB. --verbose is load-bearing: backend_cli only + # prints result.metadata under it. + # =================================================================== + - name: BaB soundness — budget exhaustion returns UNKNOWN + run: | + cd ${{ github.workspace }} + out=$(coverage run -p -m act.back_end --verify \ + --network "$ACT_NETS_DIR/mlp_plain_3x8_64x64_3962224133.json" \ + --bab --bab-max-depth 10 --bab-max-subproblems 2 --bab-max-batch-size 1 \ + --solver torchlp --device cpu --dtype float64 --verbose 2>&1) + echo "$out" + grep -q "Lane 0: VerifyStatus.UNKNOWN" <<<"$out" + grep -q "reason: budget_exhausted_with_unproven_subboxes" <<<"$out" + grep -q "exhausted_budget_nodes: True" <<<"$out" + # =================================================================== # Dual MATMUL bilinear kernel (tf_transformer): dual-tier soundness on # the MATMUL layer-testing net (torchlp sweep never exercises dual here). diff --git a/act/back_end/bab/bab.py b/act/back_end/bab/bab.py index 25fc43894..402a749d8 100644 --- a/act/back_end/bab/bab.py +++ b/act/back_end/bab/bab.py @@ -16,9 +16,7 @@ import logging import math -import os import sys -import tempfile import time import inspect from dataclasses import dataclass @@ -35,18 +33,15 @@ VALID_SOLVER_TIERS, ) from act.back_end.bab.node import ( - BabNode, SubproblemBatch, concat_children, rederive_embedding_block_eps, split_input, split_input_nary, split_neuron_subproblems, - split_subproblems, ) from act.back_end.bab.branching.branching import ( BranchingStrategy, - RandomBranching, SplitDecision, _build_branching_strategy as _build_branching_strategy_impl, _collect_neuron_candidates, @@ -2145,138 +2140,10 @@ def verify_bab( # --------------------------------------------------------------------------- -class _StubNet: # pragma: no cover - layers = [] -def test_imports(): # pragma: no cover - for sym in ( - verify_bab, - BaBConfig, - BabNode, - SubproblemBatch, - split_subproblems, - BranchingStrategy, - BoundingStrategy, - RandomBranching, - RandomBounding, - ): - assert sym is not None - - -def test_config_yaml_roundtrip(): # pragma: no cover - c1 = BaBConfig() - assert c1.max_depth == 20 - - c2 = BaBConfig.from_yaml() - assert c2.branching_method == "random" - - c3 = BaBConfig.from_yaml(max_depth=50, branching_method="kfsb") - assert c3.max_depth == 50 and c3.branching_method == "kfsb" - - # Round-trip through a standalone BaB YAML (uses top-level "bab" key) - tmp = tempfile.mktemp(suffix=".yaml") - try: - c3.to_yaml(tmp) - c4 = BaBConfig.from_yaml(tmp) - assert c4.max_depth == 50 - assert c4.branching_method == "kfsb" - finally: - os.unlink(tmp) - - # BaBConfig must not expose a time_budget_s attribute. - assert not hasattr(c1, "time_budget_s") - - -def test_subproblem_batch(): # pragma: no cover - lb = torch.tensor([[-1.0, -2.0, -3.0]]) - ub = torch.tensor([[1.0, 2.0, 3.0]]) - batch = SubproblemBatch(lb=lb, ub=ub, depths=torch.tensor([0])) - - assert batch.batch_size == 1 - assert batch.input_dim == 3 - assert batch.total_width().item() == 12.0 - - bounds = Bounds(lb.squeeze(0), ub.squeeze(0)) - batch2 = SubproblemBatch.from_bounds(bounds) - assert torch.equal(batch2.lb, lb) - - back = batch2.to_bounds_list() - assert len(back) == 1 - assert torch.equal(back[0].lb, bounds.lb) - - -def test_split_subproblems(): # pragma: no cover - lb = torch.tensor([[-1.0, -2.0, -3.0]]) - ub = torch.tensor([[1.0, 2.0, 3.0]]) - batch = SubproblemBatch(lb=lb, ub=ub, depths=torch.tensor([0])) - split_dim = torch.tensor([1]) - - left, right = split_subproblems(batch, split_dim) - - mid = (lb[0, 1] + ub[0, 1]) / 2 - assert torch.isclose(left.ub[0, 1], mid) - assert torch.isclose(right.lb[0, 1], mid) - assert left.depths[0] == 1 - assert right.depths[0] == 1 - - assert torch.equal(left.lb[0, 0], lb[0, 0]) - assert torch.equal(right.ub[0, 2], ub[0, 2]) - -def test_random_branching(): # pragma: no cover - lb = torch.tensor([[-1.0, -2.0, -3.0]]) - ub = torch.tensor([[1.0, 2.0, 3.0]]) - batch = SubproblemBatch(lb=lb, ub=ub, depths=torch.tensor([0])) - brancher = RandomBranching() - scores = brancher.compute_scores(batch, cast(Net, cast(object, _StubNet()))) - assert scores.shape == (1, 3) - assert (scores >= 0).all() - - dims = cast(torch.Tensor, brancher.select(scores)) - assert dims.shape == (1,) - assert 0 <= dims.item() <= 2 - - -def test_random_branching_with_mask(): # pragma: no cover - lb = torch.tensor([[-1.0, -2.0, -3.0]]) - ub = torch.tensor([[1.0, 2.0, 3.0]]) - batch = SubproblemBatch(lb=lb, ub=ub, depths=torch.tensor([0])) - mask = torch.tensor([False, True, False]) - - brancher = RandomBranching() - scores = brancher.compute_scores(batch, cast(Net, cast(object, _StubNet())), unstable_mask=mask) - assert scores[0, 0].item() == 0.0 - assert scores[0, 2].item() == 0.0 - assert cast(torch.Tensor, brancher.select(scores)).item() == 1 - - -def test_random_bounding(): # pragma: no cover - lb = torch.tensor([[-1.0, -2.0], [0.0, 0.0]]) - ub = torch.tensor([[1.0, 2.0], [3.0, 4.0]]) - batch = SubproblemBatch(lb=lb, ub=ub, depths=torch.tensor([0, 1])) - - pool = RandomBounding() - assert pool.empty - - pool.push(batch) - assert len(pool) == 2 - - popped = pool.pop(1) - assert popped.batch_size == 1 - assert len(pool) == 1 - - pool.pop(1) - assert pool.empty - - -def test_babnode_compat(): # pragma: no cover - bounds = Bounds(torch.tensor([-1.0, -2.0]), torch.tensor([1.0, 2.0])) - node = BabNode(box=bounds, depth=3, score=0.5) - batch = node.to_batch() - assert batch.batch_size == 1 - assert batch.depths[0].item() == 3 class _IdentityOutput(torch.nn.Module): # pragma: no cover @@ -2410,161 +2277,9 @@ def _test_check_violations_batched_b1_scalar_params(): # pragma: no cover # --------------------------------------------------------------------------- -# C12: K-batched verify_bab_batched test fixtures -# --------------------------------------------------------------------------- - - -def _load_bab_deep_net() -> Optional[Net]: # pragma: no cover - """Load layer_testing_bab_deep.json from examples/nets, or None if absent. - - Returns None silently when the fixture is missing so tests can skip rather - than hard-fail in isolated environments. Forces CPU device for hermetic - test execution: the BaB integration tests must not depend on GPU - availability or device-manager global state. - """ - from pathlib import Path - - from act.back_end.serialization.serialization import load_net_from_file - from act.util.device_manager import initialize_device - - here = Path(__file__).resolve() - candidate = here.parents[1] / "examples" / "nets" / "layer_testing_bab_deep.json" - if not candidate.exists(): - return None - initialize_device("cpu", "float64") - return load_net_from_file(str(candidate), target_device="cpu") - - -class _UnknownSolver(Solver): # pragma: no cover - """Mock solver: returns UNKNOWN on every lane (forces BaB to branch).""" - - def solve_batch(self, problem, timelimit=None): - from act.back_end.solver.solver_base import BatchLPSolution - - n = problem.N - return BatchLPSolution( - statuses=tuple([SolveStatus.UNKNOWN] * n), - x=torch.zeros( - (n, problem.nvars), device=problem.lb.device, dtype=problem.lb.dtype, - ), - max_viol=torch.full( - (n,), float("nan"), device=problem.lb.device, dtype=problem.lb.dtype, - ), - ) - - -class _OOMSolver(Solver): # pragma: no cover - """Mock solver: raises an OOM-like exception on every solve_batch call.""" - - def solve_batch(self, problem, timelimit=None): - raise RuntimeError("CUDA out of memory: mocked for OOM-fails-loud test") - - -def _test_bab_kbatch_status_parity(): # pragma: no cover - net = _load_bab_deep_net() - if net is None: - print(" SKIP _test_bab_kbatch_status_parity: layer_testing_bab_deep.json absent") - return - from act.back_end.solver.solver_torchlp import TorchLPSolver - - config = BaBConfig(max_depth=6, max_nodes=32, verbose=False) - statuses_by_k: dict[int, VerifyStatus] = {} - for k in (1, 2, 4, 8): - result = verify_bab_batched( - net=net, - solver_factory=lambda: TorchLPSolver(), - config=config, - max_batch_size=k, - time_budget_s=60.0, - ) - statuses_by_k[k] = result.status - distinct = set(statuses_by_k.values()) - assert len(distinct) == 1, ( - f"K-batch status parity violated: {statuses_by_k}" - ) - - -def _test_bab_budget_exhaustion_returns_unknown(): # pragma: no cover - net = _load_bab_deep_net() - if net is None: - print(" SKIP _test_bab_budget_exhaustion_returns_unknown: fixture absent") - return - config = BaBConfig(max_depth=10, max_nodes=2, verbose=False) - result = verify_bab_batched( - net=net, - solver_factory=lambda: _UnknownSolver(), - config=config, - max_batch_size=1, - time_budget_s=30.0, - ) - assert result.status == VerifyStatus.UNKNOWN, ( - f"Expected UNKNOWN under-budget with mock-UNKNOWN solver, got " - f"{result.status}; metadata={result.metadata}" - ) - assert result.metadata.get("reason") == "budget_exhausted_with_unproven_subboxes", ( - f"Missing soundness-reason metadata: {result.metadata}" - ) - - -def _test_bab_oom_fails_loud(): # pragma: no cover - net = _load_bab_deep_net() - if net is None: - print(" SKIP _test_bab_oom_fails_loud: fixture absent") - return - config = BaBConfig(max_depth=5, max_nodes=10, verbose=False) - raised = False - try: - verify_bab_batched( - net=net, - solver_factory=lambda: _OOMSolver(), - config=config, - max_batch_size=4, - time_budget_s=10.0, - ) - except RuntimeError as e: - msg = str(e).lower() - assert "out of memory" in msg, f"Unexpected RuntimeError message: {e}" - raised = True - assert raised, "OOM exception was swallowed — silent fallback present" - - -def _test_bab_k_fluctuates(): # pragma: no cover - net = _load_bab_deep_net() - if net is None: - print(" SKIP _test_bab_k_fluctuates: fixture absent") - return - config = BaBConfig(max_depth=8, max_nodes=20, verbose=False) - k_log: List[int] = [] - _ = verify_bab_batched( - net=net, - solver_factory=lambda: _UnknownSolver(), - config=config, - max_batch_size=8, - time_budget_s=30.0, - _k_log=k_log, - ) - distinct = set(k_log) - assert len(distinct) >= 2, ( - f"K did not fluctuate across iterations (got {k_log}); dynamic K-batching " - f"requires at least 2 distinct K values per D4." - ) - - _TESTS = [ # pragma: no cover - test_imports, - test_config_yaml_roundtrip, - test_subproblem_batch, - test_split_subproblems, - test_random_branching, - test_random_branching_with_mask, - test_random_bounding, - test_babnode_compat, _test_check_violations_batched_per_kind, _test_check_violations_batched_b1_scalar_params, - _test_bab_kbatch_status_parity, - _test_bab_budget_exhaustion_returns_unknown, - _test_bab_oom_fails_loud, - _test_bab_k_fluctuates, ] diff --git a/act/front_end/vnnlib_loader/onnx_converter.py b/act/front_end/vnnlib_loader/onnx_converter.py index 71d7f8b38..aba299106 100644 --- a/act/front_end/vnnlib_loader/onnx_converter.py +++ b/act/front_end/vnnlib_loader/onnx_converter.py @@ -448,48 +448,6 @@ def _extract_shape_from_tensor(tensor) -> list: return shape -def test_onnx_conversion( - onnx_path: Path, - input_shape: Optional[Tuple[int, ...]] = None, - batch_size: int = 1 -) -> bool: - """ - Test ONNX to PyTorch conversion with dummy input. - - Args: - onnx_path: Path to .onnx file - input_shape: Input shape (inferred from model if not provided) - batch_size: Batch size for test input - - Returns: - True if conversion successful and model runs, False otherwise - """ - try: - # Convert model - pytorch_model = convert_onnx_to_pytorch(onnx_path) - - # Get input shape if not provided - if input_shape is None: - input_shape = get_onnx_input_shape(onnx_path) - - # Create dummy input - dummy_input = torch.randn(batch_size, *input_shape) - - # Run forward pass - with torch.no_grad(): - output = pytorch_model(dummy_input) - - logger.info( - f"ONNX conversion test passed: " - f"input {dummy_input.shape} -> output {output.shape}" - ) - return True - - except Exception as e: - logger.error(f"ONNX conversion test failed: {e}") - return False - - def get_onnx_metadata(onnx_path: Path) -> dict: """ Extract metadata from ONNX model. From 09dce7570153c1f19711c4f4511983880f93b000 Mon Sep 17 00:00:00 2001 From: guanqin-123 Date: Fri, 28 Aug 2026 15:02:39 +1000 Subject: [PATCH 02/10] refactor(back_end): retire the cons_exportor and verifier self-tests Two embedded self-test batteries are removed from production modules. cons_exportor's 18 are replaced by a torchlp sweep over the 59 layer_testing nets. verifier.py's 16 are dropped outright; that file was 63% test scaffolding (1363 of 2153 lines) and is now production code only. Neither dtype job runs a self-test step any more. Retiring them exposed that the gate meant to cover those paths was not actually a gate. per_neuron_bounds' check_hookable_alignment() treated hookable_layers == 0 as "aligned" rather than "nothing to verify", so a net whose kinds were all absent from _ACT_KIND_TO_MODULE ran with no hooks, checked no neurons, and printed "All 0 checks passed". 120 of 222 validation runs were green ticks over zero work. Zero-check runs are now SKIPPED and excluded from the pass tally, and the smooth activations plus the 1:1 transformer ops are mapped and emitted as real modules so their bounds are actually checked. Pre- versus post-activation is decided from the ACT layer kind rather than the traced module name, matching DualSolver's compute_forward_bounds( post_activation=False) contract: nonlinear relaxations store the incoming box, affine, shape, pooling and bilinear handlers store the outgoing one. Module names are a tracing detail and never defined which tensor a bound represented; deriving it from them compared cos(x) against the box for x and produced 87 false violations in float32. Verified by shrinking tf_sin's interval 10% toward its midpoint: the gate previously exited 0 with 0 violations, and now reports the SIN neuron violation and exits 1. Both dtypes report 0 violations across 132 checked runs with 0 zero-check runs. The solve-path exception gate is also simplified to a comprehension over Try nodes, verified to still flag both guarded call sites. --- .github/workflows/act-bab.yml | 36 +- .github/workflows/act-backend-float32.yml | 5 - .github/workflows/act-backend-float64.yml | 7 +- act/back_end/cons_exportor.py | 1014 ------------ act/back_end/verifier.py | 1374 ----------------- act/pipeline/verification/act2torch.py | 244 ++- .../verification/per_neuron_bounds.py | 95 +- .../verification/validate_verifier.py | 17 +- 8 files changed, 343 insertions(+), 2449 deletions(-) diff --git a/.github/workflows/act-bab.yml b/.github/workflows/act-bab.yml index 2d929798c..d25b05a07 100644 --- a/.github/workflows/act-bab.yml +++ b/.github/workflows/act-bab.yml @@ -56,28 +56,26 @@ jobs: python - act/back_end/bab/bab.py act/back_end/verifier.py <<'PY' import ast, sys GUARDED = {"setup_and_solve_batch", "solve_batch"} - failed = False - for arg in sys.argv[1:]: - tree = ast.parse(open(arg).read()) - for node in ast.walk(tree): - if not isinstance(node, ast.Try): - continue - hits = set() - for stmt in node.body: - for sub in ast.walk(stmt): - if isinstance(sub, ast.Call): - fn = sub.func - name = fn.attr if isinstance(fn, ast.Attribute) else getattr(fn, "id", None) - if name in GUARDED: - hits.add(name) - if hits: - failed = True - print(f"{arg}:{node.lineno}: solver call {sorted(hits)} sits inside try/except") - if failed: + def called(node): + for sub in ast.walk(node): + fn = getattr(sub, "func", None) + name = getattr(fn, "attr", None) or getattr(fn, "id", None) + if isinstance(sub, ast.Call) and name in GUARDED: + yield name + bad = sorted({ + (path, node.lineno, name) + for path in sys.argv[1:] + for node in ast.walk(ast.parse(open(path).read())) + if isinstance(node, ast.Try) + for stmt in node.body for name in called(stmt) + }) + for path, lineno, name in bad: + print(f"{path}:{lineno}: solver call {name!r} sits inside try/except") + if bad: print("\nA swallowed solver exception turns resource exhaustion into " "'not provable'. If an unproven lane is then pruned, BaB reports " "CERTIFIED for a box it never solved. Let it propagate.") - sys.exit(1 if failed else 0) + sys.exit(1 if bad else 0) PY # ── BaB module unit tests ────────────────────────────────────────── diff --git a/.github/workflows/act-backend-float32.yml b/.github/workflows/act-backend-float32.yml index bc03b53fc..f299ef940 100644 --- a/.github/workflows/act-backend-float32.yml +++ b/.github/workflows/act-backend-float32.yml @@ -60,11 +60,6 @@ jobs: cd ${{ github.workspace }} coverage run -p -m act.pipeline --verify act2torch --device cpu --dtype float32 - - name: Run Verifier Self-Tests (float32) - run: | - cd ${{ github.workspace }} - coverage run -p -m act.back_end.verifier - # ───────────────────────────────────────────────────────────────── # Soundness check (TF-agnostic): runs once before per-solver matrix. # See act-backend-float64.yml for the full rationale. diff --git a/.github/workflows/act-backend-float64.yml b/.github/workflows/act-backend-float64.yml index e2f5fb0a8..27c505ec2 100644 --- a/.github/workflows/act-backend-float64.yml +++ b/.github/workflows/act-backend-float64.yml @@ -65,10 +65,13 @@ jobs: cd ${{ github.workspace }} coverage run -p -m act.pipeline --verify act2torch --device cpu --dtype float64 - - name: Run Verifier Self-Tests (float64) + - name: Constraint exporter — torchlp LP export over all layer_testing nets run: | cd ${{ github.workspace }} - coverage run -p -m act.back_end.verifier + for f in act/back_end/examples/nets/layer_testing_*.json; do + coverage run -p -m act.back_end --verify --network "$f" \ + --solver torchlp --device cpu --dtype float64 + done # ───────────────────────────────────────────────────────────────── # Soundness check (TF-agnostic): runs once before per-solver matrix. diff --git a/act/back_end/cons_exportor.py b/act/back_end/cons_exportor.py index b5cc90b6f..e222a7a78 100644 --- a/act/back_end/cons_exportor.py +++ b/act/back_end/cons_exportor.py @@ -2234,1017 +2234,3 @@ def export_to_batch_problem( obj_const=obj_const, ) - -# ============================================================================= -# Inline test battery for the batched exporter. Run via: -# python -m act.back_end.cons_exportor -# ============================================================================= - - -def _dense_block_rows(A_blockdiag: torch.Tensor, N: int, m: int, nvars: int): - """Return ``[N, m, nvars]`` dense view of a block-diagonal sparse matrix. - - Used for test assertions only; production code must NEVER call this on - large matrices. - """ - A_dense = A_blockdiag.to_dense() - rows = A_dense.view(N, m, N, nvars) - eye = torch.arange(N) - out = rows[eye, :, eye, :] - return out - - -def _build_relu_test_net(B: int, n: int, lb: torch.Tensor, ub: torch.Tensor): # pragma: no cover - """Net = INPUT -> INPUT_SPEC (BOX [B,n]) -> RELU -> ASSERT(LINEAR_LE). - - The ASSERT layer is required only because export_to_batch_problem - consults it; it does not affect the RELU encoding under test. - """ - from act.back_end.core import Layer, Net - from act.back_end.layer_schema import LayerKind - from act.front_end.specs import OutputSpec, OutKind - - device = lb.device - dtype = lb.dtype - in_v = list(range(n)) - out_v = list(range(n, 2 * n)) - spec_layer = OutputSpec( - kind=OutKind.LINEAR_LE, - c=torch.zeros(n, device=device, dtype=dtype), - d=torch.tensor(1.0, device=device, dtype=dtype), - ).encode_linear(B=B, n_out=n, device=device, dtype=dtype) - layers = [ - Layer( - id=0, kind=LayerKind.INPUT.value, - params={"shape": (B, n), "dtype": str(dtype)}, - in_vars=[], out_vars=in_v, - ), - Layer( - id=1, kind=LayerKind.INPUT_SPEC.value, - params={"kind": "BOX", "lb": lb, "ub": ub}, - in_vars=in_v, out_vars=in_v, - ), - Layer( - id=2, kind=LayerKind.RELU.value, - params={}, in_vars=in_v, out_vars=out_v, - ), - Layer( - id=3, kind=LayerKind.ASSERT.value, - params=spec_layer, in_vars=out_v, out_vars=out_v, - ), - ] - preds = {0: [], 1: [0], 2: [1], 3: [2]} - succs = {0: [1], 1: [2], 2: [3], 3: []} - return Net(layers=layers, preds=preds, succs=succs) - - -def _run_analyze(net, lb, ub): - from act.back_end.analyze import analyze - from act.back_end.core import Bounds, Con, ConSet, Fact - from act.front_end.specs import InKind - - input_layer_ids = [layer.id for layer in net.layers if layer.kind == "INPUT"] - if len(input_layer_ids) != 1: - raise ValueError(f"Expected exactly one INPUT layer, found {len(input_layer_ids)}.") - entry_id = input_layer_ids[0] - input_ids = list(net.by_id[entry_id].out_vars) - spec_layers = [layer for layer in net.layers if layer.kind == "INPUT_SPEC"] - seed = Bounds(lb.clone(), ub.clone()) - entry_fact = Fact(bounds=seed, cons=ConSet()) - for spec_layer in spec_layers: - kind = spec_layer.params.get("kind") - if kind == InKind.BOX: - entry_fact.cons.add_box( - -1, input_ids, - Bounds(spec_layer.params["lb"], spec_layer.params["ub"]), - ) - elif kind == InKind.LIN_POLY: - entry_fact.cons.replace( - Con( - "INEQ", tuple(input_ids), - { - "tag": "in:linpoly", - "A": spec_layer.params["A"], - "b": spec_layer.params["b"], - }, - ) - ) - else: - raise NotImplementedError(f"Unsupported INPUT_SPEC kind: {kind}") - _before, _after, globalC = analyze(net, entry_id, entry_fact) - return globalC - - -def _test_export_relu_canonical(): # pragma: no cover - """3 ineq rows per RELU neuron, ON/OFF/AMB slopes match Oracle §I.""" - torch.manual_seed(0) - B = 1 - n = 6 - lb = torch.tensor([[-2.0, -0.5, 1.0, 2.0, -1.0, -3.0]]) - ub = torch.tensor([[-0.1, 0.5, 3.0, 5.0, 2.0, -2.0]]) - net = _build_relu_test_net(B, n, lb, ub) - globalC = _run_analyze(net, lb, ub) - assert_layer = net.layers[-1] - bp = export_to_batch_problem( - net, globalC, assert_layer, - Bounds(lb=lb, ub=ub), - ) - expected_relu_rows = 3 * n - assert bp.m_le >= expected_relu_rows + 1, ( - f"expected at least {expected_relu_rows} + 1 rows; got {bp.m_le}" - ) - A_le_dense = _dense_block_rows(bp.A_le_blockdiag, bp.N, bp.m_le, bp.nvars) - rows = A_le_dense[0] - rhs = bp.b_le[0] - nvars_net = 2 * n - for i in range(n): - z_id = n + i - y_id = i - row_a = rows[3 * i] - row_b = rows[3 * i + 1] - row_c = rows[3 * i + 2] - assert float(row_a[z_id]) == -1.0, f"row_a[z_{i}] != -1" - assert float(rhs[3 * i]) == 0.0 - assert float(row_b[y_id]) == 1.0 and float(row_b[z_id]) == -1.0 - assert float(rhs[3 * i + 1]) == 0.0 - assert float(row_c[z_id]) == 1.0 - lb_i = float(lb[0, i]) - ub_i = float(ub[0, i]) - if lb_i >= 0: - expected_slope = 1.0 - expected_shift = 0.0 - elif ub_i <= 0: - expected_slope = 0.0 - expected_shift = 0.0 - else: - expected_slope = ub_i / (ub_i - lb_i) - expected_shift = -lb_i * expected_slope - coeff_on_y = float(row_c[y_id]) - assert abs(coeff_on_y - (-expected_slope)) < 1e-6, ( - f"neuron {i}: coeff_on_y={coeff_on_y} != -{expected_slope}" - ) - assert abs(float(rhs[3 * i + 2]) - expected_shift) < 1e-6, ( - f"neuron {i}: rhs={float(rhs[3 * i + 2])} != {expected_shift}" - ) - - -def _build_lrelu_test_net(B, n, lb, ub, alpha): # pragma: no cover - from act.back_end.core import Layer, Net - from act.back_end.layer_schema import LayerKind - from act.front_end.specs import OutputSpec, OutKind - - device = lb.device - dtype = lb.dtype - in_v = list(range(n)) - out_v = list(range(n, 2 * n)) - spec = OutputSpec( - kind=OutKind.LINEAR_LE, - c=torch.zeros(n, device=device, dtype=dtype), - d=torch.tensor(1.0, device=device, dtype=dtype), - ).encode_linear(B=B, n_out=n, device=device, dtype=dtype) - layers = [ - Layer( - id=0, kind=LayerKind.INPUT.value, - params={"shape": (B, n), "dtype": str(dtype)}, - in_vars=[], out_vars=in_v, - ), - Layer( - id=1, kind=LayerKind.INPUT_SPEC.value, - params={"kind": "BOX", "lb": lb, "ub": ub}, - in_vars=in_v, out_vars=in_v, - ), - Layer( - id=2, kind=LayerKind.LRELU.value, - params={"negative_slope": alpha}, in_vars=in_v, out_vars=out_v, - ), - Layer( - id=3, kind=LayerKind.ASSERT.value, - params=spec, in_vars=out_v, out_vars=out_v, - ), - ] - preds = {0: [], 1: [0], 2: [1], 3: [2]} - succs = {0: [1], 1: [2], 2: [3], 3: []} - return Net(layers=layers, preds=preds, succs=succs) - - -def _test_export_lrelu_canonical(): # pragma: no cover - """3 ineq per LRELU neuron with phase-degenerate slopes.""" - B = 1 - n = 4 - alpha = 0.1 - lb = torch.tensor([[-2.0, 0.5, -1.0, -3.0]]) - ub = torch.tensor([[-0.1, 2.0, 1.0, -2.0]]) - net = _build_lrelu_test_net(B, n, lb, ub, alpha) - globalC = _run_analyze(net, lb, ub) - bp = export_to_batch_problem( - net, globalC, net.layers[-1], - Bounds(lb=lb, ub=ub), - ) - assert bp.m_le >= 3 * n + 1, f"expected >= {3 * n + 1}, got {bp.m_le}" - A_dense = _dense_block_rows(bp.A_le_blockdiag, bp.N, bp.m_le, bp.nvars) - rows = A_dense[0] - rhs = bp.b_le[0] - for i in range(n): - z_id = n + i - y_id = i - row_a = rows[3 * i] - row_b = rows[3 * i + 1] - row_c = rows[3 * i + 2] - assert float(row_a[y_id]) == 1.0 and float(row_a[z_id]) == -1.0 - assert abs(float(row_b[y_id]) - alpha) < 1e-9 - assert float(row_b[z_id]) == -1.0 - assert float(row_c[z_id]) == 1.0 - lb_i = float(lb[0, i]) - ub_i = float(ub[0, i]) - if lb_i >= 0: - exp_slope = 1.0; exp_shift = 0.0 - elif ub_i <= 0: - exp_slope = alpha; exp_shift = 0.0 - else: - exp_slope = (ub_i - alpha * lb_i) / (ub_i - lb_i) - exp_shift = alpha * lb_i - exp_slope * lb_i - assert abs(float(row_c[y_id]) - (-exp_slope)) < 1e-6 - assert abs(float(rhs[3 * i + 2]) - exp_shift) < 1e-6 - - -def _build_tanh_test_net(B, n, lb, ub): # pragma: no cover - from act.back_end.core import Layer, Net - from act.back_end.layer_schema import LayerKind - from act.front_end.specs import OutputSpec, OutKind - - device = lb.device - dtype = lb.dtype - in_v = list(range(n)) - out_v = list(range(n, 2 * n)) - spec = OutputSpec( - kind=OutKind.LINEAR_LE, - c=torch.zeros(n, device=device, dtype=dtype), - d=torch.tensor(2.0, device=device, dtype=dtype), - ).encode_linear(B=B, n_out=n, device=device, dtype=dtype) - layers = [ - Layer( - id=0, kind=LayerKind.INPUT.value, - params={"shape": (B, n), "dtype": str(dtype)}, - in_vars=[], out_vars=in_v, - ), - Layer( - id=1, kind=LayerKind.INPUT_SPEC.value, - params={"kind": "BOX", "lb": lb, "ub": ub}, - in_vars=in_v, out_vars=in_v, - ), - Layer( - id=2, kind=LayerKind.TANH.value, - params={}, in_vars=in_v, out_vars=out_v, - ), - Layer( - id=3, kind=LayerKind.ASSERT.value, - params=spec, in_vars=out_v, out_vars=out_v, - ), - ] - preds = {0: [], 1: [0], 2: [1], 3: [2]} - succs = {0: [1], 1: [2], 2: [3], 3: []} - return Net(layers=layers, preds=preds, succs=succs) - - -def _test_export_tanh_canonical_5_cases(): # pragma: no cover - """100 random intervals spanning 5 cases: 4 valid ineq per element each. - - Validity check: for 50 random y ∈ [lo, hi], the LP-permitted z range - must INCLUDE tanh(y) (otherwise the relaxation is unsound). - """ - torch.manual_seed(42) - n = 5 - intervals = [] - for _ in range(20): - intervals.append( - (torch.rand(n) * 0.4 - 0.2, torch.rand(n) * 0.4 - 0.2) - ) - for _ in range(20): - lo = -torch.rand(n) * 3.0 - 0.5 - hi = -torch.rand(n) * 0.5 - intervals.append((torch.minimum(lo, hi), torch.maximum(lo, hi))) - for _ in range(20): - lo = torch.rand(n) * 0.5 - hi = torch.rand(n) * 3.0 + 0.5 - intervals.append((torch.minimum(lo, hi), torch.maximum(lo, hi))) - for _ in range(20): - lo = -torch.rand(n) * 3.0 - 0.1 - hi = torch.rand(n) * 3.0 + 0.1 - intervals.append((lo, hi)) - for _ in range(20): - center = (torch.rand(n) - 0.5) * 4.0 - half = torch.rand(n) * 1e-3 + 1e-6 - intervals.append((center - half, center + half)) - for k, (lo, hi) in enumerate(intervals): - lo_b = torch.where(lo <= hi, lo, hi).unsqueeze(0) - hi_b = torch.where(hi >= lo, hi, lo).unsqueeze(0) - if (hi_b - lo_b).min() < 0: - continue - net = _build_tanh_test_net(1, n, lo_b, hi_b) - globalC = _run_analyze(net, lo_b, hi_b) - bp = export_to_batch_problem( - net, globalC, net.layers[-1], - Bounds(lb=lo_b, ub=hi_b), - ) - expected_tanh_rows = 4 * n - assert bp.m_le >= expected_tanh_rows, ( - f"case {k}: expected >= {expected_tanh_rows}, got {bp.m_le}" - ) - A_dense = _dense_block_rows(bp.A_le_blockdiag, bp.N, bp.m_le, bp.nvars) - rows = A_dense[0] - rhs = bp.b_le[0] - torch.manual_seed(k) - for sample in range(50): - y_samp = lo_b[0] + (hi_b[0] - lo_b[0]) * torch.rand(n) - z_samp = torch.tanh(y_samp) - for i in range(n): - z_id = n + i - y_id = i - for r in range(4): - row = rows[4 * i + r] - coeff_z = float(row[z_id]) - coeff_y = float(row[y_id]) - lhs = coeff_z * float(z_samp[i]) + coeff_y * float(y_samp[i]) - assert lhs <= float(rhs[4 * i + r]) + 1e-4, ( - f"case {k} sample {sample} neuron {i} row {r}: " - f"tanh point ({float(y_samp[i])}, {float(z_samp[i])}) " - f"violates row coeffs (z={coeff_z}, y={coeff_y}, " - f"rhs={float(rhs[4 * i + r])}) -- lhs={lhs}" - ) - - -def _build_dense_test_net(B, n_in, n_out, W, b, lb_in, ub_in): # pragma: no cover - from act.back_end.core import Layer, Net - from act.back_end.layer_schema import LayerKind - from act.front_end.specs import OutputSpec, OutKind - - device = lb_in.device - dtype = lb_in.dtype - in_v = list(range(n_in)) - out_v = list(range(n_in, n_in + n_out)) - spec = OutputSpec( - kind=OutKind.LINEAR_LE, - c=torch.zeros(n_out, device=device, dtype=dtype), - d=torch.tensor(100.0, device=device, dtype=dtype), - ).encode_linear(B=B, n_out=n_out, device=device, dtype=dtype) - layers = [ - Layer( - id=0, kind=LayerKind.INPUT.value, - params={"shape": (B, n_in), "dtype": str(dtype)}, - in_vars=[], out_vars=in_v, - ), - Layer( - id=1, kind=LayerKind.INPUT_SPEC.value, - params={"kind": "BOX", "lb": lb_in, "ub": ub_in}, - in_vars=in_v, out_vars=in_v, - ), - Layer( - id=2, kind=LayerKind.DENSE.value, - params={ - "weight": W, "in_features": n_in, "out_features": n_out, - "weight_pos": W.clamp(min=0), "weight_neg": W.clamp(max=0), - "bias": b, "input_shape": (n_in,), - }, - in_vars=in_v, out_vars=out_v, - ), - Layer( - id=3, kind=LayerKind.ASSERT.value, - params=spec, in_vars=out_v, out_vars=out_v, - ), - ] - preds = {0: [], 1: [0], 2: [1], 3: [2]} - succs = {0: [1], 1: [2], 2: [3], 3: []} - return Net(layers=layers, preds=preds, succs=succs) - - -def _test_export_dense_uniform(): # pragma: no cover - """m_eq must equal W.shape[0] (one eq per output) for any N.""" - for B in (1, 4, 8): - n_in, n_out = 4, 3 - W = torch.tensor( - [[1.0, 2.0, -1.0, 0.5], - [0.0, 1.0, 1.0, 1.0], - [-0.5, 0.0, 2.0, 1.0]], - ) - b = torch.tensor([0.1, -0.2, 0.3]) - lb_in = torch.full((B, n_in), -1.0) - ub_in = torch.full((B, n_in), 1.0) - net = _build_dense_test_net(B, n_in, n_out, W, b, lb_in, ub_in) - globalC = _run_analyze(net, lb_in, ub_in) - bp = export_to_batch_problem( - net, globalC, net.layers[-1], - Bounds(lb=lb_in, ub=ub_in), - ) - assert bp.m_eq == n_out, ( - f"B={B}: expected m_eq={n_out}, got {bp.m_eq}" - ) - assert bp.N == B - A_dense = _dense_block_rows( - bp.A_eq_blockdiag, bp.N, bp.m_eq, bp.nvars - ) - for nb in range(B): - for i in range(n_out): - row = A_dense[nb, i] - rhs = float(bp.b_eq[nb, i]) - assert float(row[n_in + i]) == 1.0, ( - f"B={B} n={nb}: coeff on y_{i} != 1" - ) - for j in range(n_in): - assert abs(float(row[j]) - (-float(W[i, j]))) < 1e-9, ( - f"B={B} n={nb}: coeff on x_{j} != -W[{i},{j}]" - ) - assert abs(rhs - float(b[i])) < 1e-9 - - -def _build_top1_test_net(B, K, y_true, lb_in, ub_in, W, bias): # pragma: no cover - from act.back_end.core import Layer, Net - from act.back_end.layer_schema import LayerKind - from act.front_end.specs import OutputSpec, OutKind - - n_in = lb_in.shape[1] - device = lb_in.device - dtype = lb_in.dtype - in_v = list(range(n_in)) - out_v = list(range(n_in, n_in + K)) - spec = OutputSpec( - kind=OutKind.TOP1_ROBUST, - y_true=y_true, - ).encode_linear(B=B, n_out=K, device=device, dtype=dtype) - layers = [ - Layer( - id=0, kind=LayerKind.INPUT.value, - params={"shape": (B, n_in), "dtype": str(dtype)}, - in_vars=[], out_vars=in_v, - ), - Layer( - id=1, kind=LayerKind.INPUT_SPEC.value, - params={"kind": "BOX", "lb": lb_in, "ub": ub_in}, - in_vars=in_v, out_vars=in_v, - ), - Layer( - id=2, kind=LayerKind.DENSE.value, - params={ - "weight": W, "in_features": n_in, "out_features": K, - "weight_pos": W.clamp(min=0), "weight_neg": W.clamp(max=0), - "bias": bias, "input_shape": (n_in,), - }, - in_vars=in_v, out_vars=out_v, - ), - Layer( - id=3, kind=LayerKind.ASSERT.value, - params=spec, in_vars=out_v, out_vars=out_v, - ), - ] - preds = {0: [], 1: [0], 2: [1], 3: [2]} - succs = {0: [1], 1: [2], 2: [3], 3: []} - return Net(layers=layers, preds=preds, succs=succs) - - -def _test_export_top1_robust_batched(): # pragma: no cover - """K+1 rows per instance with slack at slot nvars_net.""" - torch.manual_seed(7) - for trial in range(4): - B = int(torch.randint(1, 6, (1,)).item()) - K = int(torch.randint(2, 6, (1,)).item()) - n_in = 3 - y_true = torch.randint(0, K, (B,), dtype=torch.long) - lb_in = torch.full((B, n_in), -0.5) - ub_in = torch.full((B, n_in), 0.5) - W = torch.randn(K, n_in) * 0.1 - bias = torch.zeros(K) - net = _build_top1_test_net(B, K, y_true, lb_in, ub_in, W, bias) - globalC = _run_analyze(net, lb_in, ub_in) - bp = export_to_batch_problem( - net, globalC, net.layers[-1], - Bounds(lb=lb_in, ub=ub_in), - ) - assert bp.nvars == n_in + K + 1, ( - f"trial {trial}: expected nvars=n_in+K+1={n_in + K + 1}, " - f"got {bp.nvars}" - ) - slack_id = n_in + K - for nb in range(B): - assert float(bp.lb[nb, slack_id]) == 0.0, ( - f"trial {trial} n={nb}: slack lb should be 0" - ) - assert bp.m_eq == K, f"trial {trial}: dense m_eq={bp.m_eq} != K={K}" - assert bp.m_le >= K + 1, ( - f"trial {trial}: top1 m_le={bp.m_le} should be >= K+1={K + 1}" - ) - - -def _build_simple_dense_relu_dense_top1_net( - B, n_in, n_hidden, K, y_true, W1, b1, W2, b2, lb_in, ub_in, -): - from act.back_end.core import Layer, Net - from act.back_end.layer_schema import LayerKind - from act.front_end.specs import OutputSpec, OutKind - - device = lb_in.device - dtype = lb_in.dtype - in_v = list(range(n_in)) - h_pre = list(range(n_in, n_in + n_hidden)) - h_post = list(range(n_in + n_hidden, n_in + 2 * n_hidden)) - out_v = list( - range(n_in + 2 * n_hidden, n_in + 2 * n_hidden + K) - ) - spec = OutputSpec( - kind=OutKind.TOP1_ROBUST, y_true=y_true, - ).encode_linear(B=B, n_out=K, device=device, dtype=dtype) - layers = [ - Layer( - id=0, kind=LayerKind.INPUT.value, - params={"shape": (B, n_in), "dtype": str(dtype)}, - in_vars=[], out_vars=in_v, - ), - Layer( - id=1, kind=LayerKind.INPUT_SPEC.value, - params={"kind": "BOX", "lb": lb_in, "ub": ub_in}, - in_vars=in_v, out_vars=in_v, - ), - Layer( - id=2, kind=LayerKind.DENSE.value, - params={ - "weight": W1, "in_features": n_in, "out_features": n_hidden, - "weight_pos": W1.clamp(min=0), "weight_neg": W1.clamp(max=0), - "bias": b1, "input_shape": (n_in,), - }, - in_vars=in_v, out_vars=h_pre, - ), - Layer( - id=3, kind=LayerKind.RELU.value, - params={}, in_vars=h_pre, out_vars=h_post, - ), - Layer( - id=4, kind=LayerKind.DENSE.value, - params={ - "weight": W2, "in_features": n_hidden, "out_features": K, - "weight_pos": W2.clamp(min=0), "weight_neg": W2.clamp(max=0), - "bias": b2, "input_shape": (n_hidden,), - }, - in_vars=h_post, out_vars=out_v, - ), - Layer( - id=5, kind=LayerKind.ASSERT.value, - params=spec, in_vars=out_v, out_vars=out_v, - ), - ] - preds = {0: [], 1: [0], 2: [1], 3: [2], 4: [3], 5: [4]} - succs = {0: [1], 1: [2], 2: [3], 3: [4], 4: [5], 5: []} - return Net(layers=layers, preds=preds, succs=succs) - - - - - -def _test_export_n1_batch_problem_self_consistent(): # pragma: no cover - torch.manual_seed(123) - B = 1 - n_in, n_hidden, K = 4, 6, 3 - y_true = torch.tensor([1], dtype=torch.long) - W1 = torch.randn(n_hidden, n_in) * 0.5 - b1 = torch.randn(n_hidden) * 0.1 - W2 = torch.randn(K, n_hidden) * 0.5 - b2 = torch.randn(K) * 0.1 - lb_in = torch.full((B, n_in), -1.0) - ub_in = torch.full((B, n_in), 1.0) - net = _build_simple_dense_relu_dense_top1_net( - B, n_in, n_hidden, K, y_true, W1, b1, W2, b2, lb_in, ub_in, - ) - globalC = _run_analyze(net, lb_in, ub_in) - bp = export_to_batch_problem( - net, globalC, net.layers[-1], Bounds(lb=lb_in, ub=ub_in), - ) - - assert bp.N == 1 - assert bp.nvars >= max(max(con.var_ids) for con in globalC) + 1 - assert bp.lb.shape == bp.ub.shape == (1, bp.nvars) - assert bp.A_eq_blockdiag.shape == (bp.m_eq, bp.nvars) - assert bp.A_le_blockdiag.shape == (bp.m_le, bp.nvars) - assert bp.m_eq > 0 and bp.m_le > 0 - - -def _build_conv2d_test_net( # pragma: no cover - B, C_in, H_in, W_in, C_out, K_h, K_w, stride, padding, - weight, bias_flat, lb_in, ub_in, -): - from act.back_end.core import Layer, Net - from act.back_end.layer_schema import LayerKind - from act.front_end.specs import OutputSpec, OutKind - - device = lb_in.device - dtype = lb_in.dtype - sh, sw = stride - ph, pw = padding - H_out = (H_in + 2 * ph - (K_h - 1) - 1) // sh + 1 - W_out = (W_in + 2 * pw - (K_w - 1) - 1) // sw + 1 - n_in_flat = C_in * H_in * W_in - n_out_flat = C_out * H_out * W_out - in_v = list(range(n_in_flat)) - out_v = list(range(n_in_flat, n_in_flat + n_out_flat)) - spec_layer = OutputSpec( - kind=OutKind.LINEAR_LE, - c=torch.zeros(n_out_flat, device=device, dtype=dtype), - d=torch.tensor(1.0, device=device, dtype=dtype), - ).encode_linear(B=B, n_out=n_out_flat, device=device, dtype=dtype) - layers = [ - Layer( - id=0, kind=LayerKind.INPUT.value, - params={"shape": (B, C_in, H_in, W_in), "dtype": str(dtype)}, - in_vars=[], out_vars=in_v, - ), - Layer( - id=1, kind=LayerKind.INPUT_SPEC.value, - params={ - "kind": "BOX", - "lb": lb_in.reshape(B, -1), - "ub": ub_in.reshape(B, -1), - }, - in_vars=in_v, out_vars=in_v, - ), - Layer( - id=2, kind=LayerKind.CONV2D.value, - params={ - "weight": weight, - "in_channels": C_in, "out_channels": C_out, - "kernel_size": K_h if K_h == K_w else (K_h, K_w), - "stride": stride, "padding": padding, - "dilation": 1, "groups": 1, - "input_shape": (1, C_in, H_in, W_in), - "output_shape": (1, C_out, H_out, W_out), - }, - in_vars=in_v, out_vars=out_v, - ), - Layer( - id=3, kind=LayerKind.ASSERT.value, - params=spec_layer, in_vars=out_v, out_vars=out_v, - ), - ] - preds = {0: [], 1: [0], 2: [1], 3: [2]} - succs = {0: [1], 1: [2], 2: [3], 3: []} - return Net(layers=layers, preds=preds, succs=succs), (H_out, W_out) - - -def _test_export_conv2d_n1_parity_vs_torch(): # pragma: no cover - """Conv2D LP matrix matches torch.nn.functional.conv2d on a random input.""" - torch.manual_seed(2025) - B = 1 - C_in, H_in, W_in = 3, 4, 4 - C_out, K_h, K_w = 2, 3, 3 - stride = (1, 1) - padding = (1, 1) - weight = torch.randn(C_out, C_in, K_h, K_w, dtype=torch.float64) * 0.5 - lb_in = torch.full((B, C_in, H_in, W_in), -1.0, dtype=torch.float64) - ub_in = torch.full((B, C_in, H_in, W_in), 1.0, dtype=torch.float64) - bias_flat = torch.zeros(C_out * H_in * W_in, dtype=torch.float64) - net, (H_out, W_out) = _build_conv2d_test_net( - B, C_in, H_in, W_in, C_out, K_h, K_w, stride, padding, - weight, bias_flat, lb_in, ub_in, - ) - globalC = _run_analyze( - net, lb_in.reshape(B, -1), ub_in.reshape(B, -1) - ) - bp = export_to_batch_problem( - net, globalC, net.layers[-1], - Bounds(lb=lb_in.reshape(B, -1), ub=ub_in.reshape(B, -1)), - ) - - n_in_flat = C_in * H_in * W_in - n_out_flat = C_out * H_out * W_out - assert bp.m_eq == n_out_flat, ( - f"expected m_eq={n_out_flat}, got {bp.m_eq}" - ) - - A_dense = _dense_block_rows( - bp.A_eq_blockdiag, bp.N, bp.m_eq, bp.nvars - ) - rows = A_dense[0] - rhs = bp.b_eq[0] - - x_sample = torch.randn(B, C_in, H_in, W_in, dtype=torch.float64) - y_ref = torch.nn.functional.conv2d( - x_sample, weight, bias=None, stride=stride, padding=padding, - ) - - x_flat = x_sample.reshape(B, n_in_flat) - y_flat_ref = y_ref.reshape(B, n_out_flat) - - for r in range(n_out_flat): - row = rows[r] - coef_on_y = float(row[n_in_flat + r]) - assert coef_on_y == 1.0, ( - f"row {r}: coef on y_{r} = {coef_on_y} (expected 1.0)" - ) - lhs = ( - float(y_flat_ref[0, r]) - + float((row[:n_in_flat] * x_flat[0]).sum()) - ) - assert abs(lhs - float(rhs[r])) < 1e-9, ( - f"row {r}: lhs={lhs} != rhs={float(rhs[r])} " - f"(y_ref + (-W flat) . x diff)" - ) - - -def _test_export_conv2d_batched_N_4(): # pragma: no cover - """B=4: each LP instance gets its own input bounds; W is shared (broadcast).""" - torch.manual_seed(2026) - B = 4 - C_in, H_in, W_in = 1, 4, 4 - C_out, K_h, K_w = 3, 3, 3 - stride = (1, 1) - padding = (1, 1) - weight = torch.randn(C_out, C_in, K_h, K_w, dtype=torch.float64) * 0.4 - lb_in = torch.randn(B, C_in, H_in, W_in, dtype=torch.float64) - 0.5 - ub_in = lb_in + torch.rand(B, C_in, H_in, W_in, dtype=torch.float64) + 0.5 - bias_flat = torch.zeros(C_out * H_in * W_in, dtype=torch.float64) - net, (H_out, W_out) = _build_conv2d_test_net( - B, C_in, H_in, W_in, C_out, K_h, K_w, stride, padding, - weight, bias_flat, lb_in, ub_in, - ) - globalC = _run_analyze( - net, lb_in.reshape(B, -1), ub_in.reshape(B, -1) - ) - bp = export_to_batch_problem( - net, globalC, net.layers[-1], - Bounds(lb=lb_in.reshape(B, -1), ub=ub_in.reshape(B, -1)), - ) - assert bp.N == B - n_out_flat = C_out * H_out * W_out - assert bp.m_eq == n_out_flat - A_dense = _dense_block_rows( - bp.A_eq_blockdiag, bp.N, bp.m_eq, bp.nvars - ) - for nb in range(1, B): - diff = (A_dense[0] - A_dense[nb]).abs().max().item() - assert diff < 1e-12, ( - f"conv2d coefficients must be uniform across N " - f"(W shared); instance {nb} differs by {diff}" - ) - n_in_flat = C_in * H_in * W_in - for nb in range(B): - for k in range(n_in_flat): - v = float(bp.lb[nb, k]) - expected = float(lb_in.reshape(B, n_in_flat)[nb, k]) - assert abs(v - expected) < 1e-12 - - -def _test_export_conv2d_stride2_pad0(): # pragma: no cover - """Stride=2, pad=0: shrinking spatial output, dropped kernel taps at edges.""" - torch.manual_seed(2027) - B = 1 - C_in, H_in, W_in = 1, 4, 4 - C_out, K_h, K_w = 1, 3, 3 - stride = (2, 2) - padding = (0, 0) - weight = torch.ones(C_out, C_in, K_h, K_w, dtype=torch.float64) - lb_in = torch.full((B, C_in, H_in, W_in), -1.0, dtype=torch.float64) - ub_in = torch.full((B, C_in, H_in, W_in), 1.0, dtype=torch.float64) - bias_flat = torch.zeros(C_out * 1 * 1, dtype=torch.float64) - net, (H_out, W_out) = _build_conv2d_test_net( - B, C_in, H_in, W_in, C_out, K_h, K_w, stride, padding, - weight, bias_flat, lb_in, ub_in, - ) - assert (H_out, W_out) == (1, 1), ( - f"expected 1x1 output for 4x4 input k=3 s=2 p=0; got {H_out}x{W_out}" - ) - globalC = _run_analyze( - net, lb_in.reshape(B, -1), ub_in.reshape(B, -1) - ) - bp = export_to_batch_problem( - net, globalC, net.layers[-1], - Bounds(lb=lb_in.reshape(B, -1), ub=ub_in.reshape(B, -1)), - ) - n_in_flat = C_in * H_in * W_in - n_out_flat = C_out * H_out * W_out - assert bp.m_eq == n_out_flat - A_dense = _dense_block_rows( - bp.A_eq_blockdiag, bp.N, bp.m_eq, bp.nvars - ) - row = A_dense[0, 0] - coef_y = float(row[n_in_flat]) - assert coef_y == 1.0 - x_coefs = row[:n_in_flat].reshape(C_in, H_in, W_in) - receptive = x_coefs[0, 0:3, 0:3] - assert torch.allclose( - receptive, -torch.ones_like(receptive) - ), f"top-left 3x3 receptive coefs should be -1; got {receptive}" - untouched_mask = torch.ones((H_in, W_in), dtype=torch.bool) - untouched_mask[0:3, 0:3] = False - untouched = x_coefs[0][untouched_mask] - assert untouched.abs().max().item() < 1e-12, ( - f"positions outside 3x3 receptive field must have coefficient 0; " - f"got max abs {untouched.abs().max().item()}" - ) - - -def _build_unary_layer_test_net(B, n, kind, params, lb, ub): # pragma: no cover - from act.back_end.core import Layer, Net - from act.back_end.layer_schema import LayerKind - from act.front_end.specs import OutputSpec, OutKind - - device = lb.device - dtype = lb.dtype - in_v = list(range(n)) - out_v = list(range(n, 2 * n)) - spec = OutputSpec( - kind=OutKind.LINEAR_LE, - c=torch.zeros(n, device=device, dtype=dtype), - d=torch.tensor(-1.0e6, device=device, dtype=dtype), - ).encode_linear(B=B, n_out=n, device=device, dtype=dtype) - layers = [ - Layer( - id=0, kind=LayerKind.INPUT.value, - params={"shape": (B, n), "dtype": str(dtype)}, - in_vars=[], out_vars=in_v, - ), - Layer( - id=1, kind=LayerKind.INPUT_SPEC.value, - params={"kind": "BOX", "lb": lb, "ub": ub}, - in_vars=in_v, out_vars=in_v, - ), - Layer(id=2, kind=kind, params=params, in_vars=in_v, out_vars=out_v), - Layer(id=3, kind=LayerKind.ASSERT.value, params=spec, in_vars=out_v, out_vars=out_v), - ] - preds = {0: [], 1: [0], 2: [1], 3: [2]} - succs = {0: [1], 1: [2], 2: [3], 3: []} - return Net(layers=layers, preds=preds, succs=succs) - - -def _export_unary_layer(B, n, kind, params, lb, ub): - net = _build_unary_layer_test_net(B, n, kind, params, lb, ub) - globalC = _run_analyze(net, lb, ub) - bp = export_to_batch_problem(net, globalC, net.layers[-1], Bounds(lb=lb, ub=ub)) - return net, bp - - -def _assert_layer_rows_hold(bp, x, y): - A_le = _dense_block_rows(bp.A_le_blockdiag, bp.N, bp.m_le, bp.nvars) - A_eq = _dense_block_rows(bp.A_eq_blockdiag, bp.N, bp.m_eq, bp.nvars) - n = x.shape[1] - vals = torch.cat([x, y], dim=1).to(dtype=bp.lb.dtype) - for b in range(bp.N): - if bp.m_eq: - eq_lhs = A_eq[b].matmul(vals[b]) - assert torch.allclose(eq_lhs, bp.b_eq[b], atol=1e-7, rtol=1e-7), ( - f"eq rows failed: lhs={eq_lhs} rhs={bp.b_eq[b]}" - ) - if bp.m_le: - le_lhs = A_le[b].matmul(vals[b]) - assert bool(torch.all(le_lhs <= bp.b_le[b] + 1e-6)), ( - f"le rows failed: max_violation={(le_lhs - bp.b_le[b]).max()}" - ) - assert vals.shape[1] == 2 * n - - -def _test_export_flatten_identity(): # pragma: no cover - from act.back_end.layer_schema import LayerKind - B, n = 2, 6 - lb = torch.full((B, n), -1.0, dtype=torch.float64) - ub = torch.full((B, n), 2.0, dtype=torch.float64) - _net, bp = _export_unary_layer( - B, n, LayerKind.FLATTEN.value, - {"input_shape": (B, 2, 3), "output_shape": (B, 6)}, lb, ub, - ) - assert bp.m_eq == n - x = torch.randn(B, n, dtype=torch.float64) - _assert_layer_rows_hold(bp, x, x) - - -def _test_export_sigmoid_relaxation(): # pragma: no cover - from act.back_end.layer_schema import LayerKind - B, n = 2, 4 - lb = torch.tensor([[-3.0, -1.0, 0.2, -2.0], [-0.5, 0.0, 1.0, -4.0]], dtype=torch.float64) - ub = torch.tensor([[3.0, 0.5, 2.0, -0.5], [0.5, 1.5, 4.0, 2.0]], dtype=torch.float64) - _net, bp = _export_unary_layer(B, n, LayerKind.SIGMOID.value, {}, lb, ub) - assert bp.m_le >= 4 * n - x = 0.5 * (lb + ub) - y = torch.sigmoid(x) - _assert_layer_rows_hold(bp, x, y) - - -def _test_export_relu6_hull_relaxation(): # pragma: no cover - from act.back_end.layer_schema import LayerKind - B, n = 1, 5 - lb = torch.tensor([[-2.0, -0.1, 0.5, 5.0, 7.0]], dtype=torch.float64) - ub = torch.tensor([[1.0, 2.0, 3.0, 8.0, 9.0]], dtype=torch.float64) - _net, bp = _export_unary_layer(B, n, LayerKind.RELU6.value, {}, lb, ub) - assert bp.m_le > 2 * n - x = torch.tensor([[-1.0, 1.0, 2.0, 6.0, 8.0]], dtype=torch.float64) - _assert_layer_rows_hold(bp, x, torch.clamp(x, min=0.0, max=6.0)) - - -def _test_export_hardsigmoid_hull_relaxation(): # pragma: no cover - from act.back_end.layer_schema import LayerKind - B, n = 1, 4 - lb = torch.full((B, n), -4.0, dtype=torch.float64) - ub = torch.full((B, n), 4.0, dtype=torch.float64) - params = {"alpha": 1.0 / 6.0, "beta": 0.5} - _net, bp = _export_unary_layer(B, n, LayerKind.HARDSIGMOID.value, params, lb, ub) - assert bp.m_le > 2 * n - x = torch.tensor([[-4.0, -1.0, 1.0, 4.0]], dtype=torch.float64) - y = torch.clamp(x / 6.0 + 0.5, min=0.0, max=1.0) - _assert_layer_rows_hold(bp, x, y) - - -def _test_export_hardtanh_hull_relaxation(): # pragma: no cover - from act.back_end.layer_schema import LayerKind - B, n = 1, 4 - lb = torch.full((B, n), -2.0, dtype=torch.float64) - ub = torch.full((B, n), 2.0, dtype=torch.float64) - params = {"min_val": -1.0, "max_val": 1.0} - _net, bp = _export_unary_layer(B, n, LayerKind.HARDTANH.value, params, lb, ub) - assert bp.m_le > 2 * n - x = torch.tensor([[-2.0, -0.5, 0.5, 2.0]], dtype=torch.float64) - _assert_layer_rows_hold(bp, x, torch.clamp(x, min=-1.0, max=1.0)) - - -def _test_export_mask_add_equality(): # pragma: no cover - from act.back_end.layer_schema import LayerKind - B, n = 1, 4 - lb = torch.full((B, n), -1.0, dtype=torch.float64) - ub = torch.full((B, n), 1.0, dtype=torch.float64) - mask = torch.tensor([0.0, -10000.0, 0.0, -10000.0], dtype=torch.float64) - _net, bp = _export_unary_layer(B, n, LayerKind.MASK_ADD.value, {"M": mask}, lb, ub) - x = torch.tensor([[0.1, 0.2, -0.3, 0.4]], dtype=torch.float64) - _assert_layer_rows_hold(bp, x, x + mask.unsqueeze(0)) - - -def _test_export_power_p2_relu_square_hull(): # pragma: no cover - from act.back_end.layer_schema import LayerKind - B, n = 1, 4 - lb = torch.full((B, n), -1.0, dtype=torch.float64) - ub = torch.full((B, n), 2.0, dtype=torch.float64) - _net, bp = _export_unary_layer(B, n, LayerKind.POWER.value, {"p": 2.0}, lb, ub) - x = torch.tensor([[-1.0, 0.0, 1.0, 2.0]], dtype=torch.float64) - _assert_layer_rows_hold(bp, x, torch.clamp(x, min=0.0).pow(2.0)) - - -def _test_export_square_hull(): # pragma: no cover - from act.back_end.layer_schema import LayerKind - B, n = 1, 4 - lb = torch.full((B, n), -2.0, dtype=torch.float64) - ub = torch.full((B, n), 1.5, dtype=torch.float64) - _net, bp = _export_unary_layer(B, n, LayerKind.SQUARE.value, {}, lb, ub) - x = torch.tensor([[-2.0, -0.5, 0.5, 1.5]], dtype=torch.float64) - _assert_layer_rows_hold(bp, x, x * x) - - -def _test_export_layernorm_box_relaxation(): # pragma: no cover - from act.back_end.layer_schema import LayerKind - B, n = 1, 8 - lb = torch.full((B, n), -1.0, dtype=torch.float64) - ub = torch.full((B, n), 1.0, dtype=torch.float64) - gamma = torch.ones(n, dtype=torch.float64) - beta = torch.zeros(n, dtype=torch.float64) - eps = 1e-5 - params = {"gamma": gamma, "beta": beta, "eps": eps} - _net, bp = _export_unary_layer(B, n, LayerKind.LAYERNORM.value, params, lb, ub) - x = torch.linspace(-0.7, 0.7, n, dtype=torch.float64).unsqueeze(0) - y = torch.nn.functional.layer_norm(x, (n,), gamma, beta, eps) - _assert_layer_rows_hold(bp, x, y) - - -_BATCHED_TESTS = [ # pragma: no cover - _test_export_relu_canonical, - _test_export_lrelu_canonical, - _test_export_tanh_canonical_5_cases, - _test_export_dense_uniform, - _test_export_top1_robust_batched, - _test_export_n1_batch_problem_self_consistent, - _test_export_conv2d_n1_parity_vs_torch, - _test_export_conv2d_batched_N_4, - _test_export_conv2d_stride2_pad0, - _test_export_flatten_identity, - _test_export_sigmoid_relaxation, - _test_export_relu6_hull_relaxation, - _test_export_hardsigmoid_hull_relaxation, - _test_export_hardtanh_hull_relaxation, - _test_export_mask_add_equality, - _test_export_power_p2_relu_square_hull, - _test_export_square_hull, - _test_export_layernorm_box_relaxation, -] - - -def _run_batched_tests() -> int: - passed = failed = 0 - for fn in _BATCHED_TESTS: - try: - fn() - passed += 1 - print(f" PASS {fn.__name__}") - except Exception as e: - failed += 1 - print(f" FAIL {fn.__name__}: {type(e).__name__}: {e}") - import traceback - traceback.print_exc() - print(f"\n{passed} passed, {failed} failed") - return 1 if failed else 0 - - -if __name__ == "__main__": - import sys - from act.util.device_manager import initialize_device - initialize_device("cpu", "float64") - print("Running cons_exportor batched self-tests\n") - sys.exit(_run_batched_tests()) diff --git a/act/back_end/verifier.py b/act/back_end/verifier.py index f43c7dd26..6756f8e88 100644 --- a/act/back_end/verifier.py +++ b/act/back_end/verifier.py @@ -777,1377 +777,3 @@ def _unbatch(val: Any) -> Any: VerifyResult(VerifyStatus.UNKNOWN, metadata=meta) ) return (results, after) if collect_facts else results - - -#===---------------------------------------------------------------------===# -# Self-contained ASSERT-encoding + verify_once test battery. -# Run via: python -m act.back_end.verifier -#===---------------------------------------------------------------------===# - - - - - -def _make_dense_net_box_test( # pragma: no cover - B: int, - n_in: int, - n_out: int, - weight: torch.Tensor, - bias: torch.Tensor, - lb_in: torch.Tensor, - ub_in: torch.Tensor, - assert_params: Dict[str, Any], -): - # assert_params is high-level (kind + y_true/margin/c/d/lb/ub); lift to - # encoded form via OutputSpec.encode_linear to match the production - # OutputSpecLayer.to_act_layers path. - from act.back_end.core import Layer, Net - from act.front_end.specs import OutputSpec - - in_v = list(range(n_in)) - out_v = list(range(n_in, n_in + n_out)) - - spec_kwargs = { - k: assert_params[k] for k in ("y_true", "margin", "c", "d", "lb", "ub") - if k in assert_params - } - out_spec = OutputSpec(kind=assert_params["kind"], **spec_kwargs) - encoded = out_spec.encode_linear( - B=B, n_out=n_out, device=weight.device, dtype=weight.dtype, - ) - - layers = [ - Layer( - id=0, - kind=LayerKind.INPUT.value, - params={"shape": (B, n_in), "dtype": str(weight.dtype)}, - in_vars=[], - out_vars=in_v, - ), - Layer( - id=1, - kind=LayerKind.INPUT_SPEC.value, - params={"kind": "BOX", "lb": lb_in, "ub": ub_in}, - in_vars=in_v, - out_vars=in_v, - ), - Layer( - id=2, - kind=LayerKind.DENSE.value, - params={ - "weight": weight, - "in_features": n_in, - "out_features": n_out, - "weight_pos": weight.clamp(min=0), - "weight_neg": weight.clamp(max=0), - "bias": bias, - "input_shape": (n_in,), - }, - in_vars=in_v, - out_vars=out_v, - ), - Layer( - id=3, - kind=LayerKind.ASSERT.value, - params=encoded, - in_vars=out_v, - out_vars=out_v, - ), - ] - preds = {0: [], 1: [0], 2: [1], 3: [2]} - succs = {0: [1], 1: [2], 2: [3], 3: []} - return Net(layers=layers, preds=preds, succs=succs) - - -def _make_attn_dual_planar_net( # pragma: no cover - B: int, L: int, D: int, H: int, - center: torch.Tensor, eps: float, - assert_d: float, - *, - mask: "torch.Tensor | None" = None, - clamp_alpha: bool = False, -) -> "tuple[Net, dict[str, Any]]": - """Build INPUT -> Q/K DENSE projections -> ATT_SCORES(dual_planar) -> ASSERT. - - Exercises the real ``analyze()`` -> ``tf_att_scores`` -> - ``att_scores_dual_planar``/``LinearBounds`` -> ``cons_exportor``'s - ``att_dual_planar:`` export path end-to-end, not direct unit calls into - ``interval_tf/tf_attention.py``. The ``q_lb``/``k_lb`` baked onto the - ATT_SCORES layer are seeded from the same box as INPUT_SPEC and pushed - through the same ``Wq``/``Wk`` as the DENSE Q/K layers, so the result is - a faithful (not synthetic) attention-score relaxation of this network. - """ - from act.back_end.core import Layer - from act.back_end.interval_tf.tf_attention import LinearBounds - from act.front_end.specs import OutputSpec - - n_in = L * D - in_v = list(range(n_in)) - lb_in = center - eps - ub_in = center + eps - - Wq = torch.randn(H, D, dtype=center.dtype, generator=torch.Generator().manual_seed(11)) * 0.3 - Wk = torch.randn(H, D, dtype=center.dtype, generator=torch.Generator().manual_seed(12)) * 0.3 - - eye = torch.eye(D, dtype=center.dtype) - center3 = center.reshape(B, L, D) - radius3 = torch.full((B, L, D), eps, dtype=center.dtype) - seed_w = radius3.unsqueeze(-1) * eye - emb_lb = LinearBounds( - seed_w, seed_w.clone(), center3.clone(), center3.clone(), - p=float("inf"), eps=1.0, perturbed_words=1, - ) - q_lb = emb_lb.matmul(Wq) - k_lb = emb_lb.matmul(Wk) - - q_vars = list(range(n_in, n_in + L * H)) - k_vars = list(range(n_in + L * H, n_in + 2 * L * H)) - score_vars = list(range(n_in + 2 * L * H, n_in + 2 * L * H + L * L)) - - def block_diag_proj(W: torch.Tensor) -> torch.Tensor: - full = torch.zeros(L * H, n_in, dtype=center.dtype) - for t in range(L): - full[t * H:(t + 1) * H, t * D:(t + 1) * D] = W - return full - - Wq_full, Wk_full = block_diag_proj(Wq), block_diag_proj(Wk) - - layers = [ - Layer( - id=0, kind=LayerKind.INPUT.value, - params={"shape": (B, n_in), "dtype": str(center.dtype)}, - in_vars=[], out_vars=in_v, - ), - Layer( - id=1, kind=LayerKind.INPUT_SPEC.value, - params={"kind": "BOX", "lb": lb_in, "ub": ub_in}, - in_vars=in_v, out_vars=in_v, - ), - Layer( - id=2, kind=LayerKind.DENSE.value, - params={ - "weight": Wq_full, "in_features": n_in, "out_features": L * H, - "weight_pos": Wq_full.clamp(min=0), "weight_neg": Wq_full.clamp(max=0), - "bias": torch.zeros(L * H, dtype=center.dtype), "input_shape": (n_in,), - }, - in_vars=in_v, out_vars=q_vars, - ), - Layer( - id=3, kind=LayerKind.DENSE.value, - params={ - "weight": Wk_full, "in_features": n_in, "out_features": L * H, - "weight_pos": Wk_full.clamp(min=0), "weight_neg": Wk_full.clamp(max=0), - "bias": torch.zeros(L * H, dtype=center.dtype), "input_shape": (n_in,), - }, - in_vars=in_v, out_vars=k_vars, - ), - Layer( - id=4, kind=LayerKind.ATT_SCORES.value, - params={ - "dk": float(H) ** 0.5, "q_vars": tuple(q_vars), "k_vars": tuple(k_vars), - "q_src": 2, "k_src": 3, - "attn_mode": "dual_planar", "q_lb": q_lb, "k_lb": k_lb, "head_size": H, - "mask": mask, "clamp_alpha": clamp_alpha, - }, - in_vars=q_vars + k_vars, out_vars=score_vars, - ), - ] - n_scores = len(score_vars) - out_spec = OutputSpec( - kind="LINEAR_LE", c=torch.ones(n_scores, dtype=center.dtype), - d=torch.tensor(assert_d, dtype=center.dtype), - ) - encoded = out_spec.encode_linear(B=B, n_out=n_scores, device=center.device, dtype=center.dtype) - layers.append( - Layer(id=5, kind=LayerKind.ASSERT.value, params=encoded, in_vars=score_vars, out_vars=score_vars) - ) - - preds = {0: [], 1: [0], 2: [1], 3: [1], 4: [2, 3], 5: [4]} - succs = {0: [1], 1: [2, 3], 2: [4], 3: [4], 4: [5], 5: []} - net = Net(layers=layers, preds=preds, succs=succs) - info: "dict[str, Any]" = { - "Wq": Wq, "Wk": Wk, "lb_in": lb_in, "ub_in": ub_in, - "score_id": 4, "n_in": n_in, "L": L, "D": D, "H": H, - } - return net, info - - -def _test_att_scores_dual_planar_analyze_soundness() -> None: # pragma: no cover - # Real `analyze()` worklist (not a direct LinearBounds unit call): the - # propagated box for the ATT_SCORES(dual_planar) layer must bracket the - # true concrete scaled-Q.K^T value for every sampled point in the box. - from act.back_end.analyze import analyze - from act.util.device_manager import get_default_dtype - - dtype = get_default_dtype() - B, L, D, H = 1, 3, 4, 2 - torch.manual_seed(20) - center = torch.randn(B, L * D, dtype=dtype) * 0.1 - eps = 0.05 - net, info = _make_attn_dual_planar_net(B, L, D, H, center, eps, assert_d=100.0) - - entry_fact = Fact(bounds=Bounds(info["lb_in"].clone(), info["ub_in"].clone()), cons=ConSet()) - _before, after, _globalC = analyze(net, 0, entry_fact) - bounds = after[info["score_id"]].bounds - - Wq, Wk = info["Wq"], info["Wk"] - l_box, u_box = info["lb_in"], info["ub_in"] - n_samples = 100 - - def concrete_scores(x: torch.Tensor) -> torch.Tensor: - x3 = x.reshape(B, L, D) - s = (x3 @ Wq.t()) @ (x3 @ Wk.t()).transpose(-1, -2) / (H ** 0.5) - return s.reshape(B, -1) - - true_min = concrete_scores(l_box).clone() - true_max = true_min.clone() - for _ in range(n_samples): - x = l_box + torch.rand_like(l_box) * (u_box - l_box) - s = concrete_scores(x) - true_min = torch.minimum(true_min, s) - true_max = torch.maximum(true_max, s) - assert (bounds.lb <= true_min + 1e-6).all(), "analyze(): unsound lower bound on ATT_SCORES(dual_planar)" - assert (bounds.ub >= true_max - 1e-6).all(), "analyze(): unsound upper bound on ATT_SCORES(dual_planar)" - - -def _test_att_scores_dual_planar_verify_once_certified() -> None: # pragma: no cover - # End-to-end `verify_once()` through the dual-planar attention path with - # a threshold far above the true score range -> CERTIFIED. - from act.util.device_manager import get_default_dtype - from act.util.stats import VerifyStatus - - dtype = get_default_dtype() - B, L, D, H = 1, 3, 4, 2 - torch.manual_seed(21) - center = torch.randn(B, L * D, dtype=dtype) * 0.1 - eps = 0.05 - net, _info = _make_attn_dual_planar_net(B, L, D, H, center, eps, assert_d=100.0) - - results = verify_once(net) - assert len(results) == B - assert results[0].status == VerifyStatus.CERTIFIED, f"expected CERTIFIED, got {results[0].status}" - - -def _test_att_scores_dual_planar_lp_export_solve() -> None: # pragma: no cover - # End-to-end LP export+solve through `cons_exportor`'s - # `att_dual_planar:` handler (not reachable from any other test): a - # tight threshold near the true score range exercises a real SAT/UNKNOWN - # decision from TorchLPSolver, proving the export glue round-trips. - from act.back_end.solver.solver_torchlp import TorchLPSolver - from act.util.device_manager import get_default_dtype - - dtype = get_default_dtype() - B, L, D, H = 1, 3, 4, 2 - torch.manual_seed(22) - center = torch.randn(B, L * D, dtype=dtype) * 0.1 - eps = 0.05 - net, info = _make_attn_dual_planar_net(B, L, D, H, center, eps, assert_d=0.0) - - solution = setup_and_solve_batch( - net, Bounds(info["lb_in"].clone(), info["ub_in"].clone()), TorchLPSolver(), - ) - assert solution.statuses[0] in (SolveStatus.SAT, SolveStatus.UNKNOWN), ( - f"unexpected solver status {solution.statuses[0]!r}" - ) - assert tuple(solution.x.shape)[0] == B - assert float(solution.max_viol[0].item()) < 1.0, ( - f"LP residual too large: {float(solution.max_viol[0].item())}" - ) - - -def _test_att_scores_dual_planar_masked_and_clamp_alpha_soundness() -> None: # pragma: no cover - # Real `analyze()` with an additive mask and the clamp_alpha warm-start - # variant both engaged -- exercises `fuse_attention_planes`'s - # `clamp_alpha` branch and `att_scores_dual_planar`'s `mask is not None` - # branch, neither hit by the unmasked/default tests above. - from act.back_end.analyze import analyze - from act.util.device_manager import get_default_dtype - - dtype = get_default_dtype() - B, L, D, H = 1, 3, 4, 2 - torch.manual_seed(23) - center = torch.randn(B, L * D, dtype=dtype) * 0.1 - eps = 0.05 - mask = torch.zeros(B, L, L, dtype=dtype) - mask[0, 0, 1] = -5.0 - net, info = _make_attn_dual_planar_net( - B, L, D, H, center, eps, assert_d=100.0, mask=mask, clamp_alpha=True, - ) - - entry_fact = Fact(bounds=Bounds(info["lb_in"].clone(), info["ub_in"].clone()), cons=ConSet()) - _before, after, _globalC = analyze(net, 0, entry_fact) - bounds = after[info["score_id"]].bounds - - Wq, Wk = info["Wq"], info["Wk"] - l_box, u_box = info["lb_in"], info["ub_in"] - n_samples = 100 - - def concrete_masked_scores(x: torch.Tensor) -> torch.Tensor: - x3 = x.reshape(B, L, D) - s = (x3 @ Wq.t()) @ (x3 @ Wk.t()).transpose(-1, -2) / (H ** 0.5) - return (s + mask).reshape(B, -1) - - true_min = concrete_masked_scores(l_box).clone() - true_max = true_min.clone() - for _ in range(n_samples): - x = l_box + torch.rand_like(l_box) * (u_box - l_box) - s = concrete_masked_scores(x) - true_min = torch.minimum(true_min, s) - true_max = torch.maximum(true_max, s) - assert (bounds.lb <= true_min + 1e-6).all(), "masked/clamp_alpha: unsound lower bound" - assert (bounds.ub >= true_max - 1e-6).all(), "masked/clamp_alpha: unsound upper bound" - - -def _make_mini_transformer_block_net( # pragma: no cover - B: int, L: int, D: int, center: torch.Tensor, eps: float, -) -> "tuple[Net, dict[str, Any]]": - """Build a real explicit-attention block: MHA_SPLIT(Q/K/V) -> ATT_SCORES - (plain McCormick box mode, not dual_planar) -> CONCAT -> SOFTMAX -> - ATT_MIX -> MHA_JOIN -> LAYERNORM(variant='no_var', broadcast gamma). - - Mirrors the per-position/per-feature decomposition torch2act's BERT - graph builder uses (one MHA_SPLIT per query/key position, one ATT_MIX - per value feature), at the smallest size (L=2 positions) that still - requires the CONCAT-of-two-scores -> SOFTMAX -> two-feature ATT_MIX/ - MHA_JOIN path. None of these layer kinds have any other producer in - the codebase (no NetFactory family, no torch2act path on this branch), - so this is the only real (non-direct-unit-call) exercise of them. - """ - from act.back_end.core import Layer - from act.front_end.specs import OutputSpec - - n_in = L * D - in_v = list(range(n_in)) - lb_in = center - eps - ub_in = center + eps - - gen = torch.Generator().manual_seed(40) - Wq = torch.randn(D, D, dtype=center.dtype, generator=gen) * 0.3 - Wk = torch.randn(D, D, dtype=center.dtype, generator=torch.Generator().manual_seed(41)) * 0.3 - Wv = torch.randn(D, D, dtype=center.dtype, generator=torch.Generator().manual_seed(42)) * 0.3 - - layers = [ - Layer(id=0, kind=LayerKind.INPUT.value, params={"shape": (B, n_in), "dtype": str(center.dtype)}, in_vars=[], out_vars=in_v), - Layer(id=1, kind=LayerKind.INPUT_SPEC.value, params={"kind": "BOX", "lb": lb_in, "ub": ub_in}, in_vars=in_v, out_vars=in_v), - ] - preds: "dict[int, list[int]]" = {0: [], 1: [0]} - succs: "dict[int, list[int]]" = {0: [1], 1: []} - next_id = 2 - next_var = n_in - - def alloc(n: int) -> "list[int]": - nonlocal next_var - v = list(range(next_var, next_var + n)) - next_var += n - return v - - def add_layer(kind: str, params: "dict[str, Any]", in_vars: "list[int]", out_vars: "list[int]", pred_ids: "list[int]") -> int: - nonlocal next_id - layers.append(Layer(id=next_id, kind=kind, params=params, in_vars=in_vars, out_vars=out_vars)) - lid = next_id - next_id += 1 - preds[lid] = pred_ids - succs.setdefault(lid, []) - for p in pred_ids: - succs[p].append(lid) - return lid - - mha_split = lambda W, role, **extra: add_layer( # noqa: E731 - local convenience, not module API - LayerKind.MHA_SPLIT.value, - {"weight": W, "input_shape": (B, L, D), "hidden_size": D, "role": role, **extra}, - in_v, alloc(D if role != "value" else L), [1], - ) - - q_id = mha_split(Wq, "query", position=0) - q_vars = layers[q_id].out_vars - k_ids = [mha_split(Wk, "key", position=p) for p in range(L)] - k_vars_per_pos = [layers[kid].out_vars for kid in k_ids] - - score_ids = [] - score_vars_flat: "list[int]" = [] - for kid, kv in zip(k_ids, k_vars_per_pos): - sv = alloc(1) - sid = add_layer( - LayerKind.ATT_SCORES.value, - {"dk": float(D) ** 0.5, "q_vars": q_vars, "k_vars": kv, "q_src": q_id, "k_src": kid}, - q_vars + kv, sv, [q_id, kid], - ) - score_ids.append(sid) - score_vars_flat += sv - cat_vars = alloc(L) - cat_id = add_layer(LayerKind.CONCAT.value, {"concat_dim": -1}, score_vars_flat, cat_vars, score_ids) - sm_vars = alloc(L) - sm_id = add_layer(LayerKind.SOFTMAX.value, {"axis": -1}, cat_vars, sm_vars, [cat_id]) - - v_ids = [mha_split(Wv, "value", feature=f) for f in range(D)] - v_vars_per_feature = [layers[vid].out_vars for vid in v_ids] - - mix_ids = [] - mix_vars_flat: "list[int]" = [] - for vid, vv in zip(v_ids, v_vars_per_feature): - mv = alloc(1) - mid = add_layer( - LayerKind.ATT_MIX.value, - {"rowsize": L, "w_vars": sm_vars, "v_vars": vv, "w_src": sm_id, "v_src": vid}, - sm_vars + vv, mv, [sm_id, vid], - ) - mix_ids.append(mid) - mix_vars_flat += mv - join_vars = alloc(D) - join_id = add_layer(LayerKind.MHA_JOIN.value, {}, mix_vars_flat, join_vars, mix_ids) - - # gamma.numel()==1 != D forces the broadcast-repeat branch. - gamma = torch.tensor([1.5], dtype=center.dtype) - beta = torch.tensor([0.1], dtype=center.dtype) - ln_vars = alloc(D) - ln_id = add_layer( - LayerKind.LAYERNORM.value, {"gamma": gamma, "beta": beta, "variant": "no_var"}, - join_vars, ln_vars, [join_id], - ) - - out_spec = OutputSpec(kind="LINEAR_LE", c=torch.ones(D, dtype=center.dtype), d=torch.tensor(100.0, dtype=center.dtype)) - encoded = out_spec.encode_linear(B=B, n_out=D, device=center.device, dtype=center.dtype) - assert_id = add_layer(LayerKind.ASSERT.value, encoded, ln_vars, ln_vars, [ln_id]) - - net = Net(layers=layers, preds=preds, succs=succs) - info: "dict[str, Any]" = { - "Wq": Wq, "Wk": Wk, "Wv": Wv, "gamma": gamma, "beta": beta, - "lb_in": lb_in, "ub_in": ub_in, "ln_id": ln_id, "n_in": n_in, - } - return net, info - - -def _test_mini_transformer_block_analyze_soundness() -> None: # pragma: no cover - # Real `analyze()` through MHA_SPLIT -> ATT_SCORES(box) -> SOFTMAX -> - # ATT_MIX -> MHA_JOIN -> LAYERNORM(no_var, broadcast gamma): the - # propagated box must bracket the true concrete forward pass. - from act.back_end.analyze import analyze - from act.util.device_manager import get_default_dtype - - dtype = get_default_dtype() - B, L, D = 1, 2, 2 - torch.manual_seed(43) - center = torch.randn(B, L * D, dtype=dtype) * 0.1 - eps = 0.05 - net, info = _make_mini_transformer_block_net(B, L, D, center, eps) - - entry_fact = Fact(bounds=Bounds(info["lb_in"].clone(), info["ub_in"].clone()), cons=ConSet()) - _before, after, _globalC = analyze(net, 0, entry_fact) - bounds = after[info["ln_id"]].bounds - - Wq, Wk, Wv = info["Wq"], info["Wk"], info["Wv"] - gamma, beta = info["gamma"], info["beta"] - l_box, u_box = info["lb_in"], info["ub_in"] - - def concrete_forward(x: torch.Tensor) -> torch.Tensor: - x3 = x.reshape(B, L, D) - q = (x3 @ Wq.t())[:, 0, :] - scores = torch.cat( - [(q * (x3 @ Wk.t())[:, p, :]).sum(-1, keepdim=True) / (D ** 0.5) for p in range(L)], dim=-1, - ) - probs = torch.softmax(scores, dim=-1) - v_all = x3 @ Wv.t() - mixed = torch.cat([(probs * v_all[:, :, f]).sum(-1, keepdim=True) for f in range(D)], dim=-1) - centered = mixed - mixed.mean(dim=-1, keepdim=True) - return centered * gamma.repeat(D) + beta.repeat(D) - - n_samples = 150 - true_min = concrete_forward(l_box).clone() - true_max = true_min.clone() - for _ in range(n_samples): - x = l_box + torch.rand_like(l_box) * (u_box - l_box) - y = concrete_forward(x) - true_min = torch.minimum(true_min, y) - true_max = torch.maximum(true_max, y) - assert (bounds.lb <= true_min + 1e-6).all(), "mini transformer block: unsound lower bound" - assert (bounds.ub >= true_max - 1e-6).all(), "mini transformer block: unsound upper bound" - - -def _test_mha_split_edge_cases_and_mask_add() -> None: # pragma: no cover - # Direct calls to the production transfer functions for the branches - # the full-block Net above can't reach structurally: MHA_SPLIT with no - # "weight" param (passthrough), MHA_SPLIT with no "role" (flatten), and - # MASK_ADD (an unrelated single-layer op with no other test coverage). - from act.back_end.core import Layer - from act.back_end.interval_tf.tf_transformer import tf_mha_split, tf_mask_add - from act.util.device_manager import get_default_dtype - - dtype = get_default_dtype() - Bin = Bounds(torch.tensor([[-1.0, 2.0]], dtype=dtype), torch.tensor([[1.0, 3.0]], dtype=dtype)) - - passthrough = tf_mha_split(Layer(id=0, kind=LayerKind.MHA_SPLIT.value, params={}, in_vars=[0, 1], out_vars=[0, 1]), Bin) - assert torch.equal(passthrough.bounds.lb, Bin.lb) and torch.equal(passthrough.bounds.ub, Bin.ub), ( - "MHA_SPLIT with no weight must passthrough Bin unchanged" - ) - - W = torch.eye(2, dtype=dtype) - flat = tf_mha_split( - Layer( - id=1, kind=LayerKind.MHA_SPLIT.value, - params={"weight": W, "input_shape": (1, 1, 2), "hidden_size": 2}, in_vars=[0, 1], out_vars=[0, 1], - ), - Bin, - ) - assert flat.bounds.lb.shape == (1, 2) and flat.bounds.ub.shape == (1, 2), "MHA_SPLIT flatten-role output shape" - - M = torch.tensor([[0.5, -0.5]], dtype=dtype) - masked = tf_mask_add(Layer(id=2, kind=LayerKind.MASK_ADD.value, params={"M": M}, in_vars=[0, 1], out_vars=[0, 1]), Bin) - assert torch.allclose(masked.bounds.lb, Bin.lb + M) and torch.allclose(masked.bounds.ub, Bin.ub + M), ( - "MASK_ADD must shift both bounds by M" - ) - - -def _test_new_elementwise_tf_soundness() -> None: # pragma: no cover - # Direct calls to the 5 new interval_tf/tf_mlp.py transfer functions - # (ERF, SQRT, SIN, COS, QUANTIZE) -- no NetFactory family or other - # producer generates these layer kinds, so this is their only exercise. - # Each assertion samples the true concrete function over the box and - # checks the propagated interval brackets it. - from act.back_end.core import Layer - from act.back_end.interval_tf.tf_mlp import tf_erf, tf_sqrt, tf_sin, tf_cos, tf_quantize - from act.util.device_manager import get_default_dtype - - dtype = get_default_dtype() - - def assert_sound(name: str, lo: torch.Tensor, hi: torch.Tensor, l_box: torch.Tensor, u_box: torch.Tensor, fn, n: int = 150) -> None: - true_min = fn(l_box).clone() - true_max = true_min.clone() - for _ in range(n): - x = l_box + torch.rand_like(l_box) * (u_box - l_box) - y = fn(x) - true_min = torch.minimum(true_min, y) - true_max = torch.maximum(true_max, y) - assert (lo <= true_min + 1e-6).all(), f"{name}: unsound lower bound" - assert (hi >= true_max - 1e-6).all(), f"{name}: unsound upper bound" - - l_erf = torch.tensor([[-1.0, 0.5]], dtype=dtype) - u_erf = torch.tensor([[1.0, 2.0]], dtype=dtype) - erf_out = tf_erf(Layer(id=0, kind=LayerKind.ERF.value, params={}, in_vars=[0, 1], out_vars=[0, 1]), Bounds(l_erf, u_erf)) - assert_sound("erf", erf_out.bounds.lb, erf_out.bounds.ub, l_erf, u_erf, torch.erf) - - # Box straddles negative -> exercises the min-clamp in tf_sqrt. - l_sqrt = torch.tensor([[-1.0, 0.5]], dtype=dtype) - u_sqrt = torch.tensor([[2.0, 3.0]], dtype=dtype) - sqrt_out = tf_sqrt(Layer(id=1, kind=LayerKind.SQRT.value, params={}, in_vars=[0, 1], out_vars=[0, 1]), Bounds(l_sqrt, u_sqrt)) - assert_sound( - "sqrt", sqrt_out.bounds.lb, sqrt_out.bounds.ub, l_sqrt, u_sqrt, - lambda x: torch.sqrt(torch.clamp(x, min=0.0)), - ) - - # SIN/COS: narrow (no critical point), has-max, has-min, full-period(>=2pi). - sin_cases = {"narrow": (0.1, 0.5), "has_max": (1.0, 2.0), "has_min": (-2.0, -1.0), "full_period": (0.0, 7.0)} - for name, (lv, uv) in sin_cases.items(): - lb = torch.tensor([[lv]], dtype=dtype) - ub = torch.tensor([[uv]], dtype=dtype) - out = tf_sin(Layer(id=2, kind=LayerKind.SIN.value, params={}, in_vars=[0], out_vars=[0]), Bounds(lb, ub)) - assert_sound(f"sin[{name}]", out.bounds.lb, out.bounds.ub, lb, ub, torch.sin) - - cos_cases = {"narrow": (0.1, 0.5), "has_max": (-0.5, 0.5), "has_min": (2.5, 3.5), "full_period": (0.0, 7.0)} - for name, (lv, uv) in cos_cases.items(): - lb = torch.tensor([[lv]], dtype=dtype) - ub = torch.tensor([[uv]], dtype=dtype) - out = tf_cos(Layer(id=3, kind=LayerKind.COS.value, params={}, in_vars=[0], out_vars=[0]), Bounds(lb, ub)) - assert_sound(f"cos[{name}]", out.bounds.lb, out.bounds.ub, lb, ub, torch.cos) - - scale = torch.tensor([0.1], dtype=dtype) - zero_point = torch.tensor([0.0], dtype=dtype) - l_q = torch.tensor([[-1.0, 0.5]], dtype=dtype) - u_q = torch.tensor([[1.0, 2.0]], dtype=dtype) - q_out = tf_quantize( - Layer( - id=4, kind=LayerKind.QUANTIZE.value, - params={"scale": scale, "zero_point": zero_point, "qmin": -128, "qmax": 127}, - in_vars=[0, 1], out_vars=[0, 1], - ), - Bounds(l_q, u_q), - ) - - def quantize_concrete(x: torch.Tensor) -> torch.Tensor: - code = torch.clamp(torch.round(x / scale), min=-128 - zero_point, max=127 - zero_point) - return scale * code - - assert_sound("quantize", q_out.bounds.lb, q_out.bounds.ub, l_q, u_q, quantize_concrete) - - -def _make_dual_att_cores_net( # pragma: no cover - B: int, L: int, D: int, center: torch.Tensor, eps: float, assert_d: float, -) -> "tuple[Net, dict[str, Any]]": - """DENSE Q/K/V -> ATT_SCORES -> SOFTMAX -> ATT_MIX -> CONCAT -> LAYERNORM -> GELU. - - The dual attention path (dual_tf/tf_transformer.py) consumes the bilinear - cores ATT_SCORES (Q.Kt) / ATT_MIX (probs.V) with q_src/k_src/w_src/v_src - reading predecessor boxes; it stubs MHA_SPLIT/MHA_JOIN. So Q/K/V come from - DENSE (which dual supports) rather than the interval MHA_SPLIT decomposition, - giving a net the DualSolver can run end to end. Non-degenerate dims (L,D>1) - avoid the size-1 shape class. - """ - from act.back_end.core import Layer - from act.front_end.specs import OutputSpec - - n_in = L * D - in_v = list(range(n_in)) - lb_in, ub_in = center - eps, center + eps - Wq = torch.randn(D, D, dtype=center.dtype, generator=torch.Generator().manual_seed(71)) * 0.2 - Wk = torch.randn(D, D, dtype=center.dtype, generator=torch.Generator().manual_seed(72)) * 0.2 - Wv = torch.randn(D, D, dtype=center.dtype, generator=torch.Generator().manual_seed(73)) * 0.2 - - layers = [ - Layer(id=0, kind=LayerKind.INPUT.value, params={"shape": (B, n_in), "dtype": str(center.dtype)}, in_vars=[], out_vars=in_v), - Layer(id=1, kind=LayerKind.INPUT_SPEC.value, params={"kind": "BOX", "lb": lb_in, "ub": ub_in}, in_vars=in_v, out_vars=in_v), - ] - preds: "dict[int, list[int]]" = {0: [], 1: [0]} - succs: "dict[int, list[int]]" = {0: [1], 1: []} - next_id, next_var = 2, n_in - - def alloc(n: int) -> "list[int]": - nonlocal next_var - v = list(range(next_var, next_var + n)); next_var += n - return v - - def add(kind, params, in_vars, out_vars, pred_ids) -> int: - nonlocal next_id - layers.append(Layer(id=next_id, kind=kind, params=params, in_vars=in_vars, out_vars=out_vars)) - lid = next_id; next_id += 1 - preds[lid] = pred_ids - succs.setdefault(lid, []) - for p in pred_ids: - succs[p].append(lid) - return lid - - def dense_pos(W, pos) -> int: - full = torch.zeros(D, n_in, dtype=center.dtype) - full[:, pos * D:(pos + 1) * D] = W - return add(LayerKind.DENSE.value, { - "weight": full, "in_features": n_in, "out_features": D, - "weight_pos": full.clamp(min=0), "weight_neg": full.clamp(max=0), - "bias": torch.zeros(D, dtype=center.dtype), "input_shape": (n_in,), - }, in_v, alloc(D), [1]) - - def dense_value_feature(W, feat) -> int: - full = torch.zeros(L, n_in, dtype=center.dtype) - for p in range(L): - full[p, p * D:(p + 1) * D] = W[feat] - return add(LayerKind.DENSE.value, { - "weight": full, "in_features": n_in, "out_features": L, - "weight_pos": full.clamp(min=0), "weight_neg": full.clamp(max=0), - "bias": torch.zeros(L, dtype=center.dtype), "input_shape": (n_in,), - }, in_v, alloc(L), [1]) - - q_ids = [dense_pos(Wq, p) for p in range(L)] - k_ids = [dense_pos(Wk, p) for p in range(L)] - v_ids = [dense_value_feature(Wv, f) for f in range(D)] - - score_ids = [] - score_vars: "list[int]" = [] - for kp in range(L): - sv = alloc(1) - sid = add(LayerKind.ATT_SCORES.value, { - "dk": float(D) ** 0.5, - "q_vars": layers[q_ids[0]].out_vars, "k_vars": layers[k_ids[kp]].out_vars, - "q_src": q_ids[0], "k_src": k_ids[kp], - }, layers[q_ids[0]].out_vars + layers[k_ids[kp]].out_vars, sv, [q_ids[0], k_ids[kp]]) - score_ids.append(sid); score_vars += sv - cat_id = add(LayerKind.CONCAT.value, {"concat_dim": -1}, score_vars, alloc(L), score_ids) - sm_id = add(LayerKind.SOFTMAX.value, {"axis": -1}, layers[cat_id].out_vars, alloc(L), [cat_id]) - mix_ids = [] - mix_vars: "list[int]" = [] - for f in range(D): - mv = alloc(1) - mid = add(LayerKind.ATT_MIX.value, { - "rowsize": L, "w_vars": layers[sm_id].out_vars, "v_vars": layers[v_ids[f]].out_vars, - "w_src": sm_id, "v_src": v_ids[f], - }, layers[sm_id].out_vars + layers[v_ids[f]].out_vars, mv, [sm_id, v_ids[f]]) - mix_ids.append(mid); mix_vars += mv - join_id = add(LayerKind.CONCAT.value, {"concat_dim": -1}, mix_vars, alloc(D), mix_ids) - gamma = torch.ones(D, dtype=center.dtype) - beta = torch.zeros(D, dtype=center.dtype) - ln_id = add(LayerKind.LAYERNORM.value, {"gamma": gamma, "beta": beta, "variant": "no_var"}, layers[join_id].out_vars, alloc(D), [join_id]) - gelu_id = add(LayerKind.GELU.value, {}, layers[ln_id].out_vars, alloc(D), [ln_id]) - - out_spec = OutputSpec(kind="LINEAR_LE", c=torch.ones(D, dtype=center.dtype), d=torch.tensor(assert_d, dtype=center.dtype)) - enc = out_spec.encode_linear(B=B, n_out=D, device=center.device, dtype=center.dtype) - add(LayerKind.ASSERT.value, enc, layers[gelu_id].out_vars, layers[gelu_id].out_vars, [gelu_id]) - - net = Net(layers=layers, preds=preds, succs=succs) - info: "dict[str, Any]" = {"Wq": Wq, "Wk": Wk, "Wv": Wv, "lb_in": lb_in, "ub_in": ub_in, "out_id": gelu_id, "L": L, "D": D} - return net, info - - -def _make_dual_matmul_net( # pragma: no cover - B: int, I: int, K: int, J: int, center: torch.Tensor, eps: float, assert_d: float, -) -> "tuple[Net, dict[str, Any]]": - """DENSE X [I,K] + DENSE Y [K,J] -> MATMUL -> SOFTMAX -> LAYERNORM -> GELU. - - The ONNX import lowers attention Q.Kt / probs.V to a generic var x var - MATMUL, a distinct dual kernel (forward_matmul / backward_matmul) from the - scalar ATT_SCORES/ATT_MIX cores. This net exercises that batched-bilinear - path end to end through the DualSolver. - """ - from act.back_end.core import Layer - from act.front_end.specs import OutputSpec - - n_in = center.shape[1] - in_v = list(range(n_in)) - lb_in, ub_in = center - eps, center + eps - Wx = torch.randn(I * K, n_in, dtype=center.dtype, generator=torch.Generator().manual_seed(81)) * 0.2 - Wy = torch.randn(K * J, n_in, dtype=center.dtype, generator=torch.Generator().manual_seed(82)) * 0.2 - - layers = [ - Layer(id=0, kind=LayerKind.INPUT.value, params={"shape": (B, n_in), "dtype": str(center.dtype)}, in_vars=[], out_vars=in_v), - Layer(id=1, kind=LayerKind.INPUT_SPEC.value, params={"kind": "BOX", "lb": lb_in, "ub": ub_in}, in_vars=in_v, out_vars=in_v), - ] - x_vars = list(range(n_in, n_in + I * K)) - y_vars = list(range(n_in + I * K, n_in + I * K + K * J)) - z_vars = list(range(n_in + I * K + K * J, n_in + I * K + K * J + I * J)) - - def dense(W, out_vars, n_out): - return { - "weight": W, "in_features": n_in, "out_features": n_out, - "weight_pos": W.clamp(min=0), "weight_neg": W.clamp(max=0), - "bias": torch.zeros(n_out, dtype=center.dtype), "input_shape": (n_in,), - } - - layers.append(Layer(id=2, kind=LayerKind.DENSE.value, params=dense(Wx, x_vars, I * K), in_vars=in_v, out_vars=x_vars)) - layers.append(Layer(id=3, kind=LayerKind.DENSE.value, params=dense(Wy, y_vars, K * J), in_vars=in_v, out_vars=y_vars)) - layers.append(Layer(id=4, kind=LayerKind.MATMUL.value, params={"x_vars": x_vars, "y_vars": y_vars, "x_shape": (I, K), "y_shape": (K, J)}, in_vars=x_vars + y_vars, out_vars=z_vars)) - sm_vars = list(range(z_vars[-1] + 1, z_vars[-1] + 1 + I * J)) - layers.append(Layer(id=5, kind=LayerKind.SOFTMAX.value, params={"axis": -1}, in_vars=z_vars, out_vars=sm_vars)) - gamma = torch.ones(I * J, dtype=center.dtype) - beta = torch.zeros(I * J, dtype=center.dtype) - ln_vars = list(range(sm_vars[-1] + 1, sm_vars[-1] + 1 + I * J)) - layers.append(Layer(id=6, kind=LayerKind.LAYERNORM.value, params={"gamma": gamma, "beta": beta, "variant": "no_var"}, in_vars=sm_vars, out_vars=ln_vars)) - gelu_vars = list(range(ln_vars[-1] + 1, ln_vars[-1] + 1 + I * J)) - layers.append(Layer(id=7, kind=LayerKind.GELU.value, params={}, in_vars=ln_vars, out_vars=gelu_vars)) - out_spec = OutputSpec(kind="LINEAR_LE", c=torch.ones(I * J, dtype=center.dtype), d=torch.tensor(assert_d, dtype=center.dtype)) - enc = out_spec.encode_linear(B=B, n_out=I * J, device=center.device, dtype=center.dtype) - layers.append(Layer(id=8, kind=LayerKind.ASSERT.value, params=enc, in_vars=gelu_vars, out_vars=gelu_vars)) - preds = {0: [], 1: [0], 2: [1], 3: [1], 4: [2, 3], 5: [4], 6: [5], 7: [6], 8: [7]} - succs = {0: [1], 1: [2, 3], 2: [4], 3: [4], 4: [5], 5: [6], 6: [7], 7: [8], 8: []} - net = Net(layers=layers, preds=preds, succs=succs) - info: "dict[str, Any]" = {"Wx": Wx, "Wy": Wy, "lb_in": lb_in, "ub_in": ub_in, "z_id": 4, "I": I, "K": K, "J": J} - return net, info - - -def _dual_forward_box(net, lb_in, ub_in, layer_id): # pragma: no cover - """Run the dual forward pass and return the (lb, ub) box at ``layer_id``.""" - from act.back_end.dual_tf.tf_forward import compute_forward_bounds - - bounds_dict = compute_forward_bounds(net, lb_in.clone(), ub_in.clone(), post_activation=False) - box = bounds_dict[layer_id] - return box.lb, box.ub - - -def _test_dual_transformer_att_cores() -> None: # pragma: no cover - # Dual attention scalar cores end to end: the dual FORWARD pass - # (forward_attention/softmax/layernorm/gelu) box must bracket the concrete - # attention output, and the dual BACKWARD pass (DualSolver.evaluate_spec) - # must CERTIFY a loose bound yet NOT certify a bound below the true range - # (proving the certified bound is used, not vacuous). - from act.back_end.transfer_functions import set_solver_mode, get_solver_mode - from act.util.device_manager import get_default_dtype - from act.util.stats import VerifyStatus - - dtype = get_default_dtype() - B, L, D = 1, 2, 2 - torch.manual_seed(90) - center = torch.randn(B, L * D, dtype=dtype) * 0.05 - eps = 0.02 - net, info = _make_dual_att_cores_net(B, L, D, center, eps, assert_d=100.0) - Wq, Wk, Wv = info["Wq"], info["Wk"], info["Wv"] - l_box, u_box = info["lb_in"], info["ub_in"] - - def concrete_gelu_out(x: torch.Tensor) -> torch.Tensor: - x3 = x.reshape(B, L, D) - q0 = x3[:, 0, :] @ Wq.t() - scores = torch.cat([(q0 * (x3[:, kp, :] @ Wk.t())).sum(-1, keepdim=True) / (D ** 0.5) for kp in range(L)], dim=-1) - probs = torch.softmax(scores, dim=-1) - v = torch.stack([x3[:, p, :] @ Wv.t() for p in range(L)], dim=1) - ctx = torch.cat([(probs * v[:, :, f]).sum(-1, keepdim=True) for f in range(D)], dim=-1) - normed = ctx - ctx.mean(dim=-1, keepdim=True) - return torch.nn.functional.gelu(normed) - - lb, ub = _dual_forward_box(net, l_box, u_box, info["out_id"]) - assert torch.isfinite(lb).all() and torch.isfinite(ub).all(), "dual att-cores forward box must be finite" - assert (lb <= ub + 1e-9).all(), "dual att-cores forward box lb must not exceed ub" - concrete_sum_max = float(concrete_gelu_out(l_box).sum(-1).item()) - for _ in range(120): - x = l_box + torch.rand_like(l_box) * (u_box - l_box) - concrete_sum_max = max(concrete_sum_max, float(concrete_gelu_out(x).sum(-1).item())) - - prev = get_solver_mode() - try: - set_solver_mode("dual") - loose = verify_once(net) - assert loose[0].status == VerifyStatus.CERTIFIED, f"dual att-cores: loose bound expected CERTIFIED, got {loose[0].status}" - assert concrete_sum_max <= 100.0 + 1e-6, ( - f"dual att-cores: certified d=100 contradicted by concrete sum {concrete_sum_max}" - ) - net_tight, _ = _make_dual_att_cores_net(B, L, D, center, eps, assert_d=concrete_sum_max - 1.0) - tight = verify_once(net_tight) - assert tight[0].status != VerifyStatus.CERTIFIED, ( - f"dual att-cores: threshold below range must NOT certify, got {tight[0].status}" - ) - finally: - set_solver_mode(prev) - - -def _test_dual_transformer_matmul() -> None: # pragma: no cover - # Dual batched-bilinear MATMUL core (the ONNX attention lowering) end to - # end: forward_matmul box brackets the concrete X@Y (through softmax/ - # layernorm/gelu), and backward_matmul via DualSolver certifies a loose - # bound but not a below-range one. - from act.back_end.transfer_functions import set_solver_mode, get_solver_mode - from act.util.device_manager import get_default_dtype - from act.util.stats import VerifyStatus - - dtype = get_default_dtype() - B, I, K, J = 1, 2, 2, 2 - torch.manual_seed(91) - center = torch.randn(B, 3, dtype=dtype) * 0.05 - eps = 0.02 - net, info = _make_dual_matmul_net(B, I, K, J, center, eps, assert_d=100.0) - Wx, Wy = info["Wx"], info["Wy"] - l_box, u_box = info["lb_in"], info["ub_in"] - - def concrete_matmul_z(x: torch.Tensor) -> torch.Tensor: - X = (x @ Wx.t()).reshape(B, I, K) - Y = (x @ Wy.t()).reshape(B, K, J) - return (X @ Y).reshape(B, I * J) - - lb, ub = _dual_forward_box(net, l_box, u_box, info["z_id"]) - n_samples = 120 - true_min = concrete_matmul_z(l_box).clone() - true_max = true_min.clone() - for _ in range(n_samples): - x = l_box + torch.rand_like(l_box) * (u_box - l_box) - z = concrete_matmul_z(x) - true_min = torch.minimum(true_min, z) - true_max = torch.maximum(true_max, z) - # MATMUL forward box is the sound four-corner McCormick envelope; it must - # bracket the concrete X@Y (the layernorm/gelu that follow are checked via - # the end-to-end certified bound below, not this pre-softmax box). - assert (lb <= true_min + 1e-6).all(), "dual MATMUL forward: unsound lower bound" - assert (ub >= true_max - 1e-6).all(), "dual MATMUL forward: unsound upper bound" - - prev = get_solver_mode() - try: - set_solver_mode("dual") - loose = verify_once(net) - assert loose[0].status == VerifyStatus.CERTIFIED, f"dual MATMUL: loose expected CERTIFIED, got {loose[0].status}" - net_tight, info_t = _make_dual_matmul_net(B, I, K, J, center, eps, assert_d=-50.0) - tight = verify_once(net_tight) - assert tight[0].status != VerifyStatus.CERTIFIED, ( - f"dual MATMUL: threshold below range must NOT certify, got {tight[0].status}" - ) - finally: - set_solver_mode(prev) - - -def _test_dual_lp_embedding_finite_p() -> None: # pragma: no cover - # Finite-p LP_EMBEDDING input spec (p_norm=2) verified through the dual - # solver: exercises seed_from_input_specs' LP_EMBEDDING center/eps/ - # perturbed_positions seeding AND solver_dual's exact per-word Lp-ball - # dual-norm input contribution (_resolve_perturbation_norm -> - # _dual_norm_exponent -> _dual_norm_contribution / _perturbed_block_slices), - # the finite-p path box/L-inf specs never reach. - from act.back_end.core import Layer - from act.back_end.transfer_functions import set_solver_mode, get_solver_mode - from act.front_end.specs import OutputSpec, InKind - from act.util.device_manager import get_default_dtype - from act.util.stats import VerifyStatus - - dtype = get_default_dtype() - B, L, D = 1, 2, 2 - n_in = L * D - torch.manual_seed(97) - center3 = torch.randn(B, L, D, dtype=dtype) * 0.1 - eps = 0.05 - in_v = list(range(n_in)) - d_v = list(range(n_in, n_in + 2)) - W = torch.randn(2, n_in, dtype=dtype) * 0.2 - - def build(assert_d: float) -> Net: - layers = [ - Layer(id=0, kind=LayerKind.INPUT.value, params={"shape": (B, L, D), "dtype": str(dtype)}, in_vars=[], out_vars=in_v), - Layer(id=1, kind=LayerKind.INPUT_SPEC.value, params={"kind": InKind.LP_EMBEDDING, "center": center3, "eps": torch.tensor([eps], dtype=dtype), "p_norm": 2.0, "perturbed_positions": torch.tensor([0])}, in_vars=in_v, out_vars=in_v), - Layer(id=2, kind=LayerKind.DENSE.value, params={"weight": W, "in_features": n_in, "out_features": 2, "weight_pos": W.clamp(min=0), "weight_neg": W.clamp(max=0), "bias": torch.zeros(2, dtype=dtype), "input_shape": (n_in,)}, in_vars=in_v, out_vars=d_v), - ] - enc = OutputSpec(kind="LINEAR_LE", c=torch.ones(2, dtype=dtype), d=torch.tensor(assert_d, dtype=dtype)).encode_linear(B=B, n_out=2, device=torch.device("cpu"), dtype=dtype) - layers.append(Layer(id=3, kind=LayerKind.ASSERT.value, params=enc, in_vars=d_v, out_vars=d_v)) - return Net(layers=layers, preds={0: [], 1: [0], 2: [1], 3: [2]}, succs={0: [1], 1: [2], 2: [3], 3: []}) - - prev = get_solver_mode() - try: - set_solver_mode("dual") - loose = verify_once(build(100.0)) - assert loose[0].status == VerifyStatus.CERTIFIED, f"dual LP_EMBEDDING: loose expected CERTIFIED, got {loose[0].status}" - tight = verify_once(build(-100.0)) - assert tight[0].status != VerifyStatus.CERTIFIED, ( - f"dual LP_EMBEDDING: threshold below range must NOT certify, got {tight[0].status}" - ) - finally: - set_solver_mode(prev) - - -def _test_dual_smooth_activations() -> None: # pragma: no cover - # Dual backward for the new smooth activations (ERF/SQRT/SIN/COS/QUANTIZE - # in dual_tf/tf_smooth.py): a DENSE -> activation -> ASSERT net run through - # the DualSolver must CERTIFY a loose bound, exercising each activation's - # forward relaxation + backward routing. - from act.back_end.core import Layer - from act.back_end.transfer_functions import set_solver_mode, get_solver_mode - from act.util.device_manager import get_default_dtype - from act.util.stats import VerifyStatus - - dtype = get_default_dtype() - B, n = 1, 3 - - def build(act_kind: str, act_params: "dict[str, Any]") -> Net: - center = torch.full((B, n), 0.7, dtype=dtype) - lb_in, ub_in = center - 0.05, center + 0.05 - in_v = list(range(n)) - d_v = list(range(n, 2 * n)) - o_v = list(range(2 * n, 3 * n)) - W = torch.eye(n, dtype=dtype) - layers = [ - Layer(id=0, kind=LayerKind.INPUT.value, params={"shape": (B, n), "dtype": str(dtype)}, in_vars=[], out_vars=in_v), - Layer(id=1, kind=LayerKind.INPUT_SPEC.value, params={"kind": "BOX", "lb": lb_in, "ub": ub_in}, in_vars=in_v, out_vars=in_v), - Layer(id=2, kind=LayerKind.DENSE.value, params={"weight": W, "in_features": n, "out_features": n, "weight_pos": W, "weight_neg": W * 0, "bias": torch.zeros(n, dtype=dtype), "input_shape": (n,)}, in_vars=in_v, out_vars=d_v), - Layer(id=3, kind=act_kind, params=act_params, in_vars=d_v, out_vars=o_v), - ] - from act.front_end.specs import OutputSpec - enc = OutputSpec(kind="LINEAR_LE", c=torch.ones(n, dtype=dtype), d=torch.tensor(100.0, dtype=dtype)).encode_linear(B=B, n_out=n, device=torch.device("cpu"), dtype=dtype) - layers.append(Layer(id=4, kind=LayerKind.ASSERT.value, params=enc, in_vars=o_v, out_vars=o_v)) - return Net(layers=layers, preds={0: [], 1: [0], 2: [1], 3: [2], 4: [3]}, succs={0: [1], 1: [2], 2: [3], 3: [4], 4: []}) - - cases = [ - (LayerKind.ERF.value, {}), - (LayerKind.SQRT.value, {}), - (LayerKind.SIN.value, {}), - (LayerKind.COS.value, {}), - (LayerKind.QUANTIZE.value, {"scale": torch.tensor([0.1], dtype=dtype), "zero_point": torch.tensor([0.0], dtype=dtype), "qmin": -128, "qmax": 127}), - ] - prev = get_solver_mode() - try: - set_solver_mode("dual") - for kind, params in cases: - r = verify_once(build(kind, params)) - assert r[0].status == VerifyStatus.CERTIFIED, f"dual {kind}: expected CERTIFIED, got {r[0].status}" - finally: - set_solver_mode(prev) - - -def _test_dual_mha_split_join_not_implemented() -> None: # pragma: no cover - # The dual path deliberately stubs the MHA split/join reshape family - # (only the ATT_SCORES/ATT_MIX scalar cores + MATMUL are relaxed); the - # stubs must raise NotImplementedError so a mis-lowered net fails loudly. - from act.back_end.core import Layer - from act.back_end.dual_tf.tf_transformer import forward_mha, backward_mha - - dummy = Layer(id=0, kind=LayerKind.MHA_SPLIT.value, params={}, in_vars=[0], out_vars=[0]) - raised_fwd = False - try: - forward_mha(dummy, [], [], [], [], False, torch.device("cpu"), torch.get_default_dtype()) - except NotImplementedError: - raised_fwd = True - assert raised_fwd, "forward_mha must raise NotImplementedError" - raised_bwd = False - try: - backward_mha(dummy, torch.zeros(1, 1), {}, []) - except NotImplementedError: - raised_bwd = True - assert raised_bwd, "backward_mha must raise NotImplementedError" - - - - - - - - -def _test_act2torch_smooth_activation_reconstruction() -> None: # pragma: no cover - from act.back_end.core import Layer - from act.pipeline.verification.act2torch import ACTToTorch - from act.front_end.specs import OutputSpec, OutKind - from act.util.device_manager import get_default_dtype - - dtype = get_default_dtype() - B, n = 1, 2 - in_v = list(range(n)) - layer_vars = [list(range((i + 1) * n, (i + 2) * n)) for i in range(5)] - x = torch.tensor([[0.64, 0.81]], dtype=dtype) - eps = torch.tensor([[0.01, 0.01]], dtype=dtype) - encoded = OutputSpec( - kind=OutKind.LINEAR_LE, - c=torch.ones(n, dtype=dtype), - d=torch.tensor(10.0, dtype=dtype), - ).encode_linear(B=B, n_out=n, device=torch.device("cpu"), dtype=dtype) - layers = [ - Layer(id=0, kind=LayerKind.INPUT.value, params={"shape": (B, n), "dtype": str(dtype)}, in_vars=[], out_vars=in_v), - Layer(id=1, kind=LayerKind.INPUT_SPEC.value, params={"kind": InKind.BOX, "lb": x - eps, "ub": x + eps}, in_vars=in_v, out_vars=in_v), - Layer(id=2, kind=LayerKind.ERF.value, params={}, in_vars=in_v, out_vars=layer_vars[0]), - Layer(id=3, kind=LayerKind.SQRT.value, params={}, in_vars=layer_vars[0], out_vars=layer_vars[1]), - Layer(id=4, kind=LayerKind.SIN.value, params={}, in_vars=layer_vars[1], out_vars=layer_vars[2]), - Layer(id=5, kind=LayerKind.COS.value, params={}, in_vars=layer_vars[2], out_vars=layer_vars[3]), - Layer( - id=6, - kind=LayerKind.QUANTIZE.value, - params={"scale": torch.tensor([0.05], dtype=dtype), "zero_point": torch.tensor([0.0], dtype=dtype), "qmin": -128, "qmax": 127}, - in_vars=layer_vars[3], - out_vars=layer_vars[4], - ), - Layer(id=7, kind=LayerKind.ASSERT.value, params=encoded, in_vars=layer_vars[4], out_vars=layer_vars[4]), - ] - net = Net( - layers=layers, - preds={0: [], 1: [0], 2: [1], 3: [2], 4: [3], 5: [4], 6: [5], 7: [6]}, - succs={0: [1], 1: [2], 2: [3], 3: [4], 4: [5], 5: [6], 6: [7], 7: []}, - ) - - restored = ACTToTorch(net).run() - y = restored(x)["output"] - expected = torch.erf(x) - expected = torch.sqrt(torch.clamp(expected, min=0.0)) - expected = torch.sin(expected) - expected = torch.cos(expected) - expected = 0.05 * torch.clamp(torch.round(expected / 0.05), min=-128.0, max=127.0) - assert torch.allclose(y, expected, atol=1e-6, rtol=1e-6), ( - f"smooth ACTToTorch reconstruction mismatch: got={y.tolist()} want={expected.tolist()}" - ) - - -def _test_torch2act_minimal_vit_fixture_soundness() -> None: # pragma: no cover - import torch.nn as nn - from act.back_end.analyze import analyze - from act.back_end.core import Fact, ConSet - from act.front_end.spec_creator_base import LabeledInputTensor - from act.front_end.specs import InputSpec, OutputSpec, OutKind - from act.front_end.verifiable_model import InputLayer, InputSpecLayer, OutputSpecLayer, VerifiableModel - from act.pipeline.verification.torch2act import TorchToACT - from act.util.device_manager import get_default_dtype - - dtype = get_default_dtype() - - class TinyRegressionBertLayerNorm(nn.LayerNorm): - - def __init__(self, hidden_size: int) -> None: - super().__init__(hidden_size, eps=1e-5) - self.variance_epsilon = self.eps - - - class TinyRegressionBertSelfAttention(nn.Module): - - def __init__(self, hidden_size: int) -> None: - super().__init__() - self.num_attention_heads = 1 - self.attention_head_size = hidden_size - self.query = nn.Linear(hidden_size, hidden_size) - self.key = nn.Linear(hidden_size, hidden_size) - self.value = nn.Linear(hidden_size, hidden_size) - - def forward(self, hidden_states: torch.Tensor) -> torch.Tensor: - query_layer = self.query(hidden_states) - key_layer = self.key(hidden_states) - value_layer = self.value(hidden_states) - attention_scores = torch.matmul(query_layer, key_layer.transpose(-1, -2)) - attention_scores = attention_scores / (self.attention_head_size ** 0.5) - attention_probs = torch.softmax(attention_scores, dim=-1) - return torch.matmul(attention_probs, value_layer) - - - class TinyRegressionBertSelfOutput(nn.Module): - - def __init__(self, hidden_size: int) -> None: - super().__init__() - self.dense = nn.Linear(hidden_size, hidden_size) - self.LayerNorm = TinyRegressionBertLayerNorm(hidden_size) - - def forward( - self, - hidden_states: torch.Tensor, - input_tensor: torch.Tensor, - ) -> torch.Tensor: - return self.LayerNorm(self.dense(hidden_states) + input_tensor) - - - class TinyRegressionBertAttention(nn.Module): - - def __init__(self, hidden_size: int) -> None: - super().__init__() - self.self = TinyRegressionBertSelfAttention(hidden_size) - self.output = TinyRegressionBertSelfOutput(hidden_size) - - def forward(self, input_tensor: torch.Tensor) -> torch.Tensor: - return self.output(self.self(input_tensor), input_tensor) - - - class TinyRegressionBertIntermediate(nn.Module): - - def __init__(self, hidden_size: int, intermediate_size: int) -> None: - super().__init__() - self.dense = nn.Linear(hidden_size, intermediate_size) - self.intermediate_act_fn = nn.GELU() - - def forward(self, hidden_states: torch.Tensor) -> torch.Tensor: - return self.intermediate_act_fn(self.dense(hidden_states)) - - - class TinyRegressionBertOutput(nn.Module): - - def __init__(self, hidden_size: int, intermediate_size: int) -> None: - super().__init__() - self.dense = nn.Linear(intermediate_size, hidden_size) - self.LayerNorm = TinyRegressionBertLayerNorm(hidden_size) - - def forward( - self, - hidden_states: torch.Tensor, - input_tensor: torch.Tensor, - ) -> torch.Tensor: - return self.LayerNorm(self.dense(hidden_states) + input_tensor) - - - class TinyRegressionBertLayer(nn.Module): - - def __init__(self, hidden_size: int, intermediate_size: int) -> None: - super().__init__() - self.attention = TinyRegressionBertAttention(hidden_size) - self.intermediate = TinyRegressionBertIntermediate( - hidden_size, - intermediate_size, - ) - self.output = TinyRegressionBertOutput(hidden_size, intermediate_size) - - def forward(self, hidden_states: torch.Tensor) -> torch.Tensor: - attention_output = self.attention(hidden_states) - intermediate_output = self.intermediate(attention_output) - return self.output(intermediate_output, attention_output) - - class PatchEmbed(nn.Module): - def __init__(self) -> None: - super().__init__() - self.proj = nn.Conv2d(1, 2, kernel_size=2, stride=2, bias=True) - - def forward(self, x: torch.Tensor) -> torch.Tensor: - return self.proj(x) - - class TinyDuckViT(nn.Module): - def __init__(self) -> None: - super().__init__() - self.patch_embed = PatchEmbed() - self.block = TinyRegressionBertLayer(hidden_size=2, intermediate_size=4) - self.norm = TinyRegressionBertLayerNorm(2) - self.head = nn.Linear(2, 2) - self.cls_token = nn.Parameter(torch.zeros(1, 1, 2, dtype=dtype)) - self.pos_embed = nn.Parameter(torch.zeros(1, 2, 2, dtype=dtype)) - - def forward(self, x: torch.Tensor) -> torch.Tensor: - patch = self.patch_embed.proj(x).flatten(2).transpose(1, 2) - cls = self.cls_token.expand(x.shape[0], -1, -1) - hidden = torch.cat([cls, patch], dim=1) + self.pos_embed - hidden = self.block(hidden) - hidden = self.norm(hidden) - return self.head(hidden[:, 0, :]) - - torch.manual_seed(23) - body = TinyDuckViT().to(dtype=dtype).eval() - center = torch.tensor([[[[0.1, -0.2], [0.3, 0.4]]]], dtype=dtype) - eps = torch.full_like(center, 1e-4) - wrapped = VerifiableModel( - input_layer=InputLayer( - labeled_input=LabeledInputTensor(tensor=center, label=None), - shape=tuple(center.shape), - dtype=dtype, - ), - input_spec=InputSpecLayer(InputSpec(kind=InKind.BOX, lb=center - eps, ub=center + eps)), - model=body, - output_spec=OutputSpecLayer( - OutputSpec(kind=OutKind.LINEAR_LE, c=torch.ones(2, dtype=dtype), d=torch.tensor(100.0, dtype=dtype)) - ), - ).eval() - - net = TorchToACT(wrapped).run() - kinds = [layer.kind for layer in net.layers] - assert LayerKind.CONV2D.value in kinds, "ViT fixture must emit patch Conv2d" - assert kinds.count(LayerKind.CONSTANT.value) >= 2, "ViT fixture must emit cls/pos constants" - assert LayerKind.ATT_SCORES.value in kinds and LayerKind.ATT_MIX.value in kinds, ( - "ViT fixture must lower the block through attention layers" - ) - - entry_id = find_entry_layer_id(net) - seed = seed_from_input_specs(gather_input_spec_layers(net)) - entry_fact = Fact(bounds=seed, cons=ConSet()) - add_all_input_specs(entry_fact.cons, get_input_ids(net), gather_input_spec_layers(net)) - _before, after, _global_c = analyze(net, entry_id, entry_fact) - conv_layer = next(layer for layer in net.layers if layer.kind == LayerKind.CONV2D.value) - conv_bounds = after[conv_layer.id].bounds - concrete_patch = body.patch_embed.proj(center).reshape(1, -1) - assert torch.isfinite(conv_bounds.lb).all() and torch.isfinite(conv_bounds.ub).all(), ( - "ViT fixture patch Conv2d bounds must be finite" - ) - assert (conv_bounds.lb <= concrete_patch + 1e-6).all(), "ViT patch lower bound must cover concrete output" - assert (conv_bounds.ub >= concrete_patch - 1e-6).all(), "ViT patch upper bound must cover concrete output" - results = verify_once(net) - assert len(results) == 1 and results[0].status in { - VerifyStatus.CERTIFIED, VerifyStatus.FALSIFIED, VerifyStatus.UNKNOWN - }, f"ViT fixture verify_once returned unexpected result {results}" - - - - - - -def _test_verify_once_b3_all_certified() -> None: # pragma: no cover - # Zero DENSE -> abstract output is singleton {0}, well below d=10. - # End-to-end check that the [B*M, n_out] cert pass folds to per-sample. - from act.util.device_manager import get_default_device, get_default_dtype - from act.util.stats import VerifyStatus - - device = get_default_device() - dtype = get_default_dtype() - - B, n_in, n_out = 3, 4, 2 - W = torch.zeros(n_out, n_in, device=device, dtype=dtype) - b = torch.zeros(n_out, device=device, dtype=dtype) - lb_in = torch.full((B, n_in), -1.0, device=device, dtype=dtype) - ub_in = torch.full((B, n_in), 1.0, device=device, dtype=dtype) - - net = _make_dense_net_box_test( - B=B, n_in=n_in, n_out=n_out, weight=W, bias=b, - lb_in=lb_in, ub_in=ub_in, - assert_params={ - "kind": "LINEAR_LE", - "c": torch.tensor([1.0, 1.0], device=device, dtype=dtype), - "d": 10.0, - }, - ) - - results = verify_once(net) - assert len(results) == B, f"expected {B} results, got {len(results)}" - for i, r in enumerate(results): - assert r.status == VerifyStatus.CERTIFIED, ( - f"sample {i}: expected CERTIFIED, got {r.status}" - ) - - -def _test_verify_once_b8_mixed_outcomes() -> None: # pragma: no cover - # 8 input boxes designed to produce CERT/FALS/UNK mix in one run, - # proving the cert pass + concrete falsification operate sample-wise - # rather than collapsing the batch. - from act.util.device_manager import get_default_device, get_default_dtype - from act.util.stats import VerifyStatus - - device = get_default_device() - dtype = get_default_dtype() - - B, n_in, n_out = 8, 2, 2 - W = torch.eye(n_out, device=device, dtype=dtype) - b = torch.zeros(n_out, device=device, dtype=dtype) - lb_in = torch.tensor( - [ - [2.0, -2.0], - [1.0, -2.0], - [-1.0, 0.0], - [0.0, 1.0], - [-1.0, -1.0], - [-2.0, -1.0], - [1.0, -1.0], - [-1.0, 0.0], - ], - device=device, dtype=dtype, - ) - ub_in = torch.tensor( - [ - [3.0, -1.0], - [2.0, -1.5], - [1.0, 2.0], - [1.0, 2.0], - [1.0, 0.5], - [2.0, 0.5], - [2.0, 0.0], - [1.0, 1.0], - ], - device=device, dtype=dtype, - ) - net = _make_dense_net_box_test( - B=B, n_in=n_in, n_out=n_out, weight=W, bias=b, - lb_in=lb_in, ub_in=ub_in, - assert_params={ - "kind": "TOP1_ROBUST", - "y_true": torch.zeros(B, dtype=torch.long, device=device), - }, - ) - - def model_fn(x: torch.Tensor) -> torch.Tensor: - return x - - results = verify_once(net, model_fn=model_fn) - assert len(results) == B, f"expected {B} results, got {len(results)}" - - valid = { - VerifyStatus.CERTIFIED, VerifyStatus.FALSIFIED, VerifyStatus.UNKNOWN, - } - statuses = [r.status for r in results] - assert all(s in valid for s in statuses), ( - f"unexpected status enum value in {statuses}" - ) - assert any(s == VerifyStatus.CERTIFIED for s in statuses), ( - f"no CERTIFIED lane in {statuses}" - ) - assert any(s == VerifyStatus.FALSIFIED for s in statuses), ( - f"no FALSIFIED lane in {statuses}" - ) - assert any(s == VerifyStatus.UNKNOWN for s in statuses), ( - f"no UNKNOWN lane in {statuses}" - ) - - -_TESTS = [ # pragma: no cover - _test_verify_once_b3_all_certified, - _test_verify_once_b8_mixed_outcomes, - _test_att_scores_dual_planar_analyze_soundness, - _test_att_scores_dual_planar_verify_once_certified, - _test_att_scores_dual_planar_lp_export_solve, - _test_att_scores_dual_planar_masked_and_clamp_alpha_soundness, - _test_mini_transformer_block_analyze_soundness, - _test_mha_split_edge_cases_and_mask_add, - _test_new_elementwise_tf_soundness, - _test_dual_transformer_att_cores, - _test_dual_transformer_matmul, - _test_dual_lp_embedding_finite_p, - _test_dual_smooth_activations, - _test_dual_mha_split_join_not_implemented, - _test_act2torch_smooth_activation_reconstruction, - _test_torch2act_minimal_vit_fixture_soundness, -] - - -def run_all_tests() -> int: - passed = failed = 0 - for fn in _TESTS: - try: - fn() - passed += 1 - print(f" PASS {fn.__name__}") - except Exception as e: - failed += 1 - print(f" FAIL {fn.__name__}: {type(e).__name__}: {e}") - print(f"\n{passed} passed, {failed} failed") - return 1 if failed else 0 - - -def main() -> int: - # Pin device/dtype to CPU/float64 so hosts where CUDA is visible but - # no kernel matches the runtime's compute capability don't raise on - # the default GPU init path in act.util.device_manager. - from act.util.device_manager import initialize_device - - initialize_device("cpu", "float64") - print("Running verifier self-tests (act.back_end.verifier)\n") - return run_all_tests() - - -if __name__ == "__main__": - import sys - - sys.exit(main()) diff --git a/act/pipeline/verification/act2torch.py b/act/pipeline/verification/act2torch.py index 5142c72b5..dd89a9602 100644 --- a/act/pipeline/verification/act2torch.py +++ b/act/pipeline/verification/act2torch.py @@ -60,6 +60,169 @@ def _align_elementwise_param(param: torch.Tensor, x: torch.Tensor) -> torch.Tens return param +class ACTErf(nn.Module): + def forward(self, x: torch.Tensor) -> torch.Tensor: + return torch.erf(x) + + +class ACTSqrt(nn.Module): + def forward(self, x: torch.Tensor) -> torch.Tensor: + return torch.sqrt(torch.clamp(x, min=0.0)) + + +class ACTSin(nn.Module): + def forward(self, x: torch.Tensor) -> torch.Tensor: + return torch.sin(x) + + +class ACTCos(nn.Module): + def forward(self, x: torch.Tensor) -> torch.Tensor: + return torch.cos(x) + + +class ACTQuantize(nn.Module): + def __init__( + self, + scale: object = None, + zero_point: object = None, + qmin: int = 0, + qmax: int = 255, + ) -> None: + super().__init__() + self.register_buffer("scale", torch.as_tensor(1.0 if scale is None else scale)) + self.register_buffer( + "zero_point", torch.as_tensor(0 if zero_point is None else zero_point) + ) + self.qmin = float(qmin) + self.qmax = float(qmax) + + def forward(self, x: torch.Tensor) -> torch.Tensor: + scale = self.get_buffer("scale").to(device=x.device, dtype=x.dtype) + zero_point = self.get_buffer("zero_point").to(device=x.device, dtype=x.dtype) + quantized = torch.clamp( + torch.round(x / scale), + min=self.qmin - zero_point, + max=self.qmax - zero_point, + ) + return scale * quantized + + +class ACTMatMul(nn.Module): + def forward(self, x: torch.Tensor, y: torch.Tensor) -> torch.Tensor: + return torch.matmul(x, y) + + +class ACTMaskAdd(nn.Module): + def __init__(self, mask: torch.Tensor) -> None: + super().__init__() + self.register_buffer("mask", mask.detach().clone()) + + def forward(self, x: torch.Tensor) -> torch.Tensor: + mask = self.get_buffer("mask").to(device=x.device, dtype=x.dtype) + return x + mask + + +class ACTLayerNorm(nn.Module): + def __init__( + self, + gamma: torch.Tensor, + beta: torch.Tensor, + eps: float, + variant: str, + ) -> None: + super().__init__() + self.register_buffer("gamma", gamma.detach().clone()) + self.register_buffer("beta", beta.detach().clone()) + self.eps = eps + self.variant = variant + + def forward(self, x: torch.Tensor) -> torch.Tensor: + gamma = self.get_buffer("gamma").to(device=x.device, dtype=x.dtype) + beta = self.get_buffer("beta").to(device=x.device, dtype=x.dtype) + if self.variant == "no_var": + dims = tuple(range(1, x.dim())) + return (x - x.mean(dim=dims, keepdim=True)) * gamma + beta + import torch.nn.functional as F + + return F.layer_norm(x, gamma.shape, weight=gamma, bias=beta, eps=self.eps) + + +class ACTMHASplit(nn.Module): + def __init__( + self, + weight: Optional[torch.Tensor], + bias: Optional[torch.Tensor], + role: str, + position: int, + feature: int, + hidden_size: Optional[int], + ) -> None: + super().__init__() + self.register_buffer( + "weight", weight.detach().clone() if isinstance(weight, torch.Tensor) else None + ) + self.register_buffer( + "bias", bias.detach().clone() if isinstance(bias, torch.Tensor) else None + ) + self.role = role + self.position = position + self.feature = feature + self.hidden_size = hidden_size + + def forward(self, x: torch.Tensor) -> torch.Tensor: + weight = self.get_buffer("weight") + if weight is None: + return x + import torch.nn.functional as F + + weight = weight.to(device=x.device, dtype=x.dtype) + bias = self.get_buffer("bias") + if bias is not None: + bias = bias.to(device=x.device, dtype=x.dtype) + projected = F.linear(x.reshape(x.shape[0], -1, weight.shape[1]), weight, bias) + hidden = self.hidden_size or int(projected.shape[-1]) + sequence_length = projected.shape[1] + projected = projected.reshape(x.shape[0], sequence_length, hidden) + if self.role in {"query", "key"}: + return projected[:, self.position, :] + if self.role == "value": + return projected[:, :, self.feature] + return projected + + +class ACTAttentionScores(nn.Module): + def __init__(self, dk: float, mask: Optional[torch.Tensor]) -> None: + super().__init__() + self.dk = dk + self.register_buffer( + "mask", mask.detach().clone() if isinstance(mask, torch.Tensor) else None + ) + + def forward(self, query: torch.Tensor, key: torch.Tensor) -> torch.Tensor: + output = (query * key).sum(dim=-1, keepdim=True) / self.dk + mask = self.get_buffer("mask") + if mask is not None: + output = output + mask.to(device=output.device, dtype=output.dtype) + return output + + +class ACTAttentionMix(nn.Module): + def forward(self, weights: torch.Tensor, values: torch.Tensor) -> torch.Tensor: + return (weights * values).sum(dim=-1, keepdim=True) + + +class ACTMHAJoin(nn.Module): + def __init__(self, sequence_length: int, hidden_size: Optional[int]) -> None: + super().__init__() + self.sequence_length = sequence_length + self.hidden_size = hidden_size + + def forward(self, *inputs: torch.Tensor) -> torch.Tensor: + output = torch.cat(inputs, dim=-1) + hidden_size = self.hidden_size or int(output.shape[-1]) + return output.reshape(output.shape[0], self.sequence_length, hidden_size) + + class ActGraphModule(nn.Module): """DAG-aware nn.Module for ACT body graphs reconstructed by ACTToTorch. @@ -144,12 +307,6 @@ def forward(self, x): if mod is None: out = self._apply_functional(layer, inp_tensors) else: - if len(inp_tensors) > 1: - raise NotImplementedError( - f"ActGraphModule: module-backed layer {layer.kind} (id={lid}) " - f"received {len(inp_tensors)} inputs; multi-input module dispatch " - f"not implemented (current torch2act does not emit such nets)." - ) if layer.kind == LayerKind.DENSE.value and inp_tensors[0].dim() >= 3: import torch.nn.functional as F output_shape = layer.params.get("output_shape") @@ -168,7 +325,7 @@ def forward(self, x): else: out = mod(inp_tensors[0]) else: - out = mod(inp_tensors[0]) + out = mod(*inp_tensors) # nn.RNN / LSTM / GRU return (output, hidden); MHA returns # (output, attn_weights). Verification only consumes the # primary output tensor, so drop the auxiliary state. @@ -295,7 +452,7 @@ def _apply_functional(self, layer, inputs): axes = layer.params.get("axes") keepdims = bool(layer.params.get("keepdims", 0)) if axes is None: - return torch.sum(inputs[0], keepdim=keepdims) + axes = tuple(range(inputs[0].dim())) return torch.sum(inputs[0], dim=tuple(int(a) for a in axes), keepdim=keepdims) if kind == LayerKind.COMPARE.value: if len(inputs) != 2: @@ -340,7 +497,7 @@ def _apply_functional(self, layer, inputs): mode = str(layer.params.get("mode", "nearest")).lower() scale_factor = layer.params.get("scale_factor") size = layer.params.get("size") - kwargs = {"mode": mode} + kwargs: Dict[str, Any] = {"mode": mode} if mode != "nearest" and layer.params.get("align_corners") is not None: kwargs["align_corners"] = bool(layer.params["align_corners"]) if size is not None: @@ -884,10 +1041,6 @@ def _to_target_tensor(value: Any) -> Any: LayerKind.ADD.value, LayerKind.CONCAT.value, LayerKind.MUL.value, - LayerKind.MHA_SPLIT.value, - LayerKind.ATT_SCORES.value, - LayerKind.ATT_MIX.value, - LayerKind.MHA_JOIN.value, }: layer_modules[lid] = None else: @@ -1042,6 +1195,57 @@ def _build_from_schema(self, act_layer: Layer) -> Optional[nn.Module]: if kind in (LayerKind.RNN.value, LayerKind.GRU.value, LayerKind.LSTM.value): return self._build_rnn_family(act_layer) + if kind == LayerKind.ERF.value: + return ACTErf() + if kind == LayerKind.SQRT.value: + return ACTSqrt() + if kind == LayerKind.SIN.value: + return ACTSin() + if kind == LayerKind.COS.value: + return ACTCos() + if kind == LayerKind.QUANTIZE.value: + return ACTQuantize( + scale=params.get("scale"), + zero_point=params.get("zero_point"), + qmin=int(cast(Any, params.get("qmin", 0))), + qmax=int(cast(Any, params.get("qmax", 255))), + ) + if kind == LayerKind.MATMUL.value: + return ACTMatMul() + if kind == LayerKind.MASK_ADD.value: + return ACTMaskAdd(cast(torch.Tensor, params["M"])) + if kind == LayerKind.LAYERNORM.value: + variant = str(params.get("variant", params.get("layer_norm", "standard"))) + return ACTLayerNorm( + gamma=cast(torch.Tensor, params["gamma"]), + beta=cast(torch.Tensor, params["beta"]), + eps=float(cast(Any, params.get("eps", 1e-5))), + variant=variant, + ) + if kind == LayerKind.MHA_SPLIT.value: + hidden_size = params.get("hidden_size") + return ACTMHASplit( + weight=cast(Optional[torch.Tensor], params.get("weight")), + bias=cast(Optional[torch.Tensor], params.get("bias")), + role=str(params.get("role", "")), + position=int(cast(Any, params.get("position", 0))), + feature=int(cast(Any, params.get("feature", 0))), + hidden_size=int(cast(Any, hidden_size)) if hidden_size is not None else None, + ) + if kind == LayerKind.ATT_SCORES.value: + return ACTAttentionScores( + dk=float(cast(Any, params["dk"])), + mask=cast(Optional[torch.Tensor], params.get("mask")), + ) + if kind == LayerKind.ATT_MIX.value: + return ACTAttentionMix() + if kind == LayerKind.MHA_JOIN.value: + hidden_size = params.get("hidden_size") + return ACTMHAJoin( + sequence_length=int(cast(Any, params.get("seq_len", 1))), + hidden_size=int(cast(Any, hidden_size)) if hidden_size is not None else None, + ) + cls = ACT_TO_TORCH.get(kind) if cls is None: if "requires_graph_restoration" in spec.get("params_optional", []): @@ -1051,14 +1255,6 @@ def _build_from_schema(self, act_layer: Layer) -> Optional[nn.Module]: ) return None - if kind == LayerKind.QUANTIZE.value: - return cls( - scale=params.get("scale"), - zero_point=params.get("zero_point"), - qmin=int(cast(Any, params.get("qmin", 0))), - qmax=int(cast(Any, params.get("qmax", 255))), - ) - # Build positional args from params_required (excluding tensors) # Tensors are auto-detected via isinstance() - they go to state_dict, not constructor args = [] @@ -1126,15 +1322,15 @@ def _build_rnn_family(self, act_layer: Layer) -> nn.Module: """ kind = act_layer.kind params = act_layer.params - if int(params.get("num_layers", 1)) != 1: + if int(cast(Any, params.get("num_layers", 1))) != 1: raise ValueError( f"ACTToTorch: {kind} layer {act_layer.id} has num_layers=" f"{params['num_layers']}, only single-layer is supported." ) ctor_kwargs: Dict[str, Any] = { - "input_size": int(params["input_size"]), - "hidden_size": int(params["hidden_size"]), + "input_size": int(cast(Any, params["input_size"])), + "hidden_size": int(cast(Any, params["hidden_size"])), "num_layers": 1, "bidirectional": bool(params.get("bidirectional", False)), "batch_first": bool(params.get("batch_first", False)), diff --git a/act/pipeline/verification/per_neuron_bounds.py b/act/pipeline/verification/per_neuron_bounds.py index 4897b3f2c..3a0895c31 100644 --- a/act/pipeline/verification/per_neuron_bounds.py +++ b/act/pipeline/verification/per_neuron_bounds.py @@ -86,7 +86,6 @@ from act.back_end.core import Bounds, Layer from act.back_end.layer_schema import ( - HOOKABLE_ACTIVATION_KINDS, TRANSFORMER_KINDS, LayerKind, ) @@ -102,6 +101,20 @@ LayerKind.TANH.value: "Tanh", LayerKind.SILU.value: "SiLU", LayerKind.LRELU.value: "LeakyReLU", + LayerKind.SIN.value: "ACTSin", + LayerKind.COS.value: "ACTCos", + LayerKind.ERF.value: "ACTErf", + LayerKind.SQRT.value: "ACTSqrt", + LayerKind.QUANTIZE.value: "ACTQuantize", + LayerKind.ATT_SCORES.value: "ACTAttentionScores", + LayerKind.ATT_MIX.value: "ACTAttentionMix", + LayerKind.MHA_SPLIT.value: "ACTMHASplit", + LayerKind.MHA_JOIN.value: "ACTMHAJoin", + LayerKind.SOFTMAX.value: "Softmax", + LayerKind.LAYERNORM.value: "ACTLayerNorm", + LayerKind.GELU.value: "GELU", + LayerKind.MASK_ADD.value: "ACTMaskAdd", + LayerKind.MATMUL.value: "ACTMatMul", LayerKind.FLATTEN.value: "Flatten", LayerKind.MAXPOOL1D.value: "MaxPool1d", LayerKind.MAXPOOL2D.value: "MaxPool2d", @@ -112,10 +125,57 @@ LayerKind.ADAPTIVEAVGPOOL2D.value: "AdaptiveAvgPool2d", } -_PRE_ACTIVATION_MODULES = frozenset( - _ACT_KIND_TO_MODULE[k] for k in HOOKABLE_ACTIVATION_KINDS +# ``DualSolver`` calls ``compute_forward_bounds(post_activation=False)``. Its +# nonlinear relaxation handlers therefore store the incoming (pre-activation) +# box, while affine, shape, pooling, and bilinear handlers store their output +# box. Keep that distinction in ACT-layer terms: module names are only a +# tracing detail and do not define which tensor a verifier bound represents. +_PRE_ACTIVATION_BOUND_KINDS = frozenset( + { + LayerKind.RELU.value, + LayerKind.SIGMOID.value, + LayerKind.TANH.value, + LayerKind.SILU.value, + LayerKind.LRELU.value, + LayerKind.SIN.value, + LayerKind.COS.value, + LayerKind.ERF.value, + LayerKind.SQRT.value, + LayerKind.QUANTIZE.value, + LayerKind.SOFTMAX.value, + LayerKind.LAYERNORM.value, + LayerKind.GELU.value, + } +) + +_POST_ACTIVATION_BOUND_KINDS = frozenset( + { + LayerKind.DENSE.value, + LayerKind.CONV1D.value, + LayerKind.CONV2D.value, + LayerKind.CONV3D.value, + LayerKind.ATT_SCORES.value, + LayerKind.ATT_MIX.value, + LayerKind.MHA_SPLIT.value, + LayerKind.MHA_JOIN.value, + LayerKind.MASK_ADD.value, + LayerKind.MATMUL.value, + LayerKind.FLATTEN.value, + LayerKind.MAXPOOL1D.value, + LayerKind.MAXPOOL2D.value, + LayerKind.MAXPOOL3D.value, + LayerKind.AVGPOOL1D.value, + LayerKind.AVGPOOL2D.value, + LayerKind.AVGPOOL3D.value, + LayerKind.ADAPTIVEAVGPOOL2D.value, + } ) +assert not (_PRE_ACTIVATION_BOUND_KINDS & _POST_ACTIVATION_BOUND_KINDS) +assert ( + _PRE_ACTIVATION_BOUND_KINDS | _POST_ACTIVATION_BOUND_KINDS +) == frozenset(_ACT_KIND_TO_MODULE) + def check_hookable_alignment(act_net, model: torch.nn.Module) -> Optional[str]: """Return a Level-2 skip reason for structurally un-alignable models. @@ -134,6 +194,12 @@ def check_hookable_alignment(act_net, model: torch.nn.Module) -> Optional[str]: 1 for layer in layers if _ACT_KIND_TO_MODULE.get(layer.kind) in hookable_kinds ) + if hookable_layers == 0: + return ( + "reference model and ACT net expose no 1:1 hookable layers; " + "per-neuron bounds were not checked" + ) + if hookable_modules == hookable_layers: return None @@ -241,7 +307,7 @@ def collect_concrete_activations( errors: List[str] = [] warnings: List[str] = [] call_counts: Dict[int, int] = {} - hookable_events: List[Tuple[str, torch.Tensor]] = [] + hookable_events: List[Tuple[str, Any, Any]] = [] hooks = [] def _hook(module, inputs, output): @@ -250,11 +316,8 @@ def _hook(module, inputs, output): if strict_single_call_per_module and call_counts[module_id] > 1: errors.append(f"Module called multiple times: {module.__class__.__name__}") module_type = module.__class__.__name__ - tensor_source = inputs[0] if pre_activation and module_type in _PRE_ACTIVATION_MODULES else output - if not torch.is_tensor(tensor_source): - warnings.append(f"Non-tensor activation from {module_type}") - return - hookable_events.append((module_type, tensor_source.detach())) + module_input = inputs[0] if inputs else None + hookable_events.append((module_type, module_input, output)) hookable_kinds = set(_ACT_KIND_TO_MODULE.values()) @@ -314,7 +377,7 @@ def _drop_batch_if_and_only_if_batch1( for idx, layer in enumerate(hookable_layers): if idx >= len(hookable_events): break - module_type, tensor = hookable_events[idx] + module_type, module_input, module_output = hookable_events[idx] expected = _ACT_KIND_TO_MODULE.get(layer.kind) if expected is None: errors.append( @@ -324,6 +387,18 @@ def _drop_batch_if_and_only_if_batch1( errors.append( f"Kind/type mismatch at position {idx}: act_kind={layer.kind} event_type={module_type}" ) + tensor_source = ( + module_input + if pre_activation and layer.kind in _PRE_ACTIVATION_BOUND_KINDS + else module_output + ) + if not torch.is_tensor(tensor_source): + errors.append( + f"Non-tensor activation at layer_id={layer.id}: " + f"kind={layer.kind} module={module_type}" + ) + continue + tensor = tensor_source.detach() expected_shape = None params = getattr(layer, "params", {}) or {} diff --git a/act/pipeline/verification/validate_verifier.py b/act/pipeline/verification/validate_verifier.py index 9209804e7..d1eea42c8 100644 --- a/act/pipeline/verification/validate_verifier.py +++ b/act/pipeline/verification/validate_verifier.py @@ -757,7 +757,20 @@ def _bounds_record(**fields) -> Dict[str, Any]: samples_processed=sample_idx, ) - if violations: + # Never turn an empty hook trace into a green soundness result. + if total_checks == 0: + result = _bounds_record( + validation_status="SKIPPED", + explanation=( + "⏭️ SKIPPED: per-neuron validation produced zero bound checks; " + "no soundness claim was made" + ), + total_checks=0, + violations=[], + per_neuron_config={"topk": per_neuron_config.topk}, + ) + logger.info(f"\n {result['explanation']}") + elif violations: result = _bounds_record( validation_status="FAILED", explanation=f"🚨 UNSOUND BOUNDS: {len(violations)} violations found across {num_samples} samples", @@ -987,6 +1000,8 @@ def _print_summary(self, summary: Dict[str, Any]): print(f"\n⚠️ All {validation_type} validation tests encountered errors!") print("This indicates pre-existing bugs in the verification backend.") print() + elif validation_type == "bounds" and summary.get("total_checks", 0) == 0: + print("\n⏭️ BOUNDS validation SKIPPED: no bound checks were performed.") else: print(f"\n✅ {validation_type.upper()} validation PASSED!") From 14f0e12f282f18de73a894b7499e1264f8d5f76f Mon Sep 17 00:00:00 2001 From: guanqin-123 Date: Fri, 28 Aug 2026 15:44:23 +1000 Subject: [PATCH 03/10] ci(pipeline): cover hybridz ViT verification Measured +164 repo-wide executed lines in 3 seconds over the 9,085-line combined baseline of the existing pipeline-verify commands. --- .github/workflows/act-pipeline-verify.yml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/.github/workflows/act-pipeline-verify.yml b/.github/workflows/act-pipeline-verify.yml index 34afee476..d34cdfba0 100644 --- a/.github/workflows/act-pipeline-verify.yml +++ b/.github/workflows/act-pipeline-verify.yml @@ -4,7 +4,7 @@ name: ACT Pipeline Verify Tests # One step per benchmark; each step iterates the (TF, Solver) combos it # supports. VNNLIB benchmarks (vnncomp2024 subset): acasxu_2023, dist_shift_2023, # safenlp_2024 run all three combos (interval/hybridz/dual); collins_rul_cnn_2022 -# runs dual only; vit_2023 (ViT) runs interval + dual. +# runs dual only; vit_2023 (ViT) runs interval + hybridz + dual. # TorchVision MNIST + # simple_cnn runs all three combos, exercising TOP1_ROBUST + MARGIN_ROBUST spec # kinds. Factory-network verification lives in the backend CIs. @@ -118,6 +118,11 @@ jobs: coverage run -p -m act.pipeline --verify vnnlib --category vit_2023 --max-instances 1 $combo --validate-soundness --device cpu --dtype float64 done + - name: Verify vit_2023 with hybridz transformer propagation + run: | + cd ${{ github.workspace }} + python -m coverage run -p -m act.pipeline --verify vnnlib --category vit_2023 --max-instances 1 --tf-modes hybridz --solvers torchlp --device cpu --dtype float64 + - name: Verify TorchVision MNIST + simple_cnn (interval / hybridz / dual — TOP1_ROBUST + MARGIN_ROBUST spec coverage) run: | cd ${{ github.workspace }} From b3d3d9dda503985cdc9d7d1efc90deb764593469 Mon Sep 17 00:00:00 2001 From: guanqin-123 Date: Fri, 28 Aug 2026 16:40:03 +1000 Subject: [PATCH 04/10] feat(back_end): generate an attention net for dual coverage No generated network contained ATT_SCORES or ATT_MIX, and dual_tf's forward_attention/backward_attention handle only those two kinds, so the backend jobs' existing dual sweep could never reach them. MATMUL already had cover via layer_testing_matmul; the attention cores had none. layer_testing_attention lowers DENSE Q/K/V into ATT_SCORES -> CONCAT -> SOFTMAX -> ATT_MIX -> CONCAT -> LAYERNORM -> GELU. Q/K/V come from DENSE rather than an MHA_SPLIT decomposition because the dual path stubs MHA split/join and consumes the bilinear cores directly. dual_tf/tf_transformer.py goes from 72.07% to 90.4% (36 missing, was 69). Both dtypes report 0 violations and the tf_sin unsoundness probe is still caught. Picked up by the existing sweep with no workflow change. --- act/back_end/net_factory.py | 180 ++++++++++++++++++++++++++++++++++-- act/config/gen_act_net.yaml | 24 ++++- 2 files changed, 195 insertions(+), 9 deletions(-) diff --git a/act/back_end/net_factory.py b/act/back_end/net_factory.py index e0e81af19..38ce0dbec 100644 --- a/act/back_end/net_factory.py +++ b/act/back_end/net_factory.py @@ -17,6 +17,8 @@ # Families: mlp (plain/block/residual), cnn2d (plain/residual/stage) # ===---------------------------------------------------------------------===# +# pyright: reportConstantRedefinition=false + from __future__ import annotations import functools @@ -28,7 +30,7 @@ import random import secrets from pathlib import Path -from typing import Any, Dict, FrozenSet, List, Optional, Tuple +from typing import Any, cast, Dict, FrozenSet, List, Optional, Tuple import torch # pyright: ignore[reportMissingImports] @@ -867,6 +869,16 @@ def _generate_layer_variables(kind, i, vc, params, layers): n = torch.Size(shape).numel() return [], list(range(vc, vc + n)), vc + n + # Scalar attention cores contract two predecessor vectors. Their source + # variable lists are populated by create_network from q_src/k_src or + # w_src/v_src before variable allocation. + if kind == LayerKind.ATT_SCORES.value: + in_vars = list(params["q_vars"]) + list(params["k_vars"]) + return in_vars, [vc], vc + 1 + if kind == LayerKind.ATT_MIX.value: + in_vars = list(params["w_vars"]) + list(params["v_vars"]) + return in_vars, [vc], vc + 1 + # Binary ops (x_vars + y_vars already populated by create_network) x_vars = params.get("x_vars", []) y_vars = params.get("y_vars", []) @@ -1455,6 +1467,13 @@ def create_network(self, name: str, spec: Dict[str, Any]) -> Net: if "preds" in ls and "preds_indices" not in params: params["preds_indices"] = ls["preds"] + if kind == LayerKind.ATT_SCORES.value: + params["q_vars"] = list(layers[int(params["q_src"])].out_vars) + params["k_vars"] = list(layers[int(params["k_src"])].out_vars) + elif kind == LayerKind.ATT_MIX.value: + params["w_vars"] = list(layers[int(params["w_src"])].out_vars) + params["v_vars"] = list(layers[int(params["v_src"])].out_vars) + if kind in (LayerKind.MAX.value, LayerKind.MIN.value): pred_indices = ls.get("preds", []) if pred_indices: @@ -1464,9 +1483,16 @@ def create_network(self, name: str, spec: Dict[str, Any]) -> Net: if p < len(layers) ] - in_vars, out_vars, vc = _generate_layer_variables( - kind, i, vc, params, layers - ) + input_from = ls.get("input_from") + if input_from is not None: + in_vars = list(layers[int(input_from)].out_vars) + n_out = int(params.get("out_features", len(in_vars))) + out_vars = list(range(vc, vc + n_out)) + vc += n_out + else: + in_vars, out_vars, vc = _generate_layer_variables( + kind, i, vc, params, layers + ) if kind == LayerKind.INPUT.value: params["dtype"] = dtype_str @@ -1477,7 +1503,8 @@ def create_network(self, name: str, spec: Dict[str, Any]) -> Net: elif kind == LayerKind.ASSERT.value: # B from the InputLayer (layers[0]); n_out from this ASSERT's # in_vars (which equal the upstream output variables). - B_assert = int(layers[0].params["shape"][0]) + input_shape = cast(List[int], cast(object, layers[0].params["shape"])) + B_assert = int(input_shape[0]) params = self._assert_params( params, dtype, B=B_assert, n_out=len(in_vars), ) @@ -1614,8 +1641,10 @@ def generate(self) -> List[str]: for idx in range(self.num_instances): self._generate_one(idx, dtype, names) + dsl_layer_testing = self.config.get("layer_testing", {}) print( - f"Generating {len(LAYER_TESTING_SPECS)} per-kind layer-testing examples..." + f"Generating {len(LAYER_TESTING_SPECS) + len(dsl_layer_testing)} " + "layer-testing examples..." ) names.extend(self._generate_layer_testing_examples()) @@ -1634,6 +1663,15 @@ def _generate_layer_testing_examples(self) -> List[str]: names.append(name) self.total_generated += 1 self._record(net) + for architecture, cfg in self.config.get("layer_testing", {}).items(): + if architecture != "attention": + raise ValueError(f"Unsupported layer-testing architecture: {architecture}") + name = f"{LAYER_TESTING_NAME_PREFIX}{architecture}" + net = self.create_network(name, _lt_spec_attention(cfg)) + self.save_network(net, name) + names.append(name) + self.total_generated += 1 + self._record(net) return names @@ -1825,6 +1863,136 @@ def _lt_spec_matmul() -> Dict[str, Any]: ]} +def _lt_spec_attention(cfg: Dict[str, Any]) -> Dict[str, Any]: + """Small explicit attention block for the dual bilinear core kernels.""" + B = int(cfg["batch_size"]) + L = int(cfg["sequence_length"]) + D = int(cfg["hidden_size"]) + if B != 1 or L <= 1 or D <= 1: + raise ValueError("attention layer-testing architecture requires B=1 and L,D > 1") + + dtype = get_default_dtype() + scale = float(cfg["projection_scale"]) + seeds = [int(seed) for seed in cfg["projection_seeds"]] + if len(seeds) != 3: + raise ValueError("attention projection_seeds must contain Q, K, and V seeds") + weights = [ + ( + torch.randn( + D, + D, + dtype=dtype, + device="cpu", + generator=torch.Generator(device="cpu").manual_seed(seed), + ) + * scale + ).to(get_default_device()) + for seed in seeds + ] + Wq, Wk, Wv = weights + n_in = L * D + lb, ub = (float(v) for v in cfg["input_bounds"]) + layers = _lt_input([B, n_in], lb, ub) + + def dense_projection(weight: torch.Tensor, position: int) -> int: + full = torch.zeros(D, n_in, dtype=dtype) + full[:, position * D:(position + 1) * D] = weight + layers.append({ + "kind": LayerKind.DENSE.value, + "params": { + "weight": full, + "in_features": n_in, + "out_features": D, + "weight_pos": full.clamp(min=0), + "weight_neg": full.clamp(max=0), + "bias": torch.zeros(D, dtype=dtype), + "input_shape": [n_in], + }, + "input_from": 1, + "preds": [1], + }) + return len(layers) - 1 + + def value_projection(feature: int) -> int: + full = torch.zeros(L, n_in, dtype=dtype) + for position in range(L): + full[position, position * D:(position + 1) * D] = Wv[feature] + layers.append({ + "kind": LayerKind.DENSE.value, + "params": { + "weight": full, + "in_features": n_in, + "out_features": L, + "weight_pos": full.clamp(min=0), + "weight_neg": full.clamp(max=0), + "bias": torch.zeros(L, dtype=dtype), + "input_shape": [n_in], + }, + "input_from": 1, + "preds": [1], + }) + return len(layers) - 1 + + q_ids = [dense_projection(Wq, position) for position in range(L)] + k_ids = [dense_projection(Wk, position) for position in range(L)] + v_ids = [value_projection(feature) for feature in range(D)] + + score_ids = [] + for key_position in range(L): + q_src, k_src = q_ids[0], k_ids[key_position] + layers.append({ + "kind": LayerKind.ATT_SCORES.value, + "params": {"dk": math.sqrt(D), "q_src": q_src, "k_src": k_src}, + "preds": [q_src, k_src], + }) + score_ids.append(len(layers) - 1) + layers.append({ + "kind": LayerKind.CONCAT.value, + "params": {"concat_dim": -1}, + "preds": score_ids, + }) + concat_scores = len(layers) - 1 + layers.append({ + "kind": LayerKind.SOFTMAX.value, + "params": {"axis": -1}, + "preds": [concat_scores], + }) + softmax_id = len(layers) - 1 + + mix_ids = [] + for value_id in v_ids: + layers.append({ + "kind": LayerKind.ATT_MIX.value, + "params": { + "rowsize": L, + "w_src": softmax_id, + "v_src": value_id, + }, + "preds": [softmax_id, value_id], + }) + mix_ids.append(len(layers) - 1) + layers.append({ + "kind": LayerKind.CONCAT.value, + "params": {"concat_dim": -1}, + "preds": mix_ids, + }) + concat_mix = len(layers) - 1 + layers.extend([ + { + "kind": LayerKind.LAYERNORM.value, + "params": { + "gamma": torch.ones(D, dtype=dtype), + "beta": torch.zeros(D, dtype=dtype), + "variant": str(cfg["layernorm_variant"]), + }, + "preds": [concat_mix], + }, + {"kind": LayerKind.GELU.value, "params": {}}, + _lt_assert_le([1.0] * D, float(cfg["assert_threshold"])), + ]) + return {"layers": layers} + + def _lt_spec_arg_extremum() -> Dict[str, Any]: return {"layers": _lt_input([1, 2, 3], -1.0, 1.0) + [ {"kind": LayerKind.ARG_EXTREMUM.value, diff --git a/act/config/gen_act_net.yaml b/act/config/gen_act_net.yaml index 2e8375072..ec333e6c5 100644 --- a/act/config/gen_act_net.yaml +++ b/act/config/gen_act_net.yaml @@ -384,7 +384,25 @@ net_factory: # ============================================================================ - # 4. INPUT SPECIFICATION (INPUT_SPEC layer) + # 4. DETERMINISTIC LAYER-TESTING ARCHITECTURES + # ============================================================================ + # These architectures are emitted alongside the sampled families so the + # manifest-driven netfactory sweep exercises them without workflow changes. + + layer_testing: + attention: + batch_size: 1 + sequence_length: 2 + hidden_size: 2 + input_bounds: [-0.07, 0.07] + projection_scale: 0.2 + projection_seeds: [71, 72, 73] + layernorm_variant: no_var + assert_threshold: 100.0 + + + # ============================================================================ + # 5. INPUT SPECIFICATION (INPUT_SPEC layer) # ============================================================================ # Defines the input region that verification will analyze. # Every generated network gets exactly one INPUT_SPEC. @@ -416,7 +434,7 @@ net_factory: # ============================================================================ - # 5. OUTPUT SPECIFICATION (ASSERT layer) + # 6. OUTPUT SPECIFICATION (ASSERT layer) # ============================================================================ # Defines the verification property the network output must satisfy. # Every generated network gets exactly one ASSERT. @@ -459,7 +477,7 @@ net_factory: # ============================================================================ - # 6. VALIDATE-VERIFIER DEFAULTS + # 7. VALIDATE-VERIFIER DEFAULTS # ============================================================================ # Defaults consumed by `python -m act.pipeline --verify netfactory --validate-soundness ...` # when the corresponding CLI flag is NOT explicitly passed. Any CLI flag From c56b7e49466251dd5aac4047683667443206191a Mon Sep 17 00:00:00 2001 From: guanqin-123 Date: Fri, 28 Aug 2026 16:45:51 +1000 Subject: [PATCH 05/10] fix(back_end): commit generated attention fixture Commit the generated attention network and manifest entry omitted from b3d3d9d. Dual-transformer coverage moved from 271/376 to 340/376 executable lines, a +69-line delta, and both dtypes complete with zero soundness violations. --- .../examples/nets/_meta/manifest.json | 85 ++ .../nets/layer_testing_attention.json | 815 ++++++++++++++++++ 2 files changed, 900 insertions(+) create mode 100644 act/back_end/examples/nets/_meta/manifest.json create mode 100644 act/back_end/examples/nets/layer_testing_attention.json diff --git a/act/back_end/examples/nets/_meta/manifest.json b/act/back_end/examples/nets/_meta/manifest.json new file mode 100644 index 000000000..7832a9775 --- /dev/null +++ b/act/back_end/examples/nets/_meta/manifest.json @@ -0,0 +1,85 @@ +{ + "base_seed": 42, + "num_instances": 15, + "name_prefix": "cfg_seed", + "nets": [ + "resnet_4x1x8x8_8x1x1_3104358145", + "mlp_block_4x16_32x1_1568868034", + "resnet_4x3x16x16_16x1x2_971177790", + "cnn2d_plain_4x3x16x16_16x32x8_1647068278", + "resnet_4x1x8x8_16x1x1_3502118747", + "cnn2d_plain_1x8x8_8_322351658", + "mlp_block_16_32x2_96032213", + "cnn2d_plain_4x1x8x8_32x8x16_4023708073", + "resnet_3x16x16_16x1x1_2227738452", + "mlp_plain_4x6_64x32_1193746778", + "cnn2d_plain_3x16x16_8_2362549719", + "mlp_plain_3x8_64x64_3962224133", + "resnet_1x8x8_8x2x2_2752651", + "mlp_plain_4x6_32x32x32_1301097020", + "resnet_4x3x16x16_8x2x1_1277797607", + "layer_testing_constant", + "layer_testing_add_dual", + "layer_testing_sign", + "layer_testing_reduce_sum", + "layer_testing_compare", + "layer_testing_where", + "layer_testing_matmul", + "layer_testing_arg_extremum", + "layer_testing_upsample", + "layer_testing_expand", + "layer_testing_scatter_nd", + "layer_testing_slice", + "layer_testing_gather", + "layer_testing_reshape", + "layer_testing_transpose", + "layer_testing_squeeze", + "layer_testing_unsqueeze", + "layer_testing_lstm", + "layer_testing_gru", + "layer_testing_rnn", + "layer_testing_gelu", + "layer_testing_softmax", + "layer_testing_layernorm", + "layer_testing_posenc", + "layer_testing_mask_add", + "layer_testing_conv1d", + "layer_testing_conv3d", + "layer_testing_conv_transpose_2d", + "layer_testing_cnn_pool", + "layer_testing_sub", + "layer_testing_div", + "layer_testing_bn", + "layer_testing_abs", + "layer_testing_bias", + "layer_testing_scale", + "layer_testing_relu6", + "layer_testing_hardtanh", + "layer_testing_hardsigmoid", + "layer_testing_hardswish", + "layer_testing_mish", + "layer_testing_softsign", + "layer_testing_square", + "layer_testing_pow", + "layer_testing_erf", + "layer_testing_sqrt", + "layer_testing_sin", + "layer_testing_cos", + "layer_testing_quantize", + "layer_testing_tanh", + "layer_testing_sigmoid", + "layer_testing_lrelu", + "layer_testing_max_op", + "layer_testing_min_op", + "layer_testing_bab_deep", + "layer_testing_lin_poly", + "layer_testing_margin_robust", + "layer_testing_top1_robust", + "layer_testing_range", + "layer_testing_unsafe_linear", + "layer_testing_attention" + ], + "tf_targets": null, + "registry_mode": "intersection", + "allowed_layers_count": 47 +} \ No newline at end of file diff --git a/act/back_end/examples/nets/layer_testing_attention.json b/act/back_end/examples/nets/layer_testing_attention.json new file mode 100644 index 000000000..9a5b7061b --- /dev/null +++ b/act/back_end/examples/nets/layer_testing_attention.json @@ -0,0 +1,815 @@ +{ + "format_version": "2.0", + "act_net": { + "layers": [ + { + "id": 0, + "kind": "INPUT", + "params": { + "shape": [ + 1, + 4 + ], + "dtype": "torch.float64" + }, + "in_vars": [], + "out_vars": [ + 0, + 1, + 2, + 3 + ], + "cache": {} + }, + { + "id": 1, + "kind": "INPUT_SPEC", + "params": { + "kind": "BOX", + "lb_val": -0.07, + "ub_val": 0.07, + "lb": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDEsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIArsUbgeheuxv+xRuB6F67G/7FG4HoXrsb/sUbgeheuxvw==", + "dtype": "torch.float64", + "shape": [ + 1, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "ub": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDEsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIArsUbgeheuxP+xRuB6F67E/7FG4HoXrsT/sUbgeheuxPw==", + "dtype": "torch.float64", + "shape": [ + 1, + 4 + ], + "device": "cpu", + "requires_grad": false + } + }, + "in_vars": [ + 0, + 1, + 2, + 3 + ], + "out_vars": [ + 0, + 1, + 2, + 3 + ], + "cache": {} + }, + { + "id": 2, + "kind": "DENSE", + "params": { + "weight": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAo9q7IbzA/UP+gUG5qqs74/AAAAAAAAAAAAAAAAAAAAAJs4USanw7O/1KKEhQlM3b8AAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "in_features": 4, + "out_features": 2, + "weight_pos": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAo9q7IbzA/UP+gUG5qqs74/AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "weight_neg": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAJs4USanw7O/1KKEhQlM3b8AAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "bias": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2 + ], + "device": "cpu", + "requires_grad": false + }, + "input_shape": [ + 4 + ] + }, + "in_vars": [ + 0, + 1, + 2, + 3 + ], + "out_vars": [ + 4, + 5 + ], + "cache": {} + }, + { + "id": 3, + "kind": "DENSE", + "params": { + "weight": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAPauyG8wP1D/oFBuaqrO+PwAAAAAAAAAAAAAAAAAAAACbOFEmp8Ozv9SihIUJTN2/", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "in_features": 4, + "out_features": 2, + "weight_pos": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAPauyG8wP1D/oFBuaqrO+PwAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "weight_neg": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAACbOFEmp8Ozv9SihIUJTN2/", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "bias": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2 + ], + "device": "cpu", + "requires_grad": false + }, + "input_shape": [ + 4 + ] + }, + "in_vars": [ + 0, + 1, + 2, + 3 + ], + "out_vars": [ + 6, + 7 + ], + "cache": {} + }, + { + "id": 4, + "kind": "DENSE", + "params": { + "weight": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAqN2bckV5rJvzHL6bWgj8K/AAAAAAAAAAAAAAAAAAAAABruJLusObK/Zx+2Vue0q78AAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "in_features": 4, + "out_features": 2, + "weight_pos": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "weight_neg": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAqN2bckV5rJvzHL6bWgj8K/AAAAAAAAAAAAAAAAAAAAABruJLusObK/Zx+2Vue0q78AAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "bias": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2 + ], + "device": "cpu", + "requires_grad": false + }, + "input_shape": [ + 4 + ] + }, + "in_vars": [ + 0, + 1, + 2, + 3 + ], + "out_vars": [ + 8, + 9 + ], + "cache": {} + }, + { + "id": 5, + "kind": "DENSE", + "params": { + "weight": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAjdm3JFeayb8xy+m1oI/CvwAAAAAAAAAAAAAAAAAAAAAa7iS7rDmyv2cftlbntKu/", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "in_features": 4, + "out_features": 2, + "weight_pos": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "weight_neg": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAjdm3JFeayb8xy+m1oI/CvwAAAAAAAAAAAAAAAAAAAAAa7iS7rDmyv2cftlbntKu/", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "bias": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2 + ], + "device": "cpu", + "requires_grad": false + }, + "input_shape": [ + 4 + ] + }, + "in_vars": [ + 0, + 1, + 2, + 3 + ], + "out_vars": [ + 10, + 11 + ], + "cache": {} + }, + { + "id": 6, + "kind": "DENSE", + "params": { + "weight": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAqWNQakPziIP8SuqNehwrY/AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAACWNQakPziIP8SuqNehwrY/", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "in_features": 4, + "out_features": 2, + "weight_pos": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAqWNQakPziIP8SuqNehwrY/AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAACWNQakPziIP8SuqNehwrY/", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "weight_neg": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "bias": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2 + ], + "device": "cpu", + "requires_grad": false + }, + "input_shape": [ + 4 + ] + }, + "in_vars": [ + 0, + 1, + 2, + 3 + ], + "out_vars": [ + 12, + 13 + ], + "cache": {} + }, + { + "id": 7, + "kind": "DENSE", + "params": { + "weight": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAqynq4MLSbPv82J7FtuNdE/AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAACynq4MLSbPv82J7FtuNdE/", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "in_features": 4, + "out_features": 2, + "weight_pos": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAM2J7FtuNdE/AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAM2J7FtuNdE/", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "weight_neg": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAqynq4MLSbPvwAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAACynq4MLSbPvwAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2, + 4 + ], + "device": "cpu", + "requires_grad": false + }, + "bias": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2 + ], + "device": "cpu", + "requires_grad": false + }, + "input_shape": [ + 4 + ] + }, + "in_vars": [ + 0, + 1, + 2, + 3 + ], + "out_vars": [ + 14, + 15 + ], + "cache": {} + }, + { + "id": 8, + "kind": "ATT_SCORES", + "params": { + "dk": 1.4142135623730951, + "q_src": 2, + "k_src": 4, + "q_vars": [ + 4, + 5 + ], + "k_vars": [ + 8, + 9 + ] + }, + "in_vars": [ + 4, + 5, + 8, + 9 + ], + "out_vars": [ + 16 + ], + "cache": {} + }, + { + "id": 9, + "kind": "ATT_SCORES", + "params": { + "dk": 1.4142135623730951, + "q_src": 2, + "k_src": 5, + "q_vars": [ + 4, + 5 + ], + "k_vars": [ + 10, + 11 + ] + }, + "in_vars": [ + 4, + 5, + 10, + 11 + ], + "out_vars": [ + 17 + ], + "cache": {} + }, + { + "id": 10, + "kind": "CONCAT", + "params": { + "concat_dim": -1 + }, + "in_vars": [ + 16, + 17 + ], + "out_vars": [ + 18, + 19 + ], + "cache": {} + }, + { + "id": 11, + "kind": "SOFTMAX", + "params": { + "axis": -1 + }, + "in_vars": [ + 18, + 19 + ], + "out_vars": [ + 20, + 21 + ], + "cache": {} + }, + { + "id": 12, + "kind": "ATT_MIX", + "params": { + "rowsize": 2, + "w_src": 11, + "v_src": 6, + "w_vars": [ + 20, + 21 + ], + "v_vars": [ + 12, + 13 + ] + }, + "in_vars": [ + 20, + 21, + 12, + 13 + ], + "out_vars": [ + 22 + ], + "cache": {} + }, + { + "id": 13, + "kind": "ATT_MIX", + "params": { + "rowsize": 2, + "w_src": 11, + "v_src": 7, + "w_vars": [ + 20, + 21 + ], + "v_vars": [ + 14, + 15 + ] + }, + "in_vars": [ + 20, + 21, + 14, + 15 + ], + "out_vars": [ + 23 + ], + "cache": {} + }, + { + "id": 14, + "kind": "CONCAT", + "params": { + "concat_dim": -1 + }, + "in_vars": [ + 22, + 23 + ], + "out_vars": [ + 24, + 25 + ], + "cache": {} + }, + { + "id": 15, + "kind": "LAYERNORM", + "params": { + "gamma": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAADwPwAAAAAAAPA/", + "dtype": "torch.float64", + "shape": [ + 2 + ], + "device": "cpu", + "requires_grad": false + }, + "beta": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", + "dtype": "torch.float64", + "shape": [ + 2 + ], + "device": "cpu", + "requires_grad": false + }, + "variant": "no_var" + }, + "in_vars": [ + 24, + 25 + ], + "out_vars": [ + 26, + 27 + ], + "cache": {} + }, + { + "id": 16, + "kind": "GELU", + "params": {}, + "in_vars": [ + 26, + 27 + ], + "out_vars": [ + 28, + 29 + ], + "cache": {} + }, + { + "id": 17, + "kind": "ASSERT", + "params": { + "kind": "LINEAR_LE", + "c": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDEsIDIpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAADwPwAAAAAAAPA/", + "dtype": "torch.float64", + "shape": [ + 1, + 2 + ], + "device": "cpu", + "requires_grad": false + }, + "d": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDEsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAABZQA==", + "dtype": "torch.float64", + "shape": [ + 1 + ], + "device": "cpu", + "requires_grad": false + }, + "C": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDEsIDIpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAADwPwAAAAAAAPA/", + "dtype": "torch.float64", + "shape": [ + 1, + 2 + ], + "device": "cpu", + "requires_grad": false + }, + "thresholds": { + "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDEsIDEpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAABZQA==", + "dtype": "torch.float64", + "shape": [ + 1, + 1 + ], + "device": "cpu", + "requires_grad": false + }, + "M": 1 + }, + "in_vars": [ + 28, + 29 + ], + "out_vars": [ + 28, + 29 + ], + "cache": {} + } + ], + "graph": { + "preds": { + "0": [], + "1": [ + 0 + ], + "2": [ + 1 + ], + "3": [ + 1 + ], + "4": [ + 1 + ], + "5": [ + 1 + ], + "6": [ + 1 + ], + "7": [ + 1 + ], + "8": [ + 2, + 4 + ], + "9": [ + 2, + 5 + ], + "10": [ + 8, + 9 + ], + "11": [ + 10 + ], + "12": [ + 11, + 6 + ], + "13": [ + 11, + 7 + ], + "14": [ + 12, + 13 + ], + "15": [ + 14 + ], + "16": [ + 15 + ], + "17": [ + 16 + ] + }, + "succs": { + "0": [ + 1 + ], + "1": [ + 2, + 3, + 4, + 5, + 6, + 7 + ], + "2": [ + 8, + 9 + ], + "3": [], + "4": [ + 8 + ], + "5": [ + 9 + ], + "6": [ + 12 + ], + "7": [ + 13 + ], + "8": [ + 10 + ], + "9": [ + 10 + ], + "10": [ + 11 + ], + "11": [ + 12, + 13 + ], + "12": [ + 14 + ], + "13": [ + 14 + ], + "14": [ + 15 + ], + "15": [ + 16 + ], + "16": [ + 17 + ], + "17": [] + } + } + } +} \ No newline at end of file From 2567418a9a29a4b5448f7d63c47752a499e5bb77 Mon Sep 17 00:00:00 2001 From: guanqin-123 Date: Fri, 28 Aug 2026 17:17:01 +1000 Subject: [PATCH 06/10] ci(back_end): drop the solve-path exception lint It was named a soundness gate but only ever flagged one syntactic shape: try/except wrapped directly around setup_and_solve_batch or solve_batch. An exception swallowed inside solve_batch's own body, or in a caller of verify_once, is equally fatal and invisible to it. It never fired, and the shape it guards is one review catches. Twenty-five lines of inline YAML Python for that is not worth carrying. --- .github/workflows/act-bab.yml | 33 --------------------------------- 1 file changed, 33 deletions(-) diff --git a/.github/workflows/act-bab.yml b/.github/workflows/act-bab.yml index d25b05a07..e88eda937 100644 --- a/.github/workflows/act-bab.yml +++ b/.github/workflows/act-bab.yml @@ -45,39 +45,6 @@ jobs: python -m pip install --upgrade pip pip install coverage torch onnx onnx2torch "onnx-simplifier" "onnxsim==0.6.5" pandas numpy scipy pyyaml tqdm psutil - # ── Solve path must not swallow solver exceptions ────────────────── - # Replaces the former _test_bab_oom_fails_loud self-test. That test only - # covered the one path reachable from its fixture; this covers every - # call site. A real OOM cannot be triggered deterministically in CI, so - # the invariant is checked structurally instead of at runtime. - - name: BaB soundness — no exception swallowing on the solve path - run: | - cd ${{ github.workspace }} - python - act/back_end/bab/bab.py act/back_end/verifier.py <<'PY' - import ast, sys - GUARDED = {"setup_and_solve_batch", "solve_batch"} - def called(node): - for sub in ast.walk(node): - fn = getattr(sub, "func", None) - name = getattr(fn, "attr", None) or getattr(fn, "id", None) - if isinstance(sub, ast.Call) and name in GUARDED: - yield name - bad = sorted({ - (path, node.lineno, name) - for path in sys.argv[1:] - for node in ast.walk(ast.parse(open(path).read())) - if isinstance(node, ast.Try) - for stmt in node.body for name in called(stmt) - }) - for path, lineno, name in bad: - print(f"{path}:{lineno}: solver call {name!r} sits inside try/except") - if bad: - print("\nA swallowed solver exception turns resource exhaustion into " - "'not provable'. If an unproven lane is then pruned, BaB reports " - "CERTIFIED for a box it never solved. Let it propagate.") - sys.exit(1 if bad else 0) - PY - # ── BaB module unit tests ────────────────────────────────────────── - name: BaB module run: | From 83ce9d6f5b4045b9ce91a1c59ea519be971bf394 Mon Sep 17 00:00:00 2001 From: guanqin-123 Date: Fri, 28 Aug 2026 17:43:25 +1000 Subject: [PATCH 07/10] fix(back_end): degenerate dot-product guard dropped the perturbation _dot_product_degenerate is documented as the closed-form box product for when there is no perturbation dimension, but both callers guarded it with dim_in == 1 rather than dim_in == 0. Since dim_in is embed_dim * perturbed_words, dim_in == 1 is one genuinely perturbed coordinate, and the helper zeroes lw/uw and multiplies only the bias terms, discarding the lw . x^r contribution entirely. Reproduction: for z1 = 2x and z2 = 3x over x in [-1, 1], dot_product returned [0, 0] while the true range of 6x^2 is [0, 6] -- the abstract bound excluded most of the reachable set. Routing dim_in == 1 through _dot_product_planes yields [-18, 6], looser but sound. Not reachable from any current end-to-end path, since attn_mode is never set in production, but it would have become a false-CERTIFIED source the moment the dual-planar route was wired up. --- act/back_end/interval_tf/tf_attention.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/act/back_end/interval_tf/tf_attention.py b/act/back_end/interval_tf/tf_attention.py index 10ad21fbf..6cafe470f 100644 --- a/act/back_end/interval_tf/tf_attention.py +++ b/act/back_end/interval_tf/tf_attention.py @@ -461,7 +461,7 @@ def dot_product(self, other: "LinearBounds") -> "LinearBounds": Implements the dual-norm linear bound of the multi-head dot-product: one valid plane per side, summed over the head dimension. """ - if self.dim_in == 1: + if self.dim_in == 0: return self._dot_product_degenerate(other) return self._dot_product_planes(other, z=False) @@ -473,7 +473,7 @@ def dot_product_double( The pair is fused by :func:`fuse_attention_planes`; returning both is load-bearing because the catalytic ReLU acts on their difference. """ - if self.dim_in == 1: + if self.dim_in == 0: degenerate = self._dot_product_degenerate(other) return degenerate, degenerate.clone() return ( From e24b95de2d17cba0f0916883b3d4e51ba84f1b48 Mon Sep 17 00:00:00 2001 From: guanqin-123 Date: Mon, 31 Aug 2026 13:26:42 +1000 Subject: [PATCH 08/10] chore(back_end): untrack the generated attention net c56b7e4 committed layer_testing_attention.json and the manifest into act/back_end/examples/nets, which .gitignore excludes because every net there is a build product of `act.back_end --generate`. The definition already lives in act/config/gen_act_net.yaml. Tracking a generated file also disables .gitignore for it, so a later DSL edit would silently leave the committed copy stale while CI ran the regenerated one. Verified by wiping act/back_end/examples/nets entirely: --generate rebuilds all 75 nets including the attention one, byte-identical, and the dual sweep still picks it up with no --networks flag (0 violations). --- .../examples/nets/_meta/manifest.json | 85 -- .../nets/layer_testing_attention.json | 815 ------------------ 2 files changed, 900 deletions(-) delete mode 100644 act/back_end/examples/nets/_meta/manifest.json delete mode 100644 act/back_end/examples/nets/layer_testing_attention.json diff --git a/act/back_end/examples/nets/_meta/manifest.json b/act/back_end/examples/nets/_meta/manifest.json deleted file mode 100644 index 7832a9775..000000000 --- a/act/back_end/examples/nets/_meta/manifest.json +++ /dev/null @@ -1,85 +0,0 @@ -{ - "base_seed": 42, - "num_instances": 15, - "name_prefix": "cfg_seed", - "nets": [ - "resnet_4x1x8x8_8x1x1_3104358145", - "mlp_block_4x16_32x1_1568868034", - "resnet_4x3x16x16_16x1x2_971177790", - "cnn2d_plain_4x3x16x16_16x32x8_1647068278", - "resnet_4x1x8x8_16x1x1_3502118747", - "cnn2d_plain_1x8x8_8_322351658", - "mlp_block_16_32x2_96032213", - "cnn2d_plain_4x1x8x8_32x8x16_4023708073", - "resnet_3x16x16_16x1x1_2227738452", - "mlp_plain_4x6_64x32_1193746778", - "cnn2d_plain_3x16x16_8_2362549719", - "mlp_plain_3x8_64x64_3962224133", - "resnet_1x8x8_8x2x2_2752651", - "mlp_plain_4x6_32x32x32_1301097020", - "resnet_4x3x16x16_8x2x1_1277797607", - "layer_testing_constant", - "layer_testing_add_dual", - "layer_testing_sign", - "layer_testing_reduce_sum", - "layer_testing_compare", - "layer_testing_where", - "layer_testing_matmul", - "layer_testing_arg_extremum", - "layer_testing_upsample", - "layer_testing_expand", - "layer_testing_scatter_nd", - "layer_testing_slice", - "layer_testing_gather", - "layer_testing_reshape", - "layer_testing_transpose", - "layer_testing_squeeze", - "layer_testing_unsqueeze", - "layer_testing_lstm", - "layer_testing_gru", - "layer_testing_rnn", - "layer_testing_gelu", - "layer_testing_softmax", - "layer_testing_layernorm", - "layer_testing_posenc", - "layer_testing_mask_add", - "layer_testing_conv1d", - "layer_testing_conv3d", - "layer_testing_conv_transpose_2d", - "layer_testing_cnn_pool", - "layer_testing_sub", - "layer_testing_div", - "layer_testing_bn", - "layer_testing_abs", - "layer_testing_bias", - "layer_testing_scale", - "layer_testing_relu6", - "layer_testing_hardtanh", - "layer_testing_hardsigmoid", - "layer_testing_hardswish", - "layer_testing_mish", - "layer_testing_softsign", - "layer_testing_square", - "layer_testing_pow", - "layer_testing_erf", - "layer_testing_sqrt", - "layer_testing_sin", - "layer_testing_cos", - "layer_testing_quantize", - "layer_testing_tanh", - "layer_testing_sigmoid", - "layer_testing_lrelu", - "layer_testing_max_op", - "layer_testing_min_op", - "layer_testing_bab_deep", - "layer_testing_lin_poly", - "layer_testing_margin_robust", - "layer_testing_top1_robust", - "layer_testing_range", - "layer_testing_unsafe_linear", - "layer_testing_attention" - ], - "tf_targets": null, - "registry_mode": "intersection", - "allowed_layers_count": 47 -} \ No newline at end of file diff --git a/act/back_end/examples/nets/layer_testing_attention.json b/act/back_end/examples/nets/layer_testing_attention.json deleted file mode 100644 index 9a5b7061b..000000000 --- a/act/back_end/examples/nets/layer_testing_attention.json +++ /dev/null @@ -1,815 +0,0 @@ -{ - "format_version": "2.0", - "act_net": { - "layers": [ - { - "id": 0, - "kind": "INPUT", - "params": { - "shape": [ - 1, - 4 - ], - "dtype": "torch.float64" - }, - "in_vars": [], - "out_vars": [ - 0, - 1, - 2, - 3 - ], - "cache": {} - }, - { - "id": 1, - "kind": "INPUT_SPEC", - "params": { - "kind": "BOX", - "lb_val": -0.07, - "ub_val": 0.07, - "lb": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDEsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIArsUbgeheuxv+xRuB6F67G/7FG4HoXrsb/sUbgeheuxvw==", - "dtype": "torch.float64", - "shape": [ - 1, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "ub": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDEsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIArsUbgeheuxP+xRuB6F67E/7FG4HoXrsT/sUbgeheuxPw==", - "dtype": "torch.float64", - "shape": [ - 1, - 4 - ], - "device": "cpu", - "requires_grad": false - } - }, - "in_vars": [ - 0, - 1, - 2, - 3 - ], - "out_vars": [ - 0, - 1, - 2, - 3 - ], - "cache": {} - }, - { - "id": 2, - "kind": "DENSE", - "params": { - "weight": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAo9q7IbzA/UP+gUG5qqs74/AAAAAAAAAAAAAAAAAAAAAJs4USanw7O/1KKEhQlM3b8AAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "in_features": 4, - "out_features": 2, - "weight_pos": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAo9q7IbzA/UP+gUG5qqs74/AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "weight_neg": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAJs4USanw7O/1KKEhQlM3b8AAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "bias": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2 - ], - "device": "cpu", - "requires_grad": false - }, - "input_shape": [ - 4 - ] - }, - "in_vars": [ - 0, - 1, - 2, - 3 - ], - "out_vars": [ - 4, - 5 - ], - "cache": {} - }, - { - "id": 3, - "kind": "DENSE", - "params": { - "weight": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAPauyG8wP1D/oFBuaqrO+PwAAAAAAAAAAAAAAAAAAAACbOFEmp8Ozv9SihIUJTN2/", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "in_features": 4, - "out_features": 2, - "weight_pos": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAPauyG8wP1D/oFBuaqrO+PwAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "weight_neg": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAACbOFEmp8Ozv9SihIUJTN2/", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "bias": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2 - ], - "device": "cpu", - "requires_grad": false - }, - "input_shape": [ - 4 - ] - }, - "in_vars": [ - 0, - 1, - 2, - 3 - ], - "out_vars": [ - 6, - 7 - ], - "cache": {} - }, - { - "id": 4, - "kind": "DENSE", - "params": { - "weight": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAqN2bckV5rJvzHL6bWgj8K/AAAAAAAAAAAAAAAAAAAAABruJLusObK/Zx+2Vue0q78AAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "in_features": 4, - "out_features": 2, - "weight_pos": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "weight_neg": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAqN2bckV5rJvzHL6bWgj8K/AAAAAAAAAAAAAAAAAAAAABruJLusObK/Zx+2Vue0q78AAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "bias": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2 - ], - "device": "cpu", - "requires_grad": false - }, - "input_shape": [ - 4 - ] - }, - "in_vars": [ - 0, - 1, - 2, - 3 - ], - "out_vars": [ - 8, - 9 - ], - "cache": {} - }, - { - "id": 5, - "kind": "DENSE", - "params": { - "weight": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAjdm3JFeayb8xy+m1oI/CvwAAAAAAAAAAAAAAAAAAAAAa7iS7rDmyv2cftlbntKu/", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "in_features": 4, - "out_features": 2, - "weight_pos": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "weight_neg": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAjdm3JFeayb8xy+m1oI/CvwAAAAAAAAAAAAAAAAAAAAAa7iS7rDmyv2cftlbntKu/", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "bias": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2 - ], - "device": "cpu", - "requires_grad": false - }, - "input_shape": [ - 4 - ] - }, - "in_vars": [ - 0, - 1, - 2, - 3 - ], - "out_vars": [ - 10, - 11 - ], - "cache": {} - }, - { - "id": 6, - "kind": "DENSE", - "params": { - "weight": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAqWNQakPziIP8SuqNehwrY/AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAACWNQakPziIP8SuqNehwrY/", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "in_features": 4, - "out_features": 2, - "weight_pos": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAqWNQakPziIP8SuqNehwrY/AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAACWNQakPziIP8SuqNehwrY/", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "weight_neg": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "bias": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2 - ], - "device": "cpu", - "requires_grad": false - }, - "input_shape": [ - 4 - ] - }, - "in_vars": [ - 0, - 1, - 2, - 3 - ], - "out_vars": [ - 12, - 13 - ], - "cache": {} - }, - { - "id": 7, - "kind": "DENSE", - "params": { - "weight": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAqynq4MLSbPv82J7FtuNdE/AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAACynq4MLSbPv82J7FtuNdE/", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "in_features": 4, - "out_features": 2, - "weight_pos": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAM2J7FtuNdE/AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAM2J7FtuNdE/", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "weight_neg": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsIDQpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAqynq4MLSbPvwAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAACynq4MLSbPvwAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2, - 4 - ], - "device": "cpu", - "requires_grad": false - }, - "bias": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2 - ], - "device": "cpu", - "requires_grad": false - }, - "input_shape": [ - 4 - ] - }, - "in_vars": [ - 0, - 1, - 2, - 3 - ], - "out_vars": [ - 14, - 15 - ], - "cache": {} - }, - { - "id": 8, - "kind": "ATT_SCORES", - "params": { - "dk": 1.4142135623730951, - "q_src": 2, - "k_src": 4, - "q_vars": [ - 4, - 5 - ], - "k_vars": [ - 8, - 9 - ] - }, - "in_vars": [ - 4, - 5, - 8, - 9 - ], - "out_vars": [ - 16 - ], - "cache": {} - }, - { - "id": 9, - "kind": "ATT_SCORES", - "params": { - "dk": 1.4142135623730951, - "q_src": 2, - "k_src": 5, - "q_vars": [ - 4, - 5 - ], - "k_vars": [ - 10, - 11 - ] - }, - "in_vars": [ - 4, - 5, - 10, - 11 - ], - "out_vars": [ - 17 - ], - "cache": {} - }, - { - "id": 10, - "kind": "CONCAT", - "params": { - "concat_dim": -1 - }, - "in_vars": [ - 16, - 17 - ], - "out_vars": [ - 18, - 19 - ], - "cache": {} - }, - { - "id": 11, - "kind": "SOFTMAX", - "params": { - "axis": -1 - }, - "in_vars": [ - 18, - 19 - ], - "out_vars": [ - 20, - 21 - ], - "cache": {} - }, - { - "id": 12, - "kind": "ATT_MIX", - "params": { - "rowsize": 2, - "w_src": 11, - "v_src": 6, - "w_vars": [ - 20, - 21 - ], - "v_vars": [ - 12, - 13 - ] - }, - "in_vars": [ - 20, - 21, - 12, - 13 - ], - "out_vars": [ - 22 - ], - "cache": {} - }, - { - "id": 13, - "kind": "ATT_MIX", - "params": { - "rowsize": 2, - "w_src": 11, - "v_src": 7, - "w_vars": [ - 20, - 21 - ], - "v_vars": [ - 14, - 15 - ] - }, - "in_vars": [ - 20, - 21, - 14, - 15 - ], - "out_vars": [ - 23 - ], - "cache": {} - }, - { - "id": 14, - "kind": "CONCAT", - "params": { - "concat_dim": -1 - }, - "in_vars": [ - 22, - 23 - ], - "out_vars": [ - 24, - 25 - ], - "cache": {} - }, - { - "id": 15, - "kind": "LAYERNORM", - "params": { - "gamma": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAADwPwAAAAAAAPA/", - "dtype": "torch.float64", - "shape": [ - 2 - ], - "device": "cpu", - "requires_grad": false - }, - "beta": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDIsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAAAAAAAAAAAAAAAA", - "dtype": "torch.float64", - "shape": [ - 2 - ], - "device": "cpu", - "requires_grad": false - }, - "variant": "no_var" - }, - "in_vars": [ - 24, - 25 - ], - "out_vars": [ - 26, - 27 - ], - "cache": {} - }, - { - "id": 16, - "kind": "GELU", - "params": {}, - "in_vars": [ - 26, - 27 - ], - "out_vars": [ - 28, - 29 - ], - "cache": {} - }, - { - "id": 17, - "kind": "ASSERT", - "params": { - "kind": "LINEAR_LE", - "c": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDEsIDIpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAADwPwAAAAAAAPA/", - "dtype": "torch.float64", - "shape": [ - 1, - 2 - ], - "device": "cpu", - "requires_grad": false - }, - "d": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDEsKSwgfSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAABZQA==", - "dtype": "torch.float64", - "shape": [ - 1 - ], - "device": "cpu", - "requires_grad": false - }, - "C": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDEsIDIpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAADwPwAAAAAAAPA/", - "dtype": "torch.float64", - "shape": [ - 1, - 2 - ], - "device": "cpu", - "requires_grad": false - }, - "thresholds": { - "data": "k05VTVBZAQB2AHsnZGVzY3InOiAnPGY4JywgJ2ZvcnRyYW5fb3JkZXInOiBGYWxzZSwgJ3NoYXBlJzogKDEsIDEpLCB9ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAoAAAAAAABZQA==", - "dtype": "torch.float64", - "shape": [ - 1, - 1 - ], - "device": "cpu", - "requires_grad": false - }, - "M": 1 - }, - "in_vars": [ - 28, - 29 - ], - "out_vars": [ - 28, - 29 - ], - "cache": {} - } - ], - "graph": { - "preds": { - "0": [], - "1": [ - 0 - ], - "2": [ - 1 - ], - "3": [ - 1 - ], - "4": [ - 1 - ], - "5": [ - 1 - ], - "6": [ - 1 - ], - "7": [ - 1 - ], - "8": [ - 2, - 4 - ], - "9": [ - 2, - 5 - ], - "10": [ - 8, - 9 - ], - "11": [ - 10 - ], - "12": [ - 11, - 6 - ], - "13": [ - 11, - 7 - ], - "14": [ - 12, - 13 - ], - "15": [ - 14 - ], - "16": [ - 15 - ], - "17": [ - 16 - ] - }, - "succs": { - "0": [ - 1 - ], - "1": [ - 2, - 3, - 4, - 5, - 6, - 7 - ], - "2": [ - 8, - 9 - ], - "3": [], - "4": [ - 8 - ], - "5": [ - 9 - ], - "6": [ - 12 - ], - "7": [ - 13 - ], - "8": [ - 10 - ], - "9": [ - 10 - ], - "10": [ - 11 - ], - "11": [ - 12, - 13 - ], - "12": [ - 14 - ], - "13": [ - 14 - ], - "14": [ - 15 - ], - "15": [ - 16 - ], - "16": [ - 17 - ], - "17": [] - } - } - } -} \ No newline at end of file From 2a937591b83d36c10f81dc23b850886313664727 Mon Sep 17 00:00:00 2001 From: guanqin-123 Date: Mon, 31 Aug 2026 13:32:11 +1000 Subject: [PATCH 09/10] ci(back_end): run the exporter sweep in the float32 job too 32e8f0d replaced cons_exportor's self-tests with a torchlp sweep over the layer_testing nets but only wired it into the float64 job, and the verifier self-test step was later removed from both. float32 was left with neither, so nothing there exercised the LP export path. Measured locally at float32: 60 nets, 0 failures, 246s, comparable to the float64 sweep. --- .github/workflows/act-backend-float32.yml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/.github/workflows/act-backend-float32.yml b/.github/workflows/act-backend-float32.yml index f299ef940..6f4c1c0f5 100644 --- a/.github/workflows/act-backend-float32.yml +++ b/.github/workflows/act-backend-float32.yml @@ -60,6 +60,14 @@ jobs: cd ${{ github.workspace }} coverage run -p -m act.pipeline --verify act2torch --device cpu --dtype float32 + - name: Constraint exporter — torchlp LP export over all layer_testing nets + run: | + cd ${{ github.workspace }} + for f in act/back_end/examples/nets/layer_testing_*.json; do + coverage run -p -m act.back_end --verify --network "$f" \ + --solver torchlp --device cpu --dtype float32 + done + # ───────────────────────────────────────────────────────────────── # Soundness check (TF-agnostic): runs once before per-solver matrix. # See act-backend-float64.yml for the full rationale. From 1becb64e69f632fd6969e5be0e5e152ba97c6ae8 Mon Sep 17 00:00:00 2001 From: guanqin-123 Date: Mon, 31 Aug 2026 16:18:07 +1000 Subject: [PATCH 10/10] refactor(back_end): drop bab.py's self-tests and their CI steps bab.py is production code only now, matching verifier.py. The two check_violations_batched tests, the _TESTS list and the module entry point are gone, so the workflow step that ran the module goes with them, as does the budget-exhaustion gate. What this gives up, measured rather than assumed: stubbing check_violations_batched to always report "no violation" degrades a falsifiable net from FALSIFIED to UNKNOWN, and no remaining check notices -- the netfactory counterexample validation passes because it exercises verify_once, not BaB's counterexample path. Every net CI currently runs through BaB already returns UNKNOWN, so the violation-found branch has no end-to-end cover. Restoring it needs a generated net that BaB actually falsifies, plus a step asserting FALSIFIED. --- .github/workflows/act-bab.yml | 28 --------- act/back_end/bab/bab.py | 111 ---------------------------------- 2 files changed, 139 deletions(-) diff --git a/.github/workflows/act-bab.yml b/.github/workflows/act-bab.yml index e88eda937..c880260d0 100644 --- a/.github/workflows/act-bab.yml +++ b/.github/workflows/act-bab.yml @@ -45,12 +45,6 @@ jobs: python -m pip install --upgrade pip pip install coverage torch onnx onnx2torch "onnx-simplifier" "onnxsim==0.6.5" pandas numpy scipy pyyaml tqdm psutil - # ── BaB module unit tests ────────────────────────────────────────── - - name: BaB module - run: | - cd ${{ github.workspace }} - coverage run -p -m act.back_end.bab.bab - # ── Generate artificial ACT nets (NetFactory) ────────────────────── - name: Cache generated networks id: nets-cache @@ -231,28 +225,6 @@ jobs: coverage run -p -m act.back_end --verify --network act/back_end/examples/nets/layer_testing_bab_deep.json \ --solver dual --method planar --device cpu --dtype float64 - # =================================================================== - # Soundness gate: a BaB run that exhausts its node budget with unproven - # sub-boxes left in the pool MUST report UNKNOWN, never CERTIFIED. Every - # other step here asserts throughput (node counts, exit codes); this is - # the only one asserting the verifier does not claim more than it proved. - # - # layer_testing_bab_deep is certified by presolve and never branches, so - # it cannot exhaust anything -- mlp_plain_3x8 is the net that survives - # presolve and enters BaB. --verbose is load-bearing: backend_cli only - # prints result.metadata under it. - # =================================================================== - - name: BaB soundness — budget exhaustion returns UNKNOWN - run: | - cd ${{ github.workspace }} - out=$(coverage run -p -m act.back_end --verify \ - --network "$ACT_NETS_DIR/mlp_plain_3x8_64x64_3962224133.json" \ - --bab --bab-max-depth 10 --bab-max-subproblems 2 --bab-max-batch-size 1 \ - --solver torchlp --device cpu --dtype float64 --verbose 2>&1) - echo "$out" - grep -q "Lane 0: VerifyStatus.UNKNOWN" <<<"$out" - grep -q "reason: budget_exhausted_with_unproven_subboxes" <<<"$out" - grep -q "exhausted_budget_nodes: True" <<<"$out" # =================================================================== # Dual MATMUL bilinear kernel (tf_transformer): dual-tier soundness on diff --git a/act/back_end/bab/bab.py b/act/back_end/bab/bab.py index 402a749d8..88a76261b 100644 --- a/act/back_end/bab/bab.py +++ b/act/back_end/bab/bab.py @@ -2189,114 +2189,3 @@ def _make_assert_layer(kind: str, params: dict[str, ParamValue], n_out: int) -> in_vars=list(range(n_out)), out_vars=list(range(n_out)), ) - - -def _test_check_violations_batched_per_kind(): # pragma: no cover - y = torch.tensor( - [ - [3.0, 1.0, 0.0, -1.0], - [0.0, 2.0, 1.0, -1.0], - [0.0, 3.0, 1.0, -1.0], - [0.0, 1.0, 3.0, -1.0], - [0.0, 1.0, 4.0, -1.0], - [0.0, 1.0, 2.0, 5.0], - [0.0, 1.0, 2.0, 6.0], - [4.0, 1.0, 2.0, 3.0], - ], - dtype=torch.float64, - ) - net = _IdentityOutput() - n_batch, n_out = y.shape - - top1 = _make_assert_layer( - OutKind.TOP1_ROBUST, - {"y_true": torch.tensor([0, 0, 1, 1, 2, 2, 3, 3])}, - n_out, - ) - y_true_top1 = torch.tensor([0, 0, 1, 1, 2, 2, 3, 3]) - expected_top1 = y.argmax(dim=1) != y_true_top1 - assert torch.equal(check_violations_batched(net, y, top1), expected_top1) - - margin_spec = OutputSpec( - kind=OutKind.MARGIN_ROBUST, - y_true=torch.tensor([0, 0, 1, 1, 2, 2, 3, 3]), - margin=torch.full((n_batch,), 1.5, dtype=y.dtype), - ) - margin_params = margin_spec.encode_linear(n_batch, n_out, y.device, y.dtype) - margin = _make_assert_layer(OutKind.MARGIN_ROBUST, margin_params, n_out) - margin_rows = torch.einsum( - "bmo,bo->bm", margin_params["C"].reshape(n_batch, -1, n_out), y - ) - # encode_linear certifies iff every row C @ y < threshold; violation is the complement. - expected_margin = (margin_rows >= margin_params["thresholds"]).any(dim=1) - assert torch.equal(check_violations_batched(net, y, margin), expected_margin) - - linear = _make_assert_layer( - OutKind.LINEAR_LE, - {"c": torch.ones(n_batch, n_out, dtype=y.dtype), "d": torch.full((n_batch,), 4.0, dtype=y.dtype)}, - n_out, - ) - expected_linear = y.sum(dim=1) >= 4.0 + 1e-8 - assert torch.equal(check_violations_batched(net, y, linear), expected_linear) - - range_layer = _make_assert_layer( - OutKind.RANGE, - { - "lb": torch.full((n_batch, n_out), -0.5, dtype=y.dtype), - "ub": torch.full((n_batch, n_out), 4.5, dtype=y.dtype), - }, - n_out, - ) - expected_range = ((y < -0.5 - 1e-8) | (y > 4.5 + 1e-8)).any(dim=1) - assert torch.equal(check_violations_batched(net, y, range_layer), expected_range) - - c = torch.eye(n_out, dtype=y.dtype).unsqueeze(0).expand(n_batch, -1, -1).contiguous() - d = torch.full((n_batch, n_out), 3.5, dtype=y.dtype) - unsafe = _make_assert_layer( - OutKind.UNSAFE_LINEAR, - {"c": c, "d": d, "C": c.reshape(n_batch * n_out, n_out), "thresholds": d, "M": n_out}, - n_out, - ) - expected_unsafe = (y <= 3.5 + 1e-8).all(dim=1) - assert torch.equal(check_violations_batched(net, y, unsafe), expected_unsafe) - - - -def _test_check_violations_batched_b1_scalar_params(): # pragma: no cover - net = _IdentityOutput() - x = torch.tensor([[0.0, 2.0, 1.0]], dtype=torch.float64) - assert_layer = _make_assert_layer( - OutKind.TOP1_ROBUST, - {"y_true": torch.tensor([0], dtype=torch.long)}, - n_out=3, - ) - result = check_violations_batched(net, x, assert_layer) - assert tuple(result.shape) == (1,) - assert bool(result[0].item()) is True - - - -# --------------------------------------------------------------------------- -_TESTS = [ # pragma: no cover - _test_check_violations_batched_per_kind, - _test_check_violations_batched_b1_scalar_params, -] - - -def run_all_tests() -> int: - passed = failed = 0 - for fn in _TESTS: - try: - fn() - passed += 1 - print(f" PASS {fn.__name__}") - except Exception as e: - failed += 1 - print(f" FAIL {fn.__name__}: {e}") - print(f"\n{passed} passed, {failed} failed") - return 1 if failed else 0 - - -if __name__ == "__main__": - print("Running BaB module tests\n") - sys.exit(run_all_tests())