fix and opt backend and revise netfactory. by guanqin-123 · Pull Request #96 · SVF-tools/ACT

guanqin-123 · 2026-07-09T21:11:59Z

No description provided.

codecov · 2026-07-09T21:18:21Z

Codecov Report

❌ Patch coverage is 75.16340% with 152 lines in your changes missing coverage. Please review.
✅ Project coverage is 73.67%. Comparing base (8c41b8b) to head (b34a58b).

Files with missing lines	Patch %	Lines
act/back_end/cons_exportor.py	26.66%	44 Missing ⚠️
act/back_end/net_factory.py	48.27%	15 Missing ⚠️
act/back_end/solver/solver_gurobi.py	21.05%	15 Missing ⚠️
act/config/config.py	92.10%	15 Missing ⚠️
act/front_end/model_synthesis.py	37.50%	15 Missing ⚠️
act/pipeline/verification/torch2act.py	77.04%	14 Missing ⚠️
.../front_end/torchvision_loader/data_model_loader.py	47.36%	10 Missing ⚠️
act/util/stats.py	14.28%	6 Missing ⚠️
act/back_end/bab/bab.py	40.00%	3 Missing ⚠️
act/front_end/bert_loader/create_specs.py	50.00%	3 Missing ⚠️
... and 7 more

Additional details and impacted files

@@            Coverage Diff             @@
##             main      #96      +/-   ##
==========================================
+ Coverage   73.19%   73.67%   +0.48%     
==========================================
  Files          92       91       -1     
  Lines       20268    20372     +104     
==========================================
+ Hits        14835    15010     +175     
+ Misses       5433     5362      -71

Flag	Coverage Δ
bab	`50.13% <64.21%> (+4.83%)`	⬆️
backend-float32	`49.32% <59.47%> (+0.49%)`	⬆️
backend-float64	`49.36% <59.47%> (+0.49%)`	⬆️
frontend	`32.99% <60.62%> (+0.58%)`	⬆️
pipeline-fuzz	`20.62% <39.37%> (+0.41%)`	⬆️
pipeline-verify	`39.55% <50.49%> (+0.56%)`	⬆️

Flags with carried forward coverage won't be shown. Click here to find out more.

Files with missing lines	Coverage Δ
act/back_end/bab/__init__.py	`100.00% <100.00%> (ø)`
act/back_end/core.py	`74.19% <100.00%> (+1.59%)`	⬆️
act/back_end/dual_tf/tf_cnn.py	`86.17% <ø> (ø)`
act/back_end/hybridz_tf/hybridz_tf.py	`93.77% <100.00%> (+0.35%)`	⬆️
act/back_end/hybridz_tf/tf_mlp.py	`85.81% <100.00%> (+0.01%)`	⬆️
act/back_end/interval_tf/interval_tf.py	`100.00% <100.00%> (ø)`
act/back_end/interval_tf/tf_mlp.py	`89.23% <100.00%> (+0.17%)`	⬆️
act/back_end/layer_schema.py	`100.00% <100.00%> (+2.02%)`	⬆️
act/back_end/solver/solver_dual.py	`70.67% <100.00%> (ø)`
act/back_end/solver/solver_torchlp.py	`75.65% <100.00%> (-0.78%)`	⬇️
... and 26 more

... and 1 file with indirect coverage changes

Continue to review full report in Codecov by Harness.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 8c41b8b...b34a58b. Read the comment docs.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

yuleisui · 2026-07-09T23:21:21Z

+# Single-source default LRELU/LeakyReLU negative slope, shared by dual and
+# hybridz transfer functions when a layer omits the alpha/negative_slope param.
+LRELU_ALPHA_DEFAULT = 0.01


All configuration parameters should be put into a single yaml in the back and also in CLI.

yuleisui · 2026-07-09T23:27:18Z

When simplifying the three components, could you make a single config.yaml under each of these three components to include all configurations (from CLIs)?

Make sure:
(1) every parameter appears in both yaml and CLI
(2) all ad hoc parameters and macros hardcoded in any Python file, should be included in the config.yaml.

