Skip to content

feat(hybridz): add affine and structural operators#90

Merged
yuleisui merged 1 commit into
SVF-tools:mainfrom
Kaijie-liu:hybridz-pr2-affine-structural-20260706
Jul 7, 2026
Merged

feat(hybridz): add affine and structural operators#90
yuleisui merged 1 commit into
SVF-tools:mainfrom
Kaijie-liu:hybridz-pr2-affine-structural-20260706

Conversation

@Kaijie-liu

Copy link
Copy Markdown
Contributor

PR2 Summary by file:

  • solver_hz.py: adds generator ids and shared-generator algebra for HybridZ, including Add/Sub/Concat support while preserving correlations.
  • hybridz_tf.py: reuses input generator ids across matching input boxes and tracks HybridZ side-state changes for the worklist.
  • tf_mlp.py: adds HybridZ propagation for affine/structural MLP ops such as BN, Add/Sub/Concat, shape ops, ReduceSum, and point-constant Mul/Div/MatMul.
  • tf_cnn.py: adds HybridZ propagation for affine CNN ops, including Conv2D, ConvTranspose2D, and AvgPool2D; keeps MaxPool on interval fallback.

@codecov

codecov Bot commented Jul 6, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 69.34189% with 191 lines in your changes missing coverage. Please review.
✅ Project coverage is 73.48%. Comparing base (b72b768) to head (d964759).

Files with missing lines Patch % Lines
act/back_end/solver/solver_hz.py 45.07% 106 Missing ⚠️
act/back_end/hybridz_tf/tf_mlp.py 77.57% 74 Missing ⚠️
act/back_end/hybridz_tf/tf_cnn.py 88.00% 6 Missing ⚠️
act/back_end/hybridz_tf/hybridz_tf.py 90.00% 5 Missing ⚠️
Additional details and impacted files
@@            Coverage Diff             @@
##             main      #90      +/-   ##
==========================================
- Coverage   73.62%   73.48%   -0.15%     
==========================================
  Files          92       92              
  Lines       18993    19585     +592     
==========================================
+ Hits        13984    14392     +408     
- Misses       5009     5193     +184     
Flag Coverage Δ
bab 46.37% <8.50%> (-1.19%) ⬇️
backend-float32 48.27% <69.18%> (+0.63%) ⬆️
backend-float64 48.29% <69.18%> (+0.62%) ⬆️
frontend 32.95% <8.50%> (-0.77%) ⬇️
pipeline-fuzz 19.12% <8.50%> (-0.34%) ⬇️
pipeline-verify 38.99% <18.61%> (-0.70%) ⬇️

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

Files with missing lines Coverage Δ
act/back_end/hybridz_tf/hybridz_tf.py 92.52% <90.00%> (-4.54%) ⬇️
act/back_end/hybridz_tf/tf_cnn.py 90.42% <88.00%> (-2.76%) ⬇️
act/back_end/hybridz_tf/tf_mlp.py 87.22% <77.57%> (-5.04%) ⬇️
act/back_end/solver/solver_hz.py 51.29% <45.07%> (-11.21%) ⬇️

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 b72b768...d964759. Read the comment docs.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

@Kaijie-liu Kaijie-liu force-pushed the hybridz-pr2-affine-structural-20260706 branch from 1d01c55 to fa20113 Compare July 6, 2026 11:48
Comment thread act/back_end/hybridz_tf/hybridz_tf.py Outdated
self._input_ids: Optional[torch.Tensor] = None
self._input_box: Optional[tuple] = None

def _input_box_matches(self, bounds: Bounds) -> bool:

@guanqin-123 guanqin-123 Jul 6, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe our bounds have been already settled in the model and spec synthesis phase, why we still need this flattening?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed, this was not recomputing bounds, only a guard for reusing input generator ids so correlations such as x - x can remain exact. But comparing bounds is not clean when ACT already has stable variable ids via Layer.in_vars/out_vars. I switched to seeding col_ids directly from those ids (INPUT -> out_vars, input-reading root -> in_vars), with a disjoint id block per batch item and a negative id namespace for fresh auxiliary generators. _input_box_matches is removed.

)


def _spatial_op_generators(G, op_fn, B, C, H, W, n_out_per_sample):

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

can you leverage the math expression here with what is spatial operation?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

“spatial operation” means a linear BCHW operator S, e.g. AvgPool2D or ConvTranspose2D without bias. For y = S(x)+b and x = c+G·ξ, HybridZ propagates c' = S(c)+b and G'[:,j] = vec(S(unvec(G[:,j]))) (the bias affects only the center). The helper applies S to each generator column by reshaping columns into BCHW tensors, so it avoids materializing the large matrix for S. I added a short docstring with this math.

return torch.ones(int(hz.Ac.shape[0]), dtype=torch.bool, device=hz.Ac.device)


def _shared_constraint_prefix(

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is hard to understand the usability. Can you leave some comment within/ above your code?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These helpers implement shared-generator algebra for Add/Sub, and the same generator-alignment idea is used for Concat: matching col_ids denote the same latent factor, so correlated terms can combine exactly instead of being duplicated as independent Minkowski terms (x - x = 0, not [-2r, 2r]). If ids are unavailable, we back to the sound Minkowski construction. I added short docstrings to hz_from_bounds, _align, _scatter_cols, _shared_constraint_prefix, and hz_sgm_add.

@Kaijie-liu Kaijie-liu force-pushed the hybridz-pr2-affine-structural-20260706 branch from fa20113 to d964759 Compare July 7, 2026 00:42
bcol_ids: Optional[torch.Tensor] = None


_NEXT_COL_ID = [-1]

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

what is this?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the counter for new HZ generator ids.

These ids are used when merge or align HZ generator cols, e.g. in Add/Sub/Concat. If two cols have the same id, they represent the same latent factor and should be combined; if the ids differ, they are independent factors.

Now the original input generators use ACT's variable ids from Layer.in_vars/out_vars, which are non-negative. Later, when HZ creates extra generators, e.g. for ReLU/Sigmoid/slack encodings, those new generators also need ids. If we start fresh ids from 0, they may collide with ACT input variable ids and be incorrectly merged.

So fresh internal ids are allocated on negative: -1, -2, -3, ...
They are only symbolic labels for matching generator cols, not tensor indices or ACT variable ids.

@yuleisui yuleisui merged commit a59cfa8 into SVF-tools:main Jul 7, 2026
8 checks passed
@Kaijie-liu Kaijie-liu deleted the hybridz-pr2-affine-structural-20260706 branch July 8, 2026 01:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants