star: Star.dualBounds — batched weak-duality (beta-CROWN-style) bounds over the star's own predicate constraints

[ttj]

All paths relative to the nnv repo root; verified on master @ 376568b44. Gated by the relaxFactor=0 ceiling probe issue; per category it COMPETES with (does not stack on) the CROWN-oracle intersection — pick one per category by the probe outcome.

Motivation (measured)

Star per-neuron bounds are either an LP (~12 ms per cold linprog call; measured 12,170 LPs/instance on acasxu exact-star, 945-1,133 on MNIST-scale FC approx-star; LP = 35% of FC reach time warm, 57% cold) or the C,d-blind estimate (Star.m:1085-1104). There is no middle tier that sees C's rows without an LP. Weak Lagrangian duality provides one: for any Λ ≥ 0, with W = G − ΛᵀC (G = the star's V rows for the queried neurons),
ub_i(λ) = c_i + λᵀd + Σ_j max(w_ij·plb_j, w_ij·pub_j)
is a valid upper bound (symmetrically for lb), for ANY λ — λ=0 reproduces estimateRanges exactly (Star.m:1098-1104 is literally the λ=0 formula). Subgradient is d − C·α*; the whole computation batches over all queried neurons as two matmuls per iteration; a few ascent steps with elementwise keep-best (the pattern already proven sound in gpu_bab_crown_alpha_dag.m:96-107) converge toward the LP optimum. On the exact path, C's rows ARE the ReLU split constraints, so λ is precisely a beta-CROWN split dual — novel in the star setting and publishable. Unlike the per-net CROWN oracle, dualBounds sees the ACTUAL accumulated constraints of each star, including relaxation variables.

Current behavior

• Serial LP loops: Star.getMins :823-846, Star.getMaxs :937-954 (one lpsolver call per neuron; the parfor branch at :840/:954 is dead — ReluLayer hardcodes [] for the option arg at code/nnv/engine/nn/layers/ReluLayer.m:96/:113/:148, and NN.validate_reach_options pins single-core for non-exact methods at NN.m:1228-1231).
• Estimate: Star.m:1085-1104.

Proposed change

[lb, ub] = Star.dualBounds(map, nIter): batched dual ascent returning valid bounds for the mapped rows. Deploy as (a) a pre-LP tier in getMins/getMaxs (skip LPs the dual bound already decides one-sided) and (b) the estimate upgrade inside the relax variants. Free by-products: dual values as split scores for the FC BaB and as falsifier seeds.

Soundness notes (0-wrong rule) — two specific hazards, both mandatory to fence

1. Wiring defect (false-UNSAT): a dual-proven one-sided neuron must be RE-CLASSIFIED (resetRow for ub ≤ 0; identity/exclusion for lb ≥ 0) and must NEVER be forwarded into multipleStepReachStarApprox_at_one with ub ≤ 0: the triangle slope a = ub./(ub − lb) (PosLin.m:729) becomes ≤ 0, making {y ≤ a(x−lb)} ∧ {y ≥ 0} infeasible → a (near-)empty output star → false UNSAT via verify_specification.m:49-50; the appended predicate box also inverts ([0, ub] with ub < 0, PosLin.m:737-738). A unit oracle must force exactly this case and assert correct classification.
2. FP accumulation: the bound value is trusted directly, so cap ‖Λ‖ or apply one outward-rounding epsilon on the λᵀd + Σ_j h_j accumulation (FP64 throughout).
   Weak duality guarantees validity for ANY Λ ≥ 0 — optimizer quality affects tightness only; the hazards are wiring and precision, not the math.

Acceptance gate & realism

Hard acceptance on cora: instances DECIDED within the 30 s official budget (matmul realism: ~0.3-1 s per layer per rung by layer 7 on cora-mnist-size stars — consider deploying on the last/tightest rung only). If the ceiling probe shows full-LP does not decide a category, do not build for it.

Validation plan

• Randomized oracle: on 1e5 random stars, assert dual bound is never tighter than the LP optimum (dual_ub ≥ lp_ub − tol, symmetrically for lb) and equals estimateRanges at λ=0.
• The forced ub≤0 misclassification unit test (hazard 1).
• Containment suite with dualBounds active; dev-slice verdict diff, new-unsats-only.

References

• code/nnv/engine/set/Star.m:1085-1104, :823-846, :937-954; code/nnv/engine/nn/layers/ReluLayer.m:96,113,148; code/nnv/engine/nn/NN.m:1228-1231
• code/nnv/engine/nn/funcs/PosLin.m:685-742, :729, :737-738
• Keep-best pattern: code/nnv/engine/nn/gpu_bab/gpu_bab_crown_alpha_dag.m:96-107
• False-unsat sink: code/nnv/engine/utils/verify_specification.m:49-50

---

Part of the star-set methods improvement roadmap (2026-07-01); effort estimate: L.

[ttj]

Blocked by #454 (the relaxFactor=0 ceiling probe). Alternative (not stacked) approach: #455; pick one per category based on the probe outcome. Free by-products once built: LP shadow prices as BaB split scores (#450's rung) and falsifier seeds.