…_end Consolidate a single config.yaml per component and make every Bucket-A tunable appear in BOTH the yaml and the CLI, behavior-preserving (new defaults equal the current hardcoded/argparse values). - back_end: surface all BaBConfig/BackendConfig knobs into config.yaml; add SolverConfig (TorchLP hyperparams) + TFConfig (hz_max_input_dim) wired through auto-generated --solver-*/--tf-* flags, from_yaml routing, TorchLPSolver and HybridzTF. - pipeline: new act/pipeline/config.py + single act/pipeline/config.yaml (fuzzing + verification.bab + validation at the pipeline defaults); repoint FuzzingConfig, delete fuzzing/config.yaml. - front_end: new act/front_end/config.py + single act/front_end/config.yaml (full torchvision/vnnlib/default spec presets + text_verification); repoint spec loader + path_config, delete configs/specs/*; add spec CLI flags and wire the previously-dead text-verify args. Excludes vnncomp settings, numerical/soundness constants, and math/data/enums. Verified: config snapshots byte-identical per tier; soundness harness 141/141.

# Conflicts: # act/back_end/hybridz_tf/hybridz_tf.py

guanqin-123 · 2026-07-10T03:19:57Z

When simplifying the three components, could you make a single config.yaml under each of these three components to include all configurations (from CLIs)?

Make sure: (1) every parameter appears in both yaml and CLI (2) all ad hoc parameters and macros hardcoded in any Python file, should be included in the config.yaml.

done

yuleisui · 2026-07-10T03:25:46Z

When simplifying the three components, could you make a single config.yaml under each of these three components to include all configurations (from CLIs)?
Make sure: (1) every parameter appears in both yaml and CLI (2) all ad hoc parameters and macros hardcoded in any Python file, should be included in the config.yaml.

done

Better to create a separate folder act/config to host config.yaml and config.py, having three separate yaml files but only one config.py (remove all current config.yaml and config.py)

frontend_config.yaml
backend_config.yaml
pipeline_config.yaml
config.py

Merge the three per-tier config modules into one act/config/config.py and move the yaml files to act/config/{backend,pipeline,frontend}_config.yaml. Update every importer to act.config.config, repoint runtime yaml paths (FuzzingConfig, --backend-config help, CI act-bab.yml hashFiles), and fix the gen_config path and the three _DEFAULT_YAML constants for the new location. FuzzingConfig is imported lazily inside PipelineConfig.from_yaml to avoid an import cycle. Pure relocation, behavior-preserving: all config snapshots byte-identical, imports clean (no cycle), soundness 141/141.

guanqin-123 · 2026-07-10T06:11:19Z

When simplifying the three components, could you make a single config.yaml under each of these three components to include all configurations (from CLIs)?
Make sure: (1) every parameter appears in both yaml and CLI (2) all ad hoc parameters and macros hardcoded in any Python file, should be included in the config.yaml.

done

Better to create a separate folder act/config to host config.yaml and config.py, having three separate yaml files but only one config.py (remove all current config.yaml and config.py)

frontend_config.yaml backend_config.yaml pipeline_config.yaml config.py

I revised them to act/config and unify in one config.py

yuleisui · 2026-07-10T10:28:01Z

Could you do the below ones before I merge:

(1) Remove duplicate options across these three yaml files, identify similar ones or sub-relations to simplify them
(2) Make sure any changes of a configure yaml are effective (make sure they are not only placeholders)
(4) Move CLI files of the three components also under act/config (similar naming as yaml files). Also update README regarding CLI too.
(3) CLI will override yaml configure, and CLI and yaml are one to one mapping.

… docs - Move act/{back_end,pipeline,front_end}/cli.py -> act/config/{backend,pipeline, frontend}_cli.py (matching the yaml names); repoint the three __main__.py. Entry points 'python -m act.X' unchanged; sub-loader CLIs untouched. - Remove dead HybridZConfig.engine (surfaced in yaml but never read anywhere). - Dedup pipeline_config.yaml verification.bab to its 3 real overrides (solver_tier/max_depth/max_nodes); the other keys just restated BaBConfig defaults. Behavior-preserving (absent keys fall to the same defaults). - Update READMEs (act + tiers + data/vnnlib) for config centralization + CLI move. Verified: pipeline bab byte-identical, backend identical minus engine, all python -m act.{back_end,pipeline,front_end} + sub-loaders EXIT 0, soundness 141/141.

yuleisui · 2026-07-11T00:59:02Z

Yaml files are supposed to be edited by users, when reading the current versions, it looks very disorganised and better to put options which are related next to each other and group the ones into blocks where necessary and add comments (including explanation and possible parameters) for each block.

The three tier CLIs were git mv'd to act/config/ but .codecov.yml still ignored them at their old act/{back_end,front_end,pipeline}/cli.py paths, so ~773 lines of intentionally-excluded argparse plumbing (48-70% covered) started counting toward project coverage (~1% drop). Restore the intended exclusion at the new paths.

User-facing config files are edited by hand, so group related options into labelled blocks and document each key with its purpose and valid values. - backend_config.yaml: order runtime -> cascade -> solver_config -> tf -> hybridz -> bab -> generation; split the 57-key bab block into labelled sub-blocks (search limits / branching+bounding / dual alpha-eta / refinement / auto-batch / llm-probe / bert-text / diagnostics). - pipeline_config.yaml: comment every fuzzing key (budget / coverage / mutation / seeding / output / tracing / early-stop) with valid enum values; annotate validation. - frontend_config.yaml: add a specs-schema header (valid input/output kinds, combination strategies), per-preset labels, and text_verification comments. Comments/reordering only: no key, value, or nesting changed. Verified by a resolved-config snapshot (all 3 configs load byte-identical before/after), entry points EXIT 0, and soundness harness EXIT 0 (all SOUND BOUNDS passed).

guanqin-123 · 2026-07-11T01:48:58Z

Yaml files are supposed to be edited by users, when reading the current versions, it looks very disorganised and better to put options which are related next to each other and group the ones into blocks where necessary and add comments (including explanation and possible parameters) for each block.

done

yuleisui · 2026-07-11T03:02:40Z

+  # lives in gen_config_path — a separate file with its own schema.
+  generation:
+    # Path to the architecture sampling config (families, specs, etc.).
+    gen_config_path: "act/back_end/examples/config_gen_act_net.yaml"


Could we merge config_gen_act_net.yaml into this backend_config.yaml?

yuleisui · 2026-07-11T03:06:30Z

Please also do below:

No other files, and only config.py reads the YAML config files
Add a GitHub action act.config.yml in the CI to check the consistency and 1-to-1 mapping from each CLI option to the YAML file. This will ensure that any future options are added in either of these two ways are guaranteed to be the same and will not be missed by either of them.

feat(hybridz): complete frontend solver integration

Integrate SVF-tools/ACT main (bd95412..8c41b8b): HybridZ sparse affine + sparse ReLU propagation, exact HiGHS (scipy) verdict solver, verifier timelimit plumbing. Git rename detection ported upstream's HybridZ verify gates from the old act/back_end/cli.py onto the relocated act/config/backend_cli.py (_verify_one_net: is_hybridz gating of the LP-rescue + BaB tiers, hz_timeout). Verified: clean auto-merge (no conflicts), all merged modules import, dual soundness 141/0.

guanqin-123 · 2026-07-12T04:22:12Z

Please also do below:

No other files, and only config.py reads the YAML config files

Add a GitHub action act.config.yml in the CI to check the consistency and 1-to-1 mapping from each CLI option to the YAML file. This will ensure that any future options are added in either of these two ways are guaranteed to be the same and will not be missed by either of them.

I merged the hz's part and added the config checking yml.

yuleisui · 2026-07-12T09:01:50Z

        with:
          path: act/back_end/examples/nets
-          key: act-nets-${{ hashFiles('act/back_end/examples/config_gen_act_net.yaml', 'act/back_end/net_factory.py', 'act/back_end/config.yaml') }}
+          key: act-nets-${{ hashFiles('act/back_end/examples/config_gen_act_net.yaml', 'act/back_end/net_factory.py', 'act/config/backend_config.yaml') }}


Could we merge config_gen_act_net.yaml into this backend_config.yaml?

Could we update this line if config_gen_act_net.yaml has been merged into backend_config.yaml?

yuleisui · 2026-07-12T09:05:34Z

Confusing that we have a vnncomp folder but this file is a separate one in the verification folder? Why do we need this file but not merging it into vnncomp/act_run_instance.py? What is the difference between this file and vnncomp/act_run_instance.py?

yes, runner is removed.

yuleisui · 2026-07-12T09:09:00Z

+# BackendConfig's top-level text-verification scalars mirror the bab.* copies and
+# default; they are CLI/dataclass-only and intentionally absent from the YAML.
+_BACKEND_CLI_ONLY_FIELDS = {
+    "method", "p", "perturbed_words", "eps", "max_eps",
+    "num_verify_iters", "k", "alpha_opt_steps",
+}
+
+# Backend YAML sub-section -> the prefix its keys carry in the CLI override space
+# (e.g. yaml ``backend.solver_config.lr`` corresponds to CLI/override ``solver_lr``).
+_BACKEND_SECTION_PREFIX = {
+    "bab": "bab_",
+    "generation": "gen_",
+    "hybridz": "hybridz_",
+    "solver_config": "solver_",
+    "tf": "tf_",
+}


Could we remove all these hand-coded fields for checking, in case any future options can be added without this blocker?

yuleisui · 2026-07-12T09:09:31Z

+# default; they are CLI/dataclass-only and intentionally absent from the YAML.
+_BACKEND_CLI_ONLY_FIELDS = {
+    "method", "p", "perturbed_words", "eps", "max_eps",
+    "num_verify_iters", "k", "alpha_opt_steps",
+}
+


Could we remove all these hand-coded fields for checking, in case any future options can be added without this blocker?

now, removed the hard coded fields.

…s) + inline vnncomp runner - act.config.check_parity + CI derive CLI<->YAML<->dataclass parity from the config dataclasses; no hand-coded field/prefix lists. config.py is the sole reader of the backend/pipeline/frontend config YAMLs. - inline the VNN-COMP runner into vnncomp/act_run_instance.py; remove act/pipeline/verification/vnncomp_runner.py.

…config_gen_act_net.yaml Consolidate the network-generation DSL (families, sampling rules, input/output specs, validate.batch_sizes) into backend_config.yaml under backend.generation.net_factory, exposed via GenerationConfig.net_factory. - config.py: add GenerationConfig.net_factory dict field; drop gen_config_path - backend_config.yaml: embed the DSL under generation.net_factory - net_factory.py: NetFactory takes required config dict; remove gen_config_path fallback + _load_config (no back-compat) and now-unused yaml import - backend_cli.py: pass config=gen.net_factory; exclude net_factory from generated CLI args; drop gen_config_path alias - pipeline_cli.py: _resolve_batch_sizes reads backend.generation.net_factory; fix --batch-sizes help text - path_config.py: remove get_examples_gen_config_path (no callers) - docs: repoint README references - delete act/back_end/examples/config_gen_act_net.yaml Behavior-preserving: embedded DSL parses deep-equal to the old file and _load_config was a plain yaml load. Verified: CLI<->YAML parity OK, serialization round-trip 74/74, CLI entry points import, lsp clean.

…6 sites) Replace inline separator idioms (char*width, e.g. "="*80) with rule() from act.util.format_utils, consolidating 266 copies of the banner idiom into one helper. Behavior-preserving: rule(N, C) == C*N by construction. - add `from act.util.format_utils import rule` to each file (data_model_loader extends its existing format_utils import; model_synthesis adds a local import inside its run-as-script guard) - widths/chars preserved exactly: rule(), rule(100), rule(70, "-"), ... Verified: 0 remaining idioms, lsp clean (no new errors), all 3 CLI entry points --help exit 0, all 20 modules import.

Consolidate the 38 module-backed LayerKind<->nn.Module pairs (previously duplicated as the _ACT_TO_TORCH forward dict in act2torch.py and the isinstance reverse dispatch in torch2act.py) into one source: act/back_end/layer_torch_map.py (ACT_TO_TORCH + custom activation modules). - act2torch.py: import ACT_TO_TORCH instead of a local dict literal - torch2act.py: derive _TORCH_TO_ACT_EXACT reverse lookup from ACT_TO_TORCH; keep isinstance dispatch for subclass matching + param extraction + BN decomposition (semantics unchanged) Adding a layer now edits one place. Behavior-preserving; verified --verify act2torch (float64) and --verify torch2act (float32/float64) all exit 0.

…y_context verify_once and verify_lp_batched duplicated the INPUT_SPEC seed setup (gather_input_spec_layers -> seed_from_input_specs -> batch-dim check -> B). Extract the minimal shared block into _setup_verify_context(net) -> (spec_layers, seed_bounds, B). Deliberately minimal: entry_id/input_ids/output_ids/assert_layer stay in verify_once (verify_lp_batched never computed them, and find_entry_layer_id/ get_output_ids can raise, so hoisting them would add new raising behavior). verify_lp_batched keeps its extra ub.dim() check. Behavior-preserving; verified identical before/after: --validate-soundness torchlp 222/0, dual 141/0, --test-serialization 74/74, all exit 0.

The two _LAYER_REGISTRY keysets are intentionally asymmetric by exactly one kind (MEAN is interval-only; HybridZ raises NotImplementedError for it). A literal merge into one canonical list would silently change dispatch behavior, so per Oracle review WS4.2 ships as a drift-detection guard rather than a merge. Pins interval-only == {MEAN} and hybridz-only == {} so future drift fails loudly instead of silently changing which layers each TF supports. Runnable via: python -m act.back_end.test_tf_registry_parity

…3.2a) Replace raw "SAT"/"UNSAT"/"UNKNOWN" string literals in GurobiSolver.solve_batch with SolveStatus.SAT/UNSAT/UNKNOWN (solver_base), matching solver_torchlp which already uses the enum. Value-identical (SolveStatus.SAT == "SAT") so behavior-preserving. Per Oracle review only the gurobi status literals are unified; solver_hz's VerifyStatus is intentionally left (it is the verify-layer abstraction, not solve-layer drift). Verified: solver_base self-test 5/5, no raw literals remain in solve_batch, imports + SolveStatus values OK, lsp adds no new errors.

…leton (WS4.1) IntervalTF and HybridzTF duplicated the apply() dispatch skeleton (context set + registry lookup + NotImplementedError on unsupported kind). Hoist the identical pieces into a RegistryTF base (transfer_functions.py) exposing name, supports_layer, _check_supported, _set_context. Both TFs now inherit it. - Registries stay separate (distinct handlers; keysets intentionally differ by MEAN, guarded by test_tf_registry_parity). - HybridzTF.apply keeps 100% of its cache/HZ orchestration in its own override; no cache logic moved to the base. - dual_tf left independent (different architecture). Behavior-preserving; verified: per-layer Fact.bounds bit-identical (torch.equal atol=0) for interval+hybridz on MLP/CNN/transformer; --validate-soundness torchlp 222/0 + dual 141/0 unchanged; registry parity + serialization 74/74; lsp clean.

yuleisui · 2026-07-13T08:44:03Z

+  # ─────────────────────────────────────────────────────────────────────────
+  # Transfer-function limits  (tf)
+  # ─────────────────────────────────────────────────────────────────────────
+  tf:
+    # HybridZ generator/input dimension fallback limit.
+    hz_max_input_dim: 1024
+
+  # ─────────────────────────────────────────────────────────────────────────
+  # HybridZ solver  (hybridz)
+  # ─────────────────────────────────────────────────────────────────────────
+  hybridz:
+    # Per-call wall-clock budget in seconds; null = no HybridZ-specific limit.
+    timeout: null
+


Could you fix these blocks?

yuleisui · 2026-07-13T08:45:11Z

+  # ═════════════════════════════════════════════════════════════════════════
+  # Branch-and-Bound refinement  (bab)
+  # ═════════════════════════════════════════════════════════════════════════


Could you fix BaB block too as it mixed with bab (only for dual) and a number of llm options too.

yuleisui · 2026-07-13T08:46:00Z

@@ -0,0 +1,779 @@
+# ═══════════════════════════════════════════════════════════════════════════


The current backend.yaml is very large. Any way to simplify it or split into two under the config folder?

How to split it?

previous act/back_end/examples/config_gen_act_net.yaml has 400 lines include multiple networks.

create a new file naming "gen_act_net.yaml" for all act net generation configurations.

The lone tf.hz_max_input_dim (TFConfig) was a HybridZ TF limit stranded in a generic tf: block beside a single-field hybridz: block. Merge into one HybridZConfig (timeout + max_input_dim); delete TFConfig and the tf: block. - config.py: HybridZConfig gains max_input_dim; TFConfig removed; from_yaml/ to_yaml/BackendConfig drop tf routing (the hybridz_ override prefix now covers it) - backend_cli.py: drop the tf- arg group + prefix; flag is now --hz-max-input-dim (was the double-prefixed --tf-hz-max-input-dim) - hybridz_tf.py: HybridzTF(config: HybridZConfig) reads cfg.max_input_dim - backend_config.yaml: max_input_dim moves under hybridz: Behavior-preserving (value unchanged 1024). Verified: parity OK, HybridzTF _HZ_MAX_INPUT_DIM==1024, lsp clean, 0 remaining TFConfig/hz_max_input_dim refs.

…only The backend.bab YAML block mixed general BaB, dual-tier, LLM-probe and BERT-text settings. Demote the default-only / expert-only fields to CLI-only: they keep their dataclass default + --bab-<flag>, but leave the YAML. bab YAML: 48 -> 28 keys; what remains is the set actually tuned in CI / pipeline_config / vnncomp. Enabling mechanism (in_yaml=False was previously honored only for top-level BackendConfig fields): - config.py: mark 29 BaBConfig fields metadata={"in_yaml": False}; from_yaml now filters bab_raw to in_yaml=True keys (CLI overrides still apply). - check_parity.py: honor in_yaml=False on nested BaBConfig fields (bab CLI options absent from YAML must be in_yaml=False), mirroring the top-level rule. - backend_config.yaml: drop the demoted keys; keep the tuned knobs + the BERT text-method group, grouped by concern. Behavior-preserving (demoted YAML values equalled dataclass defaults). Verified: CONFIG PARITY OK; --bab-lr-beta override still works; torchlp + dual --validate-soundness exit 0 all SOUND; lsp clean.

Drop the optional IntervalTF/HybridzTF registry parity guard (added in c27cbf9); not needed per review. Standalone leaf test — no importers.

backend_config.yaml -> backend.yaml, frontend_config.yaml -> frontend.yaml, pipeline_config.yaml -> pipeline.yaml. Updated all references: config.py _*_YAML constants + docstrings/errors, check_parity, backend/pipeline CLIs, net_factory config_path, CI act-bab.yml hashFiles, and docs. Verified: 0 remaining old-name refs, CONFIG PARITY OK, all 3 CLIs load.

yuleisui · 2026-07-14T01:40:37Z

+#!/usr/bin/env python3
+# ===- act/back_end/layer_torch_map.py - ACT/Torch layer mapping ---------====#
+


What is this file for?

it is repeated for layerschema, now deleted.

Extract the entire generation config (control knobs + net_factory architecture DSL) out of backend.yaml into act/config/networkGen.yaml. backend.yaml now holds only verification/runtime/solver/hybridz/bab settings (601 -> 129 lines). - networkGen.yaml: generation control knobs (output_dir, num_instances, base_seed, tf_targets, coverage_*, write_manifest, ...) + net_factory: DSL (families, sampling rules, input/output specs) - config.py: from_yaml loads the generation section from networkGen.yaml; net_factory reverts to a normal field (drops the in_yaml=False special-casing) - check_parity: generation gen_* keys sourced from networkGen.yaml - backend.yaml: generation: section removed - --gen-* CLI overrides still work; docs/help repointed to networkGen.yaml Behavior-preserving. Verified: generation values load (num=15, seed=42), net_factory DSL deep-equal, --gen-num override, CONFIG PARITY OK, batch_sizes [None,1,4], --generate exit 0 (74 nets), to_yaml OK, lsp clean.

…le CI cache key - Rename act/config/networkGen.yaml -> act/config/gen_act_net.yaml; update all references (config.py _NETGEN_YAML, net_factory config_path, pipeline_cli help, act/README.md + examples/README.md docs). - act-bab.yml: fix the generated-nets cache key. It still hashed act/back_end/examples/config_gen_act_net.yaml (deleted back in P0), so the cache never invalidated when the generation config changed. Point it at the real source act/config/gen_act_net.yaml. Verified: 0 stale config-path refs (incl .github), CONFIG PARITY OK, generation config loads from gen_act_net.yaml, batch_sizes [None,1,4], lsp clean.

Move ACT_TO_TORCH (LayerKind -> nn.Module) and the 5 custom activation modules (_Erf/_Sqrt/_Quantize/_Sin/_Cos) from layer_torch_map.py into layer_schema.py (after REGISTRY), so all LayerKind metadata -- param schema + torch restoration map -- lives in one file. Delete layer_torch_map.py. - act2torch.py / torch2act.py now import ACT_TO_TORCH from layer_schema - fix stale comments in layer_schema that pointed at act2torch._ACT_TO_TORCH (WS6.2 had already relocated it) No dedup (schema and torch-map are orthogonal LayerKind metadata) — this is co-location. Behavior-preserving; verified --verify act2torch (float64) and torch2act (float32) exit 0, ACT_TO_TORCH 38 entries, no import cycle, lsp clean.

…ming) SolverConfig was TorchLP-only despite the generic name. Rename to TorchLPConfig; yaml solver_config: -> torchlp:; CLI --solver-* -> --torchlp-*. First step of organizing solver params under each solver's own block. Behavior-preserving. Verified: 0 SolverConfig/solver_config refs, CONFIG PARITY OK, torchlp values + --torchlp-max-iter override work, torchlp --validate-soundness 222/0 exit 0, lsp clean.

Gurobi had no config -- all knobs hardcoded/defaulted. Add a per-solver gurobi: block (time_limit, mip_gap, threads, output_flag) and wire GurobiSolver(config) to apply them (OutputFlag/MIPGap/Threads; optional TimeLimit override). Also add a comment under solver: clarifying the selector-vs-per-solver-tuning-block layout. Config plumbing verified (the gurobi solve path needs a license, untestable locally): CONFIG PARITY OK, gurobi config loads + --gurobi-threads override, --gurobi-* flags present, solver imports, lsp clean.

HZSolver had hardcoded time_limit=30.0 and tolerance=1e-7 with no config home, and HybridZConfig.timeout was not reaching the solver. Add HybridZConfig.tolerance and wire timeout -> HZSolver.time_limit + tolerance -> HZSolver.tolerance at the construction site, so the hybridz: block actually configures the solver. Behavior-preserving (defaults unchanged: 30.0 / 1e-7 fallback). Verified: CONFIG PARITY OK, config->solver wiring proven (timeout=2.5 / tolerance=1e-6 reach HZSolver), --hz-tolerance override works, hybridz --verify runs, lsp clean.

…dual is param-free) Traced the dual solver: single-shot `solver: dual` (verify_once -> DualSolver.evaluate_spec -> compute_certified_bound(optimize=False)) is a parameter-free single fixed-slope backward pass. The 6 dual knobs (dual_n_iters, lr_alpha, lr_beta, lr_decay, per_class_alpha, incremental_start_enabled) are consumed ONLY by the BaB-optimized dual (bab.py, optimize=True; solver_tier dual_alpha/dual_alpha_eta). Conclusion: no DualConfig/dual: block is warranted -- those knobs are correctly placed in bab:. Add a comment so config users are not misled into tuning them under `solver: dual`. (Completes the per-solver config reorg: torchlp:/gurobi:/ hybridz: hold real solver params; dual's only tunables are BaB-loop behavior.)

Move the dual-solver optimization knobs out of bab: into a top-level dual: block (sibling of torchlp:/gurobi:/hybridz:) so each solver's params live in its own block. Moved: n_iters (was dual_n_iters), lr_alpha, lr_beta, lr_decay, per_class_alpha, incremental_start_enabled. bab: keeps enabled, solver_tier (the tier selector), and search/refinement params. - config.py: new DualConfig; BackendConfig.dual; from_yaml/to_yaml; build_vnncomp_ bab_config now returns (BaBConfig, DualConfig) - bab.py: verify_bab_batched(dual_config=...); dual paths read dual_config.* - backend_cli/pipeline_cli/vnncomp: thread dual_config through - backend.yaml/pipeline.yaml: add dual: block; trim bab: dual-tier section - check_parity: dual sub-config parity (lr_beta/lr_decay in_yaml=False) Behavior-preserving. Verified: CONFIG PARITY OK, dual.n_iters load + --dual-n-iters override, --validate-soundness torchlp 222/0 + dual 141/0 UNCHANGED before/after, build_vnncomp_bab_config OK, lsp clean on bab.py/config.py.

fix and opt backend

40128e5

yuleisui reviewed Jul 9, 2026

View reviewed changes

guanqin-123 added 2 commits July 10, 2026 12:12

Merge remote-tracking branch 'upstream/main' into feat/vit-bert-pipeline

985ffc3

# Conflicts: # act/back_end/hybridz_tf/hybridz_tf.py

guanqin-123 force-pushed the feat/vit-bert-pipeline branch from 7724e95 to 985ffc3 Compare July 10, 2026 02:16

guanqin-123 added 2 commits July 11, 2026 11:24

yuleisui reviewed Jul 11, 2026

View reviewed changes

yuleisui mentioned this pull request Jul 11, 2026

feat(hybridz): complete frontend solver integration #99

Closed

feat(hybridz): complete frontend solver integration

e472c58

Kaijie-liu mentioned this pull request Jul 11, 2026

feat(hybridz): complete frontend solver integration guanqin-123/ACT#4

Merged

guanqin-123 and others added 2 commits July 12, 2026 12:42

Merge pull request #4 from Kaijie-liu/hybridz-pr7-for-pr96-20260711

3d62f15

feat(hybridz): complete frontend solver integration

guanqin-123 force-pushed the feat/vit-bert-pipeline branch 2 times, most recently from 1ef7e40 to 2882015 Compare July 12, 2026 04:03

yuleisui reviewed Jul 12, 2026

View reviewed changes

guanqin-123 force-pushed the feat/vit-bert-pipeline branch 2 times, most recently from 24010da to 7704fe2 Compare July 13, 2026 00:03

guanqin-123 force-pushed the feat/vit-bert-pipeline branch from 7704fe2 to 7ef95ee Compare July 13, 2026 01:29

guanqin-123 added 7 commits July 13, 2026 16:22

yuleisui reviewed Jul 13, 2026

View reviewed changes

guanqin-123 added 4 commits July 14, 2026 09:36

chore(tf): remove test_tf_registry_parity drift-guard

6cd8d3e

Drop the optional IntervalTF/HybridzTF registry parity guard (added in c27cbf9); not needed per review. Standalone leaf test — no importers.

yuleisui reviewed Jul 14, 2026

View reviewed changes

guanqin-123 added 8 commits July 14, 2026 11:49

guanqin-123 force-pushed the feat/vit-bert-pipeline branch from 3193018 to b34a58b Compare July 14, 2026 06:32

yuleisui merged commit 09c3c6c into SVF-tools:main Jul 14, 2026
9 checks passed

		@@ -0,0 +1,779 @@
		# ═══════════════════════════════════════════════════════════════════════════

		#!/usr/bin/env python3
		# ===- act/back_end/layer_torch_map.py - ACT/Torch layer mapping ---------====#

Conversation

guanqin-123 commented Jul 9, 2026

Uh oh!

codecov Bot commented Jul 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

yuleisui commented Jul 9, 2026

Uh oh!

guanqin-123 commented Jul 10, 2026

Uh oh!

yuleisui commented Jul 10, 2026

Uh oh!

guanqin-123 commented Jul 10, 2026

Uh oh!

yuleisui commented Jul 10, 2026

Uh oh!

yuleisui commented Jul 11, 2026

Uh oh!

guanqin-123 commented Jul 11, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

yuleisui commented Jul 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

guanqin-123 commented Jul 12, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

codecov Bot commented Jul 9, 2026 •

edited

Loading

yuleisui commented Jul 11, 2026 •

edited

Loading