Repeat ase

.github/workflows/act-pipeline-fuzz.yml

@@ -93,6 +93,29 @@ jobs:
           cd ${{ github.workspace }}
           coverage run -p -m act.pipeline --fuzz --category cifar100_2024 --max-instances 2 --timeout 30 --iterations 500
 
+      - name: Run fuzzing at float64 (non-quantized CIFAR-100)
+        run: |
+          cd ${{ github.workspace }}
+          coverage run -p -m act.pipeline --fuzz --category cifar100_2024 --dtype float64 --max-instances 2 --timeout 30 --iterations 200
+
+      - name: Cache traffic signs VNNLIB benchmark
+        id: trafficsigns-cache
+        uses: actions/cache@v4
+        with:
+          path: data/vnnlib/traffic_signs_recognition_2023
+          key: vnnlib-traffic-signs-2023-v1
+
+      - name: Download traffic signs benchmark (binarized nets)
+        if: steps.trafficsigns-cache.outputs.cache-hit != 'true'
+        run: |
+          cd ${{ github.workspace }}
+          coverage run -p -m act.pipeline --download traffic_signs_recognition_2023
+
+      - name: Run fuzzing at float64 (binarized traffic signs, sign-STE path)
+        run: |
+          cd ${{ github.workspace }}
+          coverage run -p -m act.pipeline --fuzz --category traffic_signs_recognition_2023 --dtype float64 --max-instances 2 --timeout 30 --iterations 200
+
       - name: Run fuzzing with --category flag (safeNLP text benchmark, real FC+ReLU)
         run: |
           cd ${{ github.workspace }}

act/back_end/bab/bab.py

