phase II dual solver: bab with alpha and eta

[guanqin-123]

Adds per-neuron ReLU lower-slope optimization and split-constraint Lagrangians, with $\eta$ to DualSolver, jointly optimized via Adam for bab part.

[codecov]

Codecov Report

❌ Patch coverage is 77.58621% with 91 lines in your changes missing coverage. Please review.
✅ Project coverage is 70.86%. Comparing base (073467c) to head (74b107a).
⚠️ Report is 1 commits behind head on main.

Files with missing lines	Patch %	Lines
act/back_end/solver/solver_dual.py	66.91%	44 Missing ⚠️
act/back_end/bab/bab.py	78.39%	35 Missing ⚠️
act/back_end/bab/branching/branching.py	70.58%	5 Missing ⚠️
act/back_end/dual_tf/tf_forward.py	84.37%	5 Missing ⚠️
act/back_end/dual_tf/tf_mlp.py	88.88%	2 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main      #70      +/-   ##
==========================================
+ Coverage   70.66%   70.86%   +0.20%     
==========================================
  Files          86       86              
  Lines       13930    14308     +378     
==========================================
+ Hits         9843    10139     +296     
- Misses       4087     4169      +82     

Flag	Coverage Δ
bab	45.32% <74.38%> (+11.63%)	⬆️
backend-float32	50.38% <12.80%> (-1.15%)	⬇️
backend-float64	50.43% <12.80%> (-1.15%)	⬇️
frontend	39.86% <6.15%> (-0.98%)	⬇️
pipeline-fuzz	19.33% <0.24%> (-0.52%)	⬇️
pipeline-verify	37.77% <28.07%> (+3.31%)	⬆️

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

Files with missing lines	Coverage Δ
act/back_end/bab/branching/__init__.py	100.00% <100.00%> (ø)
act/back_end/bab/node.py	97.10% <100.00%> (+0.94%)	⬆️
act/back_end/config.py	90.37% <100.00%> (+1.11%)	⬆️
act/back_end/dual_tf/__init__.py	100.00% <ø> (ø)
act/back_end/dual_tf/dual_tf.py	59.67% <100.00%> (ø)
act/back_end/dual_tf/tf_cnn.py	84.71% <100.00%> (ø)
act/back_end/dual_tf/tf_rnn.py	100.00% <100.00%> (ø)
act/back_end/dual_tf/tf_smooth.py	96.29% <ø> (ø)
act/back_end/dual_tf/tf_transformer.py	100.00% <100.00%> (ø)
act/back_end/solver/solver_base.py	77.77% <ø> (ø)
... and 5 more

... and 1 file with indirect coverage changes

---

Continue to review full report in Codecov by Sentry.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 073467c...74b107a. Read the comment docs.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[guanqin-123]

@yuleisui In this pr, we finished the optimizable lower bound and brand and bound computation in the (dual) solver.
And another thing is for now, (three solvers - interval, dual, hz) verify once (batched verification) with multiple instances, and bab (batch subproblems) with one instance are detached, but they share the same tf_s and backend solver. Can we have a new ipynb for BaB, so we can explicitly demonstrate the uniqueness of each part?

[yuleisui]

@yuleisui In this pr, we finished the optimizable lower bound and brand and bound computation in the (dual) solver. And another thing is for now, (three solvers - interval, dual, hz) verify once (batched verification) with multiple instances, and bab (batch subproblems) with one instance are detached, but they share the same tf_s and backend solver. Can we have a new ipynb for BaB, so we can explicitly demonstrate the uniqueness of each part?

You could update the verify ipynb instead of creating a new one in the next pull request.

For this pr, can we keep optimise the performance to include larger benchmarks?

[yuleisui]

Is this supposed to be torchvision?

[guanqin-123]

yes, now we are supporting torchvision model for verification

[yuleisui]

I couldn’t find the code related to counterexample handling during inference.

1. If the counterexample produced by the verifier is genuine after inference, should the corresponding subproblem in the batch stop while the others continue to be explored?

2. If the counterexample produced by the verifier is spurious, what iterative operation should be performed for subproblem partitioning? What heuristics are used? Did you consider node depth and solver results (quantitative assessment), this should be treated as one of the baseline heuristics.

[guanqin-123]

1. in the batch bab main function for batched spurious counterexample generation. After checking, the rest of unresolved subproblems are continued for splitting in the new batch tensor

[guanqin-123]

2. Now I capped the subproblem depth. I can do the quant assessment in this pr.

[yuleisui]

Need to use ecoop one as a baseline