Repository navigation
BranchCore work - #115
BranchCore work#115guanqin-123 wants to merge 15 commits into
Conversation
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## main #115 +/- ##
==========================================
+ Coverage 75.44% 77.59% +2.14%
==========================================
Files 91 94 +3
Lines 22575 22985 +410
==========================================
+ Hits 17032 17835 +803
+ Misses 5543 5150 -393
Flags with carried forward coverage won't be shown. Click here to find out more.
... and 5 files with indirect coverage changes Continue to review full report in Codecov by Harness.
🚀 New features to boost your workflow:
|
|
Please fix the coverage ci |
d9327ac to
0b42029
Compare
Finished. after this, the upcoming pr to support SST, and YELP (NLP verification instance that contains a transformer architecture) |
| --network "$ACT_NETS_DIR/mlp_plain_3x8_64x64_3962224133.json" \ | ||
| --solver dual --bab --bab-solver-tier dual_alpha_eta \ | ||
| --bab-branching babsr --bab-bounding depth_bound_blend \ | ||
| --bab-root-bounds-reuse none --bab-intermediate-refine none \ | ||
| --bab-per-subproblem-refine none --bab-climb-enabled \ | ||
| --bab-climb-theta 0.5 --bab-climb-recheck-k 2 \ | ||
| --bab-multi-split-levels 1 --bab-max-batch-size 16 \ | ||
| --bab-max-depth 10 --bab-max-subproblems 90 --timeout 80 \ | ||
| --device cpu --dtype float64 --verbose 2>&1) | ||
| echo "$out" | ||
| grep -qE "climb_cores_inserted: [1-9]" <<<"$out" | ||
| grep -qE "climb_main_bound_calls: [1-9]" <<<"$out" | ||
| grep -qE "climb_propagate_time_s: (0\.[0-9]*[1-9]|[1-9])" <<<"$out" |
There was a problem hiding this comment.
Could you make sure the below:
(1) Options in command line will also have the same mirrored one in yaml?
(2) Try to reduce the number of command line here in the CI file if possible
(3) I am not sure what grep commandline is doing here. Are these grep lines doing validation? I would suggest adding more assertions in your code so that we could catch any issues or implementation bugs and pinpoint them in the source code.
Please do so in the below two CI tests too.
| @@ -8,46 +8,55 @@ | |||
| # | |||
There was a problem hiding this comment.
The current bab.py is too large and should be simplified and obsolete code should be removed.
| # All tensor shapes follow the (N, D) batch convention for batch-parallel scoring. | ||
| # | ||
| # ===---------------------------------------------------------------------====# | ||
|
|
There was a problem hiding this comment.
This branching.py is too large close to 2k lines of code after your update. Redundant or obsolete code should be removed for future maintanance purposes.
…to branching/ and node.py; take CLIMB margins and BaB batch size from central config
0a112c5 to
881935b
Compare
… CLIMB CI budget 250 subproblems
…it, top-k pool, MCTS visits, witness decisions
…stored tensors instead of re-running the batched wrapper
…); smart_turn CI step asserts the rejection instead of || true
| set -e | ||
| test "$status" -eq 3 |
There was a problem hiding this comment.
Do we need to set +e and test? Can we use raise asserts instead?
| --timeout 20 --bab-max-depth 2 --bab-max-subproblems 5 >/dev/null 2>&1 | ||
| status=$? | ||
| set -e |
There was a problem hiding this comment.
Could we use raise assert?
| set +e | ||
| out=$(coverage run -p -m act.back_end --verify \ | ||
| --network "$ACT_NETS_DIR/mlp_plain_3x8_64x64_3962224133.json" \ | ||
| --solver dual --bab --bab-preset climb \ | ||
| --bab-bounding random --bab-max-depth 1 --bab-max-subproblems 1 2>&1) | ||
| status=$? | ||
| set -e | ||
| echo "$out" | ||
| test "$status" -eq 2 |
There was a problem hiding this comment.
Could we use raise asert instead of outputing them in a text file?
There was a problem hiding this comment.
Where are all asserts added in the backend folder? I didn't find the changes you made?
There was a problem hiding this comment.
Please point me to where the asserts were added. If not, please try to do another round of searching, fix the "print errors" and make them all as strict assertions.
| # Implements the 2^k sign-combination fan-out described in "Mining Verdict | ||
| # Boundaries for Neural Network Verification" (Jiawei Ren, Guanqin Zhang, | ||
| # Zhenya Zhang, Yulei Sui, FM 2026). Each lane's top-k BaBSR-scored neurons | ||
| # are split together into all 2^k sign combinations in a single wave; the | ||
| # joint gain is super-additive versus k greedy single splits. |
There was a problem hiding this comment.
should put ecoop and this FM in the vnnlib-comp references, as both are implemented in ACT
| intermediate_refine: "all" | ||
| multi_split_levels: 4 | ||
|
|
||
| climb: |
There was a problem hiding this comment.
better to explain the options in comments, as quite a number of variables/options in this file need a description.
…d, util, vnncomp); explicit fallbacks; fix NaN in HybridZ softmax ratio bound
core: raise on errors instead of printing or returning empty
| @@ -0,0 +1,84 @@ | |||
| #===- act/front_end/vnnlib_loader/test_multi_input_rejection.py - Multi-Input --====# | |||
There was a problem hiding this comment.
what is this file for? Do we need it or could some of these put in the CI?
There was a problem hiding this comment.
it's for my local testing, deleted.
| # Layout (all under the single top-level `backend:` mapping): | ||
| # runtime selectors → verification cascade → torchlp → tf → hybridz | ||
| # → bab (branch-and-bound) | ||
| # Layout: |
There was a problem hiding this comment.
For all the options (variable names), please try to add a comment for each variable.
…ced in source Remove the three set +e exit-status steps (smart_turn multi-input, top-k with random/mcts, CLIMB with non-TopK bounding) and the smart_turn download. The rejections are unchanged: BaBConfig.__post_init__ and validate_climb_config raise ConfigError (back-end CLI exit 2), and the VNNLIB pre-scan raises UnsupportedSpecError (pipeline exit 3).
Comments only; values are unchanged (the YAML parses identically and check_parity passes).
9b4036a to
da67f3d
Compare
Every key now has its own comment giving its unit, valid values and special values, checked against the code. Fixes comments that were wrong: torchlp.stagnation_patience counts iterations; backend.timeout is given in full to the LP tier and to each BaB run; hybridz.timeout null/0 falls back to backend.timeout; sigmoid_segments applies to Sigmoid only; llm_probe_neuron_topk=0 keeps the FSB fallback; bab.verbose is not read yet. Comments only; values unchanged.
Silent failures now raise:
- torch2act/act2torch test harnesses raise when a conversion or test case
fails or when nothing ran, instead of printing and exiting 0. Drop the
torch2act placeholder verification block (verify_once was commented out
and its status hard-coded to SKIPPED). act2torch reports property
outcomes on random-weight nets as counterexamples, not "Test FAILED".
- VNNLIB/TorchVision spec creation collects per-instance failures and
raises; unreadable files and invalid specs raise instead of returning
None/{}/False, and spec creators no longer fall back to hard-coded
defaults when the YAML config fails to load.
- Back end: narrow broad except clauses in witness branching, attention
slopes, the interval refresh and the TF self-heal.
|
we added assertion to replace try except and return 0 @yuleisui |
Could you list the program lines that you changed to asserts? I didn't find them in the recent commit. |
|
This is a very large pull request (52 files changed and many of them are restructured). I’d like it to be simplified by removing legacy and unused code, identifying and consolidating code with similar functionality, and reducing duplication as much as possible to make it easier to review and maintain. Please also point out in the reply where you changed or added your asserts. |
@Kaijie-liu could you also help review this pull request, as it involves quite a lot in the backend and should be compact and extendable for later work. |
• bab.py#L200: multi-split counters |
CLI commands no longer swallow failures:
- front_end (--download/--synthesis/--inference/--info), pipeline
(--download/--info) and the vnnlib/torchvision loader CLIs re-raise after
printing their hints, assert that every download/inference result is
'success', and drop catch-all handlers, so a failed step exits non-zero
(CI's --synthesis step previously exited 0 on failure).
- Loaders let exceptions propagate instead of converting them into
{'status': 'error'} dicts; a partially failed dataset or VNNLIB category
download, an unreadable info.json/instances.csv, and a failed batch load
now raise where they happen.
Silent fallbacks become assertions or propagated errors:
- VNNLIB: an unparsable property no longer yields empty input bounds, and
bounds on X_i beyond the declared inputs are asserted.
- ONNX Where/MinMax/Compare no longer guess an output shape when operand
shapes do not broadcast; constant-subgraph evaluation and ASSERT-layer
re-encoding errors propagate; the fuzzing report no longer zeroes
coverage on error; BERT tokenisation falls back to regex only when nltk
or its data is missing; solver "auto" picks Gurobi only when gurobipy is
importable instead of hiding Gurobi errors.
- model_inference handles parameter-free models and unlabelled or
non-classification outputs instead of crashing (previously masked by the
--synthesis catch-all).
Legacy, unused and duplicated code removed:
- Unreferenced legacy helpers: ACTStats/ACTLog (util/stats.py); the unused
PerformanceProfiler/ParallelExecutor/ProgressTracker/retry/timeout harness
in pipeline/verification/utils.py and its act.pipeline re-exports;
Config.to_yaml (x2); eight unused Net/Layer accessors in back_end/core.py;
convert_and_save_pytorch; net_factory.append_concat; get_solver_mode.
- branching.py: the serial-evaluation fallback for "legacy solvers" was
unreachable (FSB always receives a DualSolver, the only solver that
implements compute_certified_bound); removed with its two catch-all
except clauses, so a wrong candidate dimension now raises.
- pipeline_cli: the five data-model commands (list/search/info/download/
list-downloaded) duplicated frontend_cli's unified handlers; dispatch to
those instead.
|
split this large pr in the future following pr. now closde here. |
Part 1 of 3 of the TensorCE work (#115): the changes that are independent of the BaB/CLIMB restructuring. Errors are raised where they occur instead of printed or swallowed: - back_end core/serialization/layer_util/solver_hz/hybridz_tf and util raise instead of printing or returning empty results; fix a NaN in the HybridZ softmax ratio bound. - vnnlib: reject multi-input properties before parsing (pipeline exit 3); fuzzing exits 1 on failure and writes counterexample witnesses from the stored tensors. - torch2act/act2torch harnesses raise on failed conversions or test cases and when nothing ran; spec creation raises per-instance failures; the front_end, pipeline and loader CLIs assert download/inference success and re-raise after printing their hints instead of exiting 0. Torch->ACT conversion: - Convert nn.ReLU6 and F.adaptive_avg_pool2d (torchvision mobilenet_v2; CI's torch2act step hid 4/36 failed conversions behind PASSED). - Enter chain conversions (BatchNorm -> SCALE + BIAS, c - x, DequantizeLinear) at their head: the incoming edge bypassed SCALE, so abstract interpretation ran on a different network than the PyTorch model (SVHN resnet18: output 0.95 outside the bounds -> 7e-15 after). TorchToACT.run asserts that every layer reads only variables produced by its predecessors. Legacy and duplicated code removed: ACTStats/ACTLog; the unused profiler, parallel-executor and retry/timeout harness in pipeline/verification/utils and its act.pipeline re-exports; Config.to_yaml (x2); unused Net/Layer accessors; convert_and_save_pytorch; net_factory.append_concat; get_solver_mode. pipeline_cli's data-model commands now dispatch to frontend_cli's unified handlers instead of duplicating them.
Fail loudly on errors; fix Torch->ACT conversion; remove legacy code (part 1/3 of #115)
Part 2 of 3 of #115. - Forward bounds keep explicit linear terms only for the perturbed input dimensions (DualConfig.forward_lin_max_perturbed, default 100, mirrored in backend.yaml); above the cap the forward pass is interval-only. - MaxPool gets a linear relaxation; conv bounds use centre-radius numerics with lane chunking. Fixes the lb > ub crash on VGG16.
Sound dual bounds for large conv nets (part 2/3 of #115)
Part 3 of 3 of SVF-tools#115 (parts 1 and 2 merged as SVF-tools#116 and SVF-tools#118). - CLIMB certificate reuse (opt-in): certified dual certificates are replayed as ReLU phase cores and propagated to prune BaB subproblems early (bab/climb.py). - BaB restructuring: split, violation-check and multi-split logic move out of bab.py into node.py, violation.py and branching/multi_split.py (bab.py 2191 -> 1151 lines, branching.py 1217 -> 1094). - BaB config: reuse_root_bounds becomes the root_bounds_reuse tri-state; CLIMB preset; every backend.yaml option documented; input splits can no longer pick a zero-width dimension. - CI: act-bab.yml grep checks replaced by in-source invariants and exit-status checks.
2 participants
Uh oh!
There was an error while loading. Please reload this page.