@@ -559,21 +559,6 @@ def _slice_branching_state(
 
 
 
-def _unbatch_field(val: Any) -> Any:
-    """Strip lazy-M broadcast batch dim when a field is shared by one sample.
-
-    BaB dual dispatch rebuilds an ``OutputSpec`` from ASSERT parameters while
-    subproblem lanes live in the leading lazy-M dimension. If a parameter is a
-    tensor with a singleton leading batch axis, remove that axis so
-    ``OutputSpec.encode_linear`` can re-broadcast it to the current K lanes.
-    """
-    if isinstance(val, torch.Tensor) and val.dim() >= 2 and val.shape[0] == 1:
-        return val[0]
-    return val
-
-
-
-
 def _as_batched_vector(
     value: object,
     n_batch: int,
@@ -719,7 +704,10 @@ def check_violations_batched(net: object, x_batch: torch.Tensor, assert_layer: L
         mask = torch.ones_like(y_batch, dtype=torch.bool)
         _ = mask.scatter_(1, y_true.unsqueeze(1), False)
         other_scores = y_batch.masked_fill(~mask, -float("inf"))
-        return (other_scores.max(dim=1).values - y_true_scores) >= margin
+        # ``-margin``, not ``+margin``: ``encode_linear`` emits rows ``e_j - e_t``
+        # with ``thresholds = -margin``, so a lane is certified iff
+        # ``max_j(z_j - z_t) < -margin``. The negative sign is deliberate.
+        return (other_scores.max(dim=1).values - y_true_scores) >= -margin
 
     if kind == OutKind.LINEAR_LE:
         c_raw = params["c"]
@@ -1044,12 +1032,16 @@ def _dispatch_dual_solve(
     if not isinstance(out_kind_raw, str):
         raise TypeError(f"ASSERT kind must be str, got {type(out_kind_raw).__name__}")
 
-    out_spec_fields: dict[str, torch.Tensor] = {}
-    for key in OutputSpec.SLICEABLE_PARAM_KEYS:
-        if key in assert_layer.params and assert_layer.params[key] is not None:
-            value = assert_layer.params[key]
-            tensor_value = value if isinstance(value, torch.Tensor) else torch.as_tensor(value)
-            out_spec_fields[key] = _unbatch_field(tensor_value)
+    out_spec_fields = OutputSpec(kind=out_kind_raw)._gather_rows(
+        rows=None,
+        batch_size=1,
+        device=batched_bounds.lb.device,
+        dtype=batched_bounds.lb.dtype,
+        shared_ndim={},
+        source=assert_layer.params,
+        source_batch_size=1,
+        drop_singleton_batch=True,
+    )
 
     out_spec = OutputSpec(
         kind=out_kind_raw,
@@ -2358,19 +2350,18 @@ def _test_check_violations_batched_per_kind():  # pragma: no cover
     expected_top1 = y.argmax(dim=1) != y_true_top1
     assert torch.equal(check_violations_batched(net, y, top1), expected_top1)
 
-    margin = _make_assert_layer(
-        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),
-        },
-        n_out,
+    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
     )
-    y_true = torch.tensor([0, 0, 1, 1, 2, 2, 3, 3])
-    true_scores = y.gather(1, y_true.unsqueeze(1)).squeeze(1)
-    mask = torch.ones_like(y, dtype=torch.bool)
-    _ = mask.scatter_(1, y_true.unsqueeze(1), False)
-    expected_margin = (y.masked_fill(~mask, -float("inf")).max(dim=1).values - true_scores) >= 1.5
+    # 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(

act/config/pipeline.yaml

@@ -67,6 +67,20 @@ fuzzing:
   # time-to-first-counterexample).
   stop_on_first_violation: false
 
+  # Tensor dtype for this tier. Deliberately float32 while backend.yaml is
+  # float64 -- this is not an oversight. The pipeline tier fuzzes ONNX models
+  # whose weights are natively float32, so float32 IS the network on disk and
+  # is what every measurement to date was taken at; the back_end verifier wants
+  # float64 for numerical stability in LP and branch-and-bound.
+  dtype: "float32"
+
+  # Independent PGD random starts per mutation; the best lane-wise result wins
+  # and restarts stop early once every lane violates. 1 = single start.
+  pgd_restarts: 1
+  # Used instead of pgd_restarts once sign estimators are installed, which only
+  # happens on a binarized network.
+  pgd_restarts_binarized: 40
+
 # ─────────────────────────────────────────────────────────────────────────────
 # Verification  (Branch-and-Bound)
 # ─────────────────────────────────────────────────────────────────────────────

act/config/pipeline_cli.py

@@ -31,7 +31,7 @@
 from act.front_end.torchvision_loader.create_specs import TorchVisionSpecCreator
 from act.front_end.torchvision_loader import data_model_loader as tv_loader
 from act.front_end.torchvision_loader import data_model_mapping as tv_mapping
-from act.front_end.model_synthesis import synthesize_models_from_specs
+from act.front_end.model_synthesis import synthesize_models_and_seeds_from_specs
 from act.pipeline.fuzzing.actfuzzer import ACTFuzzer, FuzzingConfig
 from act.pipeline.verification.per_neuron_bounds import PerNeuronCheckConfig
 from act.config.config import PipelineConfig
@@ -60,6 +60,9 @@
     ("trace_storage", "--trace-storage", "trace_storage", str),
     ("trace_output", "--trace-output", "trace_output", Path),
     ("stop_on_first_violation", "--stop-on-first-violation", "stop_on_first_violation", bool),
+    ("dtype", "--dtype", "dtype", str),
+    ("pgd_restarts", "--pgd-restarts", "pgd_restarts", int),
+    ("pgd_restarts_binarized", "--pgd-restarts-binarized", "pgd_restarts_binarized", int),
 ]
 
 
@@ -149,6 +152,18 @@ def _add_fuzz_config_args(parser: argparse.ArgumentParser) -> None:
         default=None,
         help="Stop after the first counterexample (default: from config.yaml/FuzzingConfig default)",
     )
+    group.add_argument(
+        "--pgd-restarts",
+        type=int,
+        default=None,
+        help="PGD random starts per mutation (default: from config.yaml)",
+    )
+    group.add_argument(
+        "--pgd-restarts-binarized",
+        type=int,
+        default=None,
+        help="PGD random starts per mutation on binarized networks (default: from config.yaml)",
+    )
 
 
 def _collect_fuzzing_overrides(args: Any) -> dict[str, Any]:
@@ -232,6 +247,8 @@ def _collect_pipeline_config_overrides(args: Any) -> dict[str, Any]:
 
 def _apply_pipeline_config_defaults(args: Any) -> PipelineConfig:
     config = PipelineConfig.from_yaml(**_collect_pipeline_config_overrides(args))
+    if getattr(args, "dtype", None) is None:
+        args.dtype = FuzzingConfig.from_yaml().dtype
     args.bab_solver_tier = config.bab.solver_tier
     args.bab_max_depth = config.bab.max_depth
     args.bab_max_nodes = config.bab.max_nodes
@@ -536,8 +553,6 @@ def cmd_fuzz(args):
     print(f"{rule()}\n")
 
     spec_results = []
-    initial_seeds = []
-
     try:
         if creator == "vnnlib":
             spec_creator = VNNLibSpecCreator()
@@ -648,7 +663,9 @@ def cmd_fuzz(args):
     VerifiableModel.set_strict_mode(args.strict_mode)
 
     try:
-        wrapped_models = synthesize_models_from_specs(cast(Any, spec_results))
+        wrapped_models, synthesized_seeds = synthesize_models_and_seeds_from_specs(
+            cast(Any, spec_results), cd_group="shape"
+        )
     except Exception as e:
         print(f"❌ Model synthesis failed: {e}")
         import traceback
@@ -667,9 +684,8 @@ def cmd_fuzz(args):
     print(f"STEP 3: Seed Extraction")
     print(f"{rule()}\n")
 
-    # Single model only; mixing seeds across spec_results breaks SeedCorpus(torch.cat).
-    _, _, _, labeled_tensors, _ = spec_results[0]
-    initial_seeds.extend(labeled_tensors)
+    model_id = list(wrapped_models.keys())[0]
+    initial_seeds = synthesized_seeds[model_id]
 
     if not initial_seeds:
         print("❌ No initial seeds extracted!")
@@ -682,7 +698,6 @@ def cmd_fuzz(args):
     print(f"STEP 4: Fuzzing")
     print(f"{rule()}\n")
 
-    model_id = list(wrapped_models.keys())[0]
     wrapped_model = wrapped_models[model_id]
 
     print(f"Fuzzing model: {model_id}\n")
@@ -940,15 +955,32 @@ def _sliced_net_view(net, sample_idx: int, batch_size: int):
     orig_spec_params = [deepcopy(spec_layer.params) for spec_layer in spec_layers]
     orig_input_outvars = list(input_layer.out_vars)
     try:
-        for key in OutputSpec.SLICEABLE_PARAM_KEYS:
-            val = orig_assert_params.get(key)
-            if (
-                val is not None
-                and hasattr(val, "dim")
-                and val.dim() >= 1
-                and val.shape[0] == batch_size
-            ):
-                assert_layer.params[key] = val[sample_idx : sample_idx + 1]
+        assert_kind = orig_assert_params.get("kind")
+        if not isinstance(assert_kind, str):
+            raise TypeError(
+                f"ASSERT kind must be str, got {type(assert_kind).__name__}"
+            )
+        reference = next(
+            (
+                value
+                for value in orig_assert_params.values()
+                if isinstance(value, torch.Tensor) and value.is_floating_point()
+            ),
+            None,
+        )
+        if reference is None:
+            raise RuntimeError("ASSERT params contain no floating tensor for slicing")
+        assert_layer.params.update(
+            OutputSpec(kind=assert_kind)._gather_rows(
+                rows=torch.tensor([sample_idx], device=reference.device),
+                batch_size=1,
+                device=reference.device,
+                dtype=reference.dtype,
+                shared_ndim={},
+                source=orig_assert_params,
+                source_batch_size=batch_size,
+            )
+        )
 
         for spec_layer, sp_orig in zip(spec_layers, orig_spec_params):
             for sp_key, sp_val in sp_orig.items():
@@ -1722,7 +1754,7 @@ def main():
     )
 
     # Add standard device/dtype arguments (shared across all ACT CLIs)
-    add_device_args(parser)
+    add_device_args(parser, default_dtype=None)
 
     _add_fuzz_config_args(parser)