star: containment-based soundness regression suite for approx-star and all relax-star variants

[ttj]

All paths relative to the nnv repo root; verified on master @ 376568b44.

Motivation

The relax-star ladder is a deciding engine at 7+ VNN-COMP 2026 categories (cora 57.2%, dist_shift 76.4%, tllverifybench 62.5%, relusplitter 50.8%, cersyve 25.0%; routing via relax_ladder, code/nnv/examples/Submission/VNN_COMP2026/run_vnncomp_instance.m:1366-1384). Yet the existing soundness tests assert only non-emptiness of the result set — e.g. tests/soundness/test_soundness_relax_star.m:20-21:

output = L.reach(input_star, 'relax-star-range');
assert(~isempty(output), 'relax-star-range should produce output');

A relaxation that returned a wrong (too-small) set would pass every current test. Two verified latent bugs in this family (the TanSig relax stub R = I at TanSig.m:1913-1915, and the LeakyReLU wrong-index reset at LeakyReLU.m:642) would both have been caught by containment assertions. This suite is the regression net for all planned tightening work (CROWN-bound intersection, dualBounds, midpoint tangents, Taylor transformers).

Current behavior

• Relax family implementations: code/nnv/engine/nn/funcs/PosLin.m:861-1652 (range/area/bound/random/static heuristics; shared skeleton: estimateRanges → straddler set → LP budget n1 = round((1-relaxFactor)*|map2|) at PosLin.m:929 → one-shot triangle multipleStepReachStarApprox_at_one at PosLin.m:685-742).
• Tests: tests/soundness/test_soundness_relax_star.m — non-emptiness only.

Proposed change

Add tests/soundness/test_containment_star.m (or extend the existing file) that, for random seeded FC nets (relu, leaky-relu, tanh, sigmoid; 2-5 layers) and one small conv net, and for every relax heuristic × relaxFactor ∈ {0, 0.25, 0.5, 1}:

1. Sample containment: sample N ≥ 1e4 inputs from the input star, execute the network exactly, and assert every output point is contained in the computed output star (point-in-star = one LP feasibility on {Cα ≤ d, plb ≤ α ≤ pub, V·[1;α] = y}).
2. Nesting: assert relax(f)-set ⊇ approx-star set on box bounds (getRanges of the relax result must enclose the approx result within tolerance), per heuristic.
3. Monotonicity spot-checks across relaxFactor (higher relaxFactor never tighter than lower on output box bounds).
4. Regression cases from the TanSig-stub and LeakyReLU-index bug fixes (a tanh net whose input box lies outside [-1,1]; a leaky-relu net where the LP/sort order disagree).

Soundness notes (0-wrong rule)

Test-only change; no verdict paths touched. Its purpose is to fence the −150 rule for all future star work: any transformer change that shrinks a set below the true reachable set fails CI instead of reaching competition.

Validation plan

Run on current master: all containment tests must pass EXCEPT the two known-bug regression cases (which are expected to fail until the corresponding bug fixes land). Wire into the standard test entry point.

References

• tests/soundness/test_soundness_relax_star.m:20-21 (current non-emptiness-only asserts)
• code/nnv/engine/nn/funcs/PosLin.m:861-1652, :685-742, :929
• Known-bug anchors: code/nnv/engine/nn/funcs/TanSig.m:1913-1915, code/nnv/engine/nn/funcs/LeakyReLU.m:642

---

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