Repository navigation
BaB restructuring, CLIMB certificate reuse and CI invariants (part 3/3 of #115) - #119
Merged
Merged
Conversation
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.
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## main #119 +/- ##
==========================================
+ Coverage 76.85% 77.63% +0.78%
==========================================
Files 91 95 +4
Lines 22367 23009 +642
==========================================
+ Hits 17191 17864 +673
+ Misses 5176 5145 -31
Flags with carried forward coverage won't be shown. Click here to find out more.
... and 8 files with indirect coverage changes Continue to review full report in Codecov by Harness.
🚀 New features to boost your workflow:
|
Collaborator
|
Could you add asserts where necessary and replace return/print with asserts. |
- backend_cli: errors in --verify/--generate/--diff-nets/--self-test and the serialization test propagate (traceback, exit 1) instead of being printed and mapped to a return code; "no verdict" is an assertion. The explicit unsupported-layer skip (exit 1) and ConfigError (exit 2) keep their exit codes. config.py's self-test raises on the first failure. - solver_dual: a net without an INPUT layer, missing INPUT bounds, a non-tensor DENSE weight and a RELU layer without bounds are assertion failures instead of silently disabling the refresh/alpha. - climb.certificate_replay asserts the solver returned nu_per_layer. - node.split_neurons asserts the child count and parent_index length.
Contributor
Author
revised |
Collaborator
|
Could you add a new Jupyter notebook file to demonstrate tensor bab? |
Collaborator
|
When adding a demo .ipynb, try to simplify these 3 patches too and delete/remove unused code where necessary. |
- ipynb/tensor_bab.ipynb and its README section: K-batched branch-and-bound on three VNN-COMP instances, each decided only after branching: ACAS Xu prop_3 CERTIFIED and prop_2 FALSIFIED (input splitting), and a CIFAR-100 ResNet CERTIFIED (neuron splitting), with the per-iteration trace, plots and the counterexample check. - verify_bab_batched: public `trace` parameter replaces the private `_k_log`; result metadata gains `iterations`. - Delete the zero-reference Layer.get_bounds_for_var, ConSet._is_op_supported_by_exporter, VerifyResult.is_conclusive, VerifyResult.is_safe and SpecBatchResult.worst_violation, and the unused imports and locals flagged by ruff F401/F841/F811 in 17 files.
The SVHN host (ufldl.stanford.edu) is down, so `python -m act.front_end --download SVHN` crashed with URLError and failed the Frontend Tests job. - act/util/download_utils.py: a new "unavailable" download status. is_source_unreachable() treats DNS failures, refused or reset connections, timeouts, unreachable hosts and HTTP 502/503/504 as an outage; any other HTTP status (e.g. 404) stays an error. report_unavailable() prints a SKIPPED notice and, under GitHub Actions, a warning annotation. - The TorchVision and VNNLIB loaders return "unavailable" when every attempt failed that way, after removing the directories the attempt created (an empty raw/ made later calls treat the dataset as downloaded). - The unified --download (act.front_end and act.pipeline) and both loader CLIs report it as a skip and exit 0; every other failure still fails.
Contributor
Author
added. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part 3 of 3 of #115 (parts 1 and 2 merged as #116 and #118); a single commit on
main.bab.pyintonode.py,violation.py,branching/multi_split.py(bab.py2191 → 1151 lines,branching.py1217 → 1094).reuse_root_boundsbecomes theroot_bounds_reusetri-state; CLIMB preset; everybackend.yamloption documented; input splits can no longer pick a zero-width dimension.act-bab.ymlgrep checks replaced by in-source invariants and exit-status checks.