backend tensor - #106
Open
guanqin-123 wants to merge 3 commits into
Open
Conversation
Codecov Report❌ Patch coverage is
❌ Your patch check has failed because the patch coverage (54.51%) is below the target coverage (65.00%). You can increase the patch coverage or adjust the target coverage. Additional details and impacted files@@ Coverage Diff @@
## main #106 +/- ##
==========================================
- Coverage 73.53% 73.17% -0.36%
==========================================
Files 91 91
Lines 20508 20987 +479
==========================================
+ Hits 15080 15357 +277
- Misses 5428 5630 +202
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:
|
yuleisui
reviewed
Jul 27, 2026
| coverage run -p -m act.pipeline --verify vnnlib --category acasxu_2023 --max-instances 2 \ | ||
| --solvers dual --bab --bab-solver-tier dual_alpha_eta \ | ||
| --bab-bounding-method topk --bab-branching-method babsr \ | ||
| --bab-bounding depth_lb --bab-branching-method babsr \ |
Collaborator
There was a problem hiding this comment.
What does depth_lb mean here? Could you make the name easier to understand and add a comment to where it is defined (e.g., in the config.yaml and cli.py)
yuleisui
reviewed
Jul 27, 2026
| # by a swappable order strategy; supports frontier-cap eviction (``evict_to``), | ||
| # which drops worst-priority leaves and forces a sound ``UNKNOWN``. | ||
| # * ``MCTSBounding`` — MCTS side tables (``N``/``Q``) over the BaB tree, maintained as | ||
| # a pure observer; ``pop`` is plain top-k until UCB1 selection lands. |
Collaborator
There was a problem hiding this comment.
Fix these comments to reflect the below bounding strategies using a table with explanations, and better to rename depth_lb, sa and diverse.
"random",
"depth_lb",
"greedy",
"sa",
"diverse",
"mcts",
Collaborator
There was a problem hiding this comment.
Also fix the top-k and make sure it works as a parameter and only for the first three options.
Addresses the three review comments on PR SVF-tools#106. Bounding strategies renamed (hard rename, no aliases -- old names now fail at argparse): depth_lb -> depth_bound_blend, sa -> annealed, diverse -> diverse_split_signs. greedy/random/mcts unchanged. Note depth_bound_blend is NOT greedy: GreedyOrder is the pure-bound special case of the depth+urgency blend. The strategy table is now in all four places the reviewer asked for: the bounding.py module header, above VALID_BOUNDINGS in config.py, above `bounding:` in backend.yaml, and both CLIs' --help. top_k is a real parameter instead of a name baked into a strategy string: BaBConfig.top_k, --bab-top-k on both CLIs, k=0 meaning unbounded to match frontier_cap. Capping pop never discards a subproblem -- the remainder stays pooled -- so unlike evict_to it is a scheduling knob, not a soundness one. Honoured by the four TopKBounding-family strategies (diverse_split_signs is a TopKBounding subclass, so excluding it would be arbitrary); random and mcts raise rather than silently ignore it. Shipping top_k alone would have silently changed `annealed`: pop skips scoring when the pool already fits the wave while evict_to scores anyway, so the annealing temperature tracked pool size and eviction pressure rather than elapsed waves. SAOrder.advance_schedule() is now called once per pop in all three pooling strategies and never by evict_to. Joint multi-neuron splitting is decoupled from branching_method == "gain": scoring a split and materializing 2^k children are orthogonal, and the k neurons come from the BaBSR heuristic either way. --bab-multi-split-levels is added to the pipeline CLI, where joint splitting was previously unreachable. Two effectiveness bugs fixed: k_eff no longer collapses to the minimum over lanes (one candidate-starved lane disabled the whole wave), and six telemetry counters plus a one-shot warning make the log2 memory clamp observable -- it needs effective_batch >= lanes * 2^k, so the default batch of 8 left the feature dormant. --solver dual no longer discards explicitly-passed BaB flags; it is now a defaults-only preset. The workflow job passing --multi-split-levels 3 was silently getting 4. Also: witness-residual branching scores neurons by the relaxation gap realized at the dual solver's spurious counterexample, delegating the concrete forward pass to compute_forward_bounds on a degenerate box rather than re-implementing a layer-kind dispatch (11 -> 48 kinds covered).
onnx-simplifier 0.5.0 declares its compiled backend `onnxsim` with no version constraint, so CI silently picked up 0.7.0 (released one day after the last green run) and then 0.7.1. 0.7.x rewrites ViT attention into a MatMul that torch2act rejects: OnnxMatMul at _1_1_0_1_0_0_fn_fn_1_mat_mul_1: incompatible var-var shapes (1, 3, 5, 5) @ (1, 3, 1, 16) Bisected by diffing the pip output of the last green run against the red one: onnxsim 0.6.5 -> 0.7.1 was the only package that moved. Reproduced locally by swapping only onnxsim -- 0.6.2 and 0.6.5 pass, 0.7.1 fails with the identical node name and shapes. Pinned in all six workflows plus environment.yml; vit_2023 verified under both CI combos. backend.yaml gains a branching_method table (which over-approximated activation or input axis gets split, and which entries need a dual_alpha* tier), and the bounding table's last column becomes selection determinism rather than top-k applicability -- only annealed and random draw from an RNG, which is what governs run-to-run reproducibility. provenance_enabled is documented too. branching.py cites the FM 2026 paper on the joint-split section banner and drops the module header's reference to MultiNeuronSplitBranching, a class that does not exist; the entry point is _multi_split_from_decision.
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
2 participants
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.
Uh oh!
There was an error while loading. Please reload this page.