BranchCore work by guanqin-123 · Pull Request #115 · SVF-tools/ACT

guanqin-123 · 2026-09-23T01:35:53Z

CLIMB certificate reuse (opt-in): replays certified dual certificates as ReLU phase cores and propagates them to prune BaB subproblems early.
Sound dual bounds for large conv nets (VGG16): forward bounds are symbolic only in the perturbed dimensions and MaxPool has a linear relaxation, with centre–radius numerics and lane chunking. Fixes the lb > ub crash.
BaB config and branching fixes: reuse_root_bounds becomes the root_bounds_reuse tri-state and a forward_lin_max_perturbed cap is added. Input splits can no longer pick a zero-width dimension.

codecov · 2026-09-23T01:45:08Z

Codecov Report

❌ Patch coverage is 78.46594% with 452 lines in your changes missing coverage. Please review.
✅ Project coverage is 76.62%. Comparing base (e9ed992) to head (c88e1cd).

Files with missing lines	Patch %	Lines
act/back_end/bab/branching/multi_split.py	51.95%	86 Missing ⚠️
act/back_end/bab/violation.py	59.62%	86 Missing ⚠️
act/back_end/bab/node.py	63.15%	56 Missing ⚠️
act/back_end/bab/climb.py	90.76%	52 Missing ⚠️
act/back_end/dual_tf/tf_forward.py	81.48%	35 Missing ⚠️
act/back_end/solver/solver_dual.py	84.18%	31 Missing ⚠️
act/back_end/bab/bab.py	80.43%	27 Missing ⚠️
act/back_end/bab/branching/branching.py	76.31%	27 Missing ⚠️
act/back_end/bab/branching/bounding.py	71.73%	13 Missing ⚠️
act/util/device_manager.py	73.33%	8 Missing ⚠️
... and 9 more

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #115      +/-   ##
==========================================
+ Coverage   75.44%   76.62%   +1.17%     
==========================================
  Files          91       94       +3     
  Lines       22575    23440     +865     
==========================================
+ Hits        17032    17960     +928     
+ Misses       5543     5480      -63

Flag	Coverage Δ
bab	`50.57% <74.27%> (+7.01%)`	⬆️
backend-float32	`49.32% <35.49%> (-0.17%)`	⬇️
backend-float64	`51.04% <35.87%> (-0.22%)`	⬇️
frontend	`30.92% <10.10%> (-0.63%)`	⬇️
pipeline-fuzz	`20.13% <8.62%> (-0.24%)`	⬇️
pipeline-verify	`42.67% <34.25%> (+1.02%)`	⬆️

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

Files with missing lines	Coverage Δ
act/back_end/__init__.py	`100.00% <ø> (ø)`
act/back_end/bab/__init__.py	`100.00% <100.00%> (ø)`
act/back_end/hybridz_tf/hybridz_tf.py	`95.76% <100.00%> (+0.28%)`	⬆️
act/back_end/hybridz_tf/tf_transformer.py	`78.60% <100.00%> (+0.32%)`	⬆️
act/back_end/layer_util.py	`69.74% <100.00%> (+0.89%)`	⬆️
act/back_end/net_factory.py	`88.25% <100.00%> (+0.43%)`	⬆️
act/back_end/serialization/serialization.py	`88.09% <100.00%> (+12.09%)`	⬆️
act/back_end/verifier.py	`83.91% <100.00%> (-0.32%)`	⬇️
act/front_end/spec_creator_base.py	`61.80% <100.00%> (ø)`
act/util/format_utils.py	`95.65% <100.00%> (+8.69%)`	⬆️
... and 19 more

... and 3 files 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 e9ed992...c88e1cd. 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-09-23T02:54:34Z

Please fix the coverage ci

guanqin-123 · 2026-09-23T04:32:41Z

Please fix the coverage ci

Finished. after this, the upcoming pr to support SST, and YELP (NLP verification instance that contains a transformer architecture)

yuleisui · 2026-09-23T04:54:49Z

+            --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"


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.

yuleisui · 2026-09-23T04:56:16Z

@@ -8,46 +8,55 @@
 #


The current bab.py is too large and should be simplified and obsolete code should be removed.

