Repeat ase - #107
Open
guanqin-123 wants to merge 7 commits into
Open
Conversation
…pec.violation() Concrete violation semantics were implemented three times over: in OutputSpecLayer.forward, in bab.check_violations_batched, and again in the fuzzer's PropertyChecker. The fuzzer's copy handled only 4 of the 5 OutKinds and read the true label from seeds.label rather than the spec, so on every VNNLib benchmark valid_mask was all-False and the violation mask could never fire. A dispatch miss on UNSAFE_LINEAR returned all-False just as quietly. Both failures were silent: the fuzzer ran at full speed with normal coverage and simply reported zero counterexamples. Add OutputSpec.violation(y, rows) returning (violated, severity) for all five kinds, raising on an unhandled kind. The rows argument matters: SeedCorpus samples with replacement, so batch lane i carries a mutation of instance original_index[i], not i. Evaluating spec row i against lane i would compare one instance's output against another's label. OutputSpecLayer.forward now delegates with identity rows; PropertyChecker passes rows=seeds.original_index and keeps only counterexample materialization, losing its dispatch table and all four _check_* methods. Counterexample is rebuilt around spec_row/severity/true_class, dropping the -1 sentinels that a label-less kind was forced to carry, and summary() no longer needs the spec handed back to it. Per-row slicing, previously duplicated in bab.py and pipeline_cli.py, moves onto the shared _gather_rows helper. Missing specs and seed/spec-row misalignment now raise instead of degrading quietly. bab.check_violations_batched keeps its own eps tolerance: it validates LP-solver candidates, where numerical slack is expected. CIFAR-100 ResNet goes from 0 to ~2900 counterexamples in a 30s budget.
PGD and FGSM both fell back to maximizing output.var() whenever no label was available. VNNLib seeds carry label=None, so on those benchmarks the gradient attack was never aimed at the property at all - it optimized an unrelated objective while the schedule around it was tuned. pipeline.yaml gives pgd a weight of 0.4, so this was the strategy actually running. Drive both strategies with the severity returned by OutputSpec.violation, gathered per lane. For TOP1_ROBUST this reproduces the existing CW loss exactly, so it generalizes the objective to all five kinds rather than changing the classification case. Attack the inner network instead of the VerifiableModel wrapper: InputLayer and InputSpecLayer are tensor pass-throughs, so the logits are identical, but the wrapper's spec layers ran .sum().item() at nine sites - roughly 200 CUDA syncs per mutation across PGD's 50 steps. SeedCorpus.add hardcoded zeros for _select_counts while every sibling field indexed seeds.X[idx], and child_seeds never carried select_count forward. The adaptive perturbation schedule s_b = 1-(1-s0)^(n+1) reads n from that counter, so it was frozen at n=0 for every discovered seed. Also drop the perturb-size banner, which printed a value that the first mutate() call overwrote, and expose the synthesis grouping key so callers stop pairing seeds by id(pytorch_model) - insufficient, since synthesis also splits on InKind, OutKind and a cd_sig hash.
check_violations_batched tested MARGIN_ROBUST as (max_other - z_t) >= +margin, the wrong sign. encode_linear is the authority here: it emits rows e_j - e_t with thresholds = -margin and certifies iff max_j(z_j - z_t) < -margin, so a lane is violated iff (max_other - z_t) >= -margin. The old predicate only flagged a violation once the runner-up had beaten the target by margin, i.e. it missed every genuine counterexample in the band -margin <= gap < +margin. TOP1_ROBUST and MARGIN_ROBUST also compared with > where encode_linear uses >=. Robustness demands strict separation, so a separation of exactly the threshold already falsifies it; an argmax-based check cannot express this at all, since it resolves ties by lowest class index. All three implementations now agree on both kinds. InputSpecLayer carried the same identity-lane assumption that OutputSpecLayer had, comparing lane-indexed inputs against spec-row-indexed bounds, which left input_satisfied_per_sample silently wrong under a permuted fuzzer batch; it is now row-aware. Counterexample emission is gated on input feasibility, because the LIN_POLY projection is still a no-op and would otherwise report inputs that never satisfied the input spec as counterexamples; rejected candidates are counted rather than dropped in silence. OutputSpec also accepts a list-valued margin, matching how y_true was already handled.
Four silent failures made the fuzzer report zero counterexamples on every VNNLib benchmark: violation semantics were duplicated across three call sites and the fuzzer's copy read the label from the seed instead of the spec, bab tested MARGIN_ROBUST with the wrong sign, TF32 truncated float32 so attacks landed on fabricated sign flips, and the ONNX model cache was consulted after conversion rather than before. Binarized networks needed a straight-through estimator and pre-softmax logits on top of that, since torch.sign has no gradient and the trailing softmax saturates. CIFAR-100 goes from zero to ~107k counterexamples, TinyImageNet to 59k and traffic signs to 7.3k, with no false positives found in onnxruntime audits.
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## main #107 +/- ##
==========================================
+ Coverage 73.54% 74.00% +0.46%
==========================================
Files 91 91
Lines 20987 21159 +172
==========================================
+ Hits 15435 15659 +224
+ Misses 5552 5500 -52
Flags with carried forward coverage won't be shown. Click here to find out more.
... and 3 files with indirect coverage changes Continue to review full report in Codecov by Harness.
🚀 New features to boost your workflow:
|
yuleisui
reviewed
Aug 21, 2026
| - name: Run fuzzing at float64 (non-quantized CIFAR-100) | ||
| run: | | ||
| cd ${{ github.workspace }} | ||
| coverage run -p -m act.pipeline --fuzz --category cifar100_2024 --dtype float64 --max-instances 2 --timeout 30 --iterations 200 |
Collaborator
There was a problem hiding this comment.
What is the difference between line 112 and line 94? Why do we put cifar100_2024 under traffic signs CI but not close to cifar100 at line 94?
…00 steps It sat after the traffic signs cache and download, which made it read as part of the traffic signs block.
- Add cd_group="shape" to model synthesis so instances sharing c but differing in d group together; the fuzz CLI opts in, verification keeps the byte-valued default and is unchanged. - Key seed-corpus dedup by (spec row, tensor hash) so byte-identical seeds on different lanes survive instead of collapsing and breaking lane alignment. - lsnc_relu goes from 1040 groups of batch 1 to 13 of batch 80: 58.7x faster at equal work, with higher coverage.
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.
Unify violation semantics. Concrete violation logic existed in three
places; the fuzzer's copy handled 4 of the 5
OutKinds and read the truelabel from the seed instead of the spec, so
valid_maskwas all-false onevery VNNLib instance and an
UNSAFE_LINEARdispatch miss returned quietly.OutputSpec.violation(y, rows)is now the single implementation.Correct the violation predicates.
babtestedMARGIN_ROBUSTas(max_other − z_t) >= +margin, the wrong sign — it missed everycounterexample in
-margin <= gap < +margin.TOP1andMARGINalsocompared with
>whereencode_linearuses>=