gpu-bab: batch the input-bisection BaB frontier (gpu_bab_halfspace_input_bab) via gpu_bab_crown_spec_dag with per-page input coefficients

[ttj]

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

Motivation (measured)

gpu_bab_halfspace_input_bab.m is the engine that certified the 45 acasxu prop_1 instances in 0.3-14 s each, but it is serial: one full bound computation per popped sub-box. Low-input-dimension categories with unused budget are exactly where it pays to batch:

• cersyve (4-6-D inputs, 100 s budget, 25.0%): its 2 already-proven unsats landed at 122-140 s — a pure latency miss of 22-40 s; each instance is worth ~8.3 breadth points. A >2x throughput lever closes this directly.
• tllverifybench (62.5%) already routes this engine as a backstop.
• adaptive_cruise (2-D) and cgan2026 (5-D, 900-1800 s budgets) are the target consumers of a batched frontier (tracked separately).
  Combined sizing across the low-dim categories: +60-130 breadth points (shares claimed by the per-category issues).

Current behavior

code/nnv/engine/nn/gpu_bab/gpu_bab_halfspace_input_bab.m:

• LIFO stack, ONE gpu_bab_crown_tight call per popped node (:56), widest-dim bisection (:70-78), and a joint disjunct test via gpu_bab_clip on the returned input-space coefficients Ain/din (:63).
• Soundness header (:13-19): children PARTITION the parent (closed split), robust returned only when the stack empties with every popped sub-box certified; certified path is FP64 (opts.precision defaults to 'double').
• Header (:21-23): for pure-ReLU nets input bisection does NOT converge (the looseness is in the ReLU relaxation) — callers should gate on presence of a product/bilinear op, or pair with per-node alpha iterations.

Proposed change

1. Batch the frontier: pop k nodes per iteration, bound all k sub-boxes in one call. The batched bounder must be gpu_bab_crown_spec_dag (code/nnv/engine/nn/gpu_bab/gpu_bab_crown_spec_dag.m) — NOT gpu_bab_crown_spec, which supports only affine/relu ops with forward-IBP intermediates (it errors on e.g. add ops, which cersyve nets contain, and is strictly looser).
2. Extend gpu_bab_crown_spec_dag to return per-page input coefficients (Ain/din per box page) so the joint gpu_bab_clip emptiness test at :63 survives batching — without this the batched path loses the joint-disjunct certification and only single-row separation remains.
3. Optional split-ordering heuristic (zero soundness exposure): smear score |df/dx_j| * width_j from the root CROWN A-row instead of widest-dim. Caveat: for bilinear nets, widest-dim is already matched to the O(width^2) McCormick gap — keep widest-dim there.

Soundness notes (0-wrong rule)

• The partition-coverage proof (:13-19) is evaluation-order-independent, so batching k pops preserves it verbatim; assert in tests that every child pair partitions its parent.
• The certified path must remain FP64; never emit a verdict from raw FP32 GPU bounds (no directed rounding exists on gpuArray).
• gpu_bab_crown_spec_dag caveat (header :1-15): any call passing the cSel (binding-spec) argument returns SELECTED-row margins that must be used for split scoring only and NEVER for certification — certification must use full-C margins from a cSel-absent call. The batched frontier must preserve this discipline.

Validation plan

• Unit: batched per-page Ain/din and margins equal the serial gpu_bab_crown_tight outputs page-by-page (tolerance 0) on small nets.
• A/B on cersyve + tll instances: identical verdicts, measured wall-time reduction; the 2 cersyve unsats must land under 100 s.
• Partition invariant test across randomized split sequences.

References

• code/nnv/engine/nn/gpu_bab/gpu_bab_halfspace_input_bab.m:13-23, :56, :63, :70-78
• code/nnv/engine/nn/gpu_bab/gpu_bab_crown_spec_dag.m:1-15 (cSel discipline)
• code/nnv/engine/nn/gpu_bab/gpu_bab_crown_tight.m:1 (signature returning margins + Ain/din)

---

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