yuleisui · 2026-09-23T04:57:13Z

 #   All tensor shapes follow the (N, D) batch convention for batch-parallel scoring.
 #
 # ===---------------------------------------------------------------------====#



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

… 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

yuleisui · 2026-09-25T00:44:44Z

+          set -e
+          test "$status" -eq 3


Do we need to set +e and test? Can we use raise asserts instead?

yuleisui · 2026-09-25T00:45:09Z

+              --timeout 20 --bab-max-depth 2 --bab-max-subproblems 5 >/dev/null 2>&1
+            status=$?
+            set -e


Could we use raise assert?

yuleisui · 2026-09-25T00:45:38Z

+          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


Could we use raise asert instead of outputing them in a text file?

yes, now fix.

Where are all asserts added in the backend folder? I didn't find the changes you made?

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.

@guanqin-123 please review and update.

yuleisui · 2026-09-25T00:47:33Z

+#   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.


should put ecoop and this FM in the vnnlib-comp references, as both are implemented in ACT

yuleisui · 2026-09-25T00:59:55Z

+    intermediate_refine: "all"
+    multi_split_levels: 4
+
+  climb:


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

yuleisui · 2026-09-25T05:21:10Z

@@ -0,0 +1,84 @@
+#===- act/front_end/vnnlib_loader/test_multi_input_rejection.py - Multi-Input --====#


what is this file for? Do we need it or could some of these put in the CI?

it's for my local testing, deleted.

yuleisui · 2026-09-25T05:22:01Z

-# Layout (all under the single top-level `backend:` mapping):
-#   runtime selectors → verification cascade → torchlp → tf → hybridz
-#   → bab (branch-and-bound)
+# Layout:


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).

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.

BranchCore work

528452d

update for newly added climb functions

0b42029

guanqin-123 force-pushed the TensorCE branch from d9327ac to 0b42029 Compare September 23, 2026 04:09

yuleisui reviewed Sep 23, 2026

View reviewed changes

guanqin-123 added 2 commits September 24, 2026 07:18

refine code structure

dfa6f4e

add climb, violation and multi_split modules; move BaB split logic in…

881935b

…to branching/ and node.py; take CLIMB margins and BaB batch size from central config

guanqin-123 force-pushed the TensorCE branch from 0a112c5 to 881935b Compare September 24, 2026 00:50

guanqin-123 added 4 commits September 24, 2026 11:30

replace CLIMB CI greps with exit-status checks: config errors exit 2,…

d942158

… CLIMB CI budget 250 subproblems

replace remaining act-bab CI greps with in-code invariants: multi-spl…

673bfef

…it, top-k pool, MCTS visits, witness decisions

fuzz: exit 1 when fuzzing fails; write counterexample witnesses from …

63f0a0c

…stored tensors instead of re-running the batched wrapper

vnnlib: reject multi-input properties before parsing (pipeline exit 3…

b072b22

…); smart_turn CI step asserts the rejection instead of || true

yuleisui reviewed Sep 25, 2026

View reviewed changes

guanqin-123 and others added 2 commits September 25, 2026 13:48

core: raise on errors instead of printing or returning empty (back_en…

ee92e9d

…d, util, vnncomp); explicit fallbacks; fix NaN in HybridZ softmax ratio bound

Merge pull request #5 from guanqin-123/CLIMB

c9f8a90

core: raise on errors instead of printing or returning empty

yuleisui reviewed Sep 25, 2026

View reviewed changes

guanqin-123 added 2 commits September 25, 2026 15:34

config: document every backend.yaml option and the CLIMB preset

da67f3d

Comments only; values are unchanged (the YAML parses identically and check_parity passes).

guanqin-123 force-pushed the TensorCE branch from 9b4036a to da67f3d Compare September 25, 2026 05:35

		@@ -0,0 +1,84 @@
		#===- act/front_end/vnnlib_loader/test_multi_input_rejection.py - Multi-Input --====#

Conversation

guanqin-123 commented Sep 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

yuleisui commented Sep 23, 2026

Uh oh!

guanqin-123 commented Sep 23, 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!

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

guanqin-123 commented Sep 23, 2026 •

edited

Loading

codecov Bot commented Sep 23, 2026 •

edited

Loading