Skip to content

FIX: Have output spec shape verifier working with batched models#75

Merged
yuleisui merged 5 commits into
SVF-tools:mainfrom
hanyuone:frontend-dtype
Jun 4, 2026
Merged

FIX: Have output spec shape verifier working with batched models#75
yuleisui merged 5 commits into
SVF-tools:mainfrom
hanyuone:frontend-dtype

Conversation

@hanyuone

@hanyuone hanyuone commented Jun 4, 2026

Copy link
Copy Markdown
Contributor

Because of batching, y_true in OutputSpecs are concatenated. The original check for whether y_true is a valid class no longer works - 0 <= spec.y_true < num_classes is syntactic sugar for 0 <= spec.y_true and spec.y_true < num_classes, and the output for both comparisons is a boolean tensor, which cannot be directly anded.

This PR fixes this bug, and patches both create_specs.py to reflect the output of self.validate_spec_pair_with_model, which now returns an (is_valid, errors) tuple.

@codecov

codecov Bot commented Jun 4, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 71.81%. Comparing base (5a3e1b7) to head (a1098cc).

Additional details and impacted files
@@            Coverage Diff             @@
##             main      #75      +/-   ##
==========================================
- Coverage   71.83%   71.81%   -0.03%     
==========================================
  Files          86       86              
  Lines       14902    14903       +1     
==========================================
- Hits        10705    10702       -3     
- Misses       4197     4201       +4     
Flag Coverage Δ
bab 46.66% <25.00%> (-0.01%) ⬇️
backend-float32 49.07% <0.00%> (-0.04%) ⬇️
backend-float64 49.12% <0.00%> (-0.01%) ⬇️
frontend 38.49% <100.00%> (+<0.01%) ⬆️
pipeline-fuzz 19.16% <75.00%> (-0.01%) ⬇️
pipeline-verify 38.20% <100.00%> (+<0.01%) ⬆️

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

Files with missing lines Coverage Δ
act/front_end/spec_creator_base.py 59.85% <100.00%> (+0.29%) ⬆️
act/front_end/torchvision_loader/create_specs.py 70.86% <100.00%> (ø)
act/front_end/vnnlib_loader/create_specs.py 84.69% <100.00%> (ø)

... 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 5a3e1b7...a1098cc. Read the comment docs.

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

@yuleisui

yuleisui commented Jun 4, 2026

Copy link
Copy Markdown
Collaborator

Please fix the coverage issue. @hanyuone

@guanqin-123

Copy link
Copy Markdown
Contributor

It would be better to squash the commits into one for easier maintaining.

@yuleisui yuleisui merged commit e831a0f into SVF-tools:main Jun 4, 2026
8 checks passed
@hanyuone hanyuone deleted the frontend-dtype branch June 4, 2026 07:06
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