vnncomp-runner: adaptive_cruise 2-D cell-grid certification via batched FP64 bounds and the existing python AST interval evaluator

[ttj]

All paths relative to the nnv repo root; verified on master @ 376568b44. Both the runner and the python evaluator live in the nnv repo (code/nnv/examples/Submission/VNN_COMP2026/).

Motivation (measured)

adaptive_cruise (extended category) scored 38% (19/50) in the S12 sweep: SATs from the sampling falsifier plus 18 vacuous UNSATs where the nonlinear input constraint is provably infeasible. The remaining ~15-31 instances are unknowns worth +30-62 breadth points — the largest single-category sound-uplift opportunity on the board. The network is tiny (2 inputs → 4×64 ReLU → 1 output), the input space is 2-D, and the official budget is 100 s: a cell-grid certification is cheap and student-suited.

Current behavior

code/nnv/examples/Submission/VNN_COMP2026/run_vnncomp_instance.m:128-156: verify_adaptive_cruise_falsify(onnx, vnnlib) drives adaptive_cruise_falsify.py (same directory). Outcomes today: SAT (ORT-confirmed counterexample), UNSAT only for the empty-input cases (interval arithmetic over the authoritative parsed vnnlib AST proves the nonlinear input constraint infeasible over the box — "emits 11 ONLY when proven", :143-147), otherwise unknown and the nonlinear-vnnlib gate keeps reach off. No mechanism exists to certify a NON-empty instance UNSAT.

Proposed change

1. Grid/bisect the 2-D input box into cells (adaptive refinement on unrefuted cells).
2. For each cell, compute a sound FP64 output interval for the network output: one batched gpu_bab_crown_tight call with C = ±I over all cells at once (code/nnv/engine/nn/gpu_bab/gpu_bab_crown_tight.m:1 already accepts a batch of boxes), or per-cell approx-star on the trivial net.
3. Extend adaptive_cruise_falsify.py to accept ALL (X-cell, Y-interval) pairs in ONE process invocation and evaluate the nonlinear spec over each cell with outward-rounded interval arithmetic on the parsed AST (per-cell process spawns would blow the 100 s budget).
4. If every cell of the partition is refuted (spec interval-disjoint) → emit unsat; otherwise the unrefuted cells focus the existing falsifier (region-restricted sampling).

Soundness notes (0-wrong rule)

• UNSAT is emitted only when (a) the cells form an exact partition of the input box (closed-split bisection, same argument as gpu_bab_halfspace_input_bab.m:13-19), (b) each cell's network bound comes from an FP64 certified path (never raw FP32; no directed rounding on gpuArray), and (c) the AST evaluation is outward-rounded interval arithmetic over the authoritative parser (the same evaluator that already backs the vacuous-unsat path).
• Keep the standing fence: the 18 empty-input unsats were reported to the benchmark proposer as a likely benchmark bug — retain abstain-if-oracle-disagrees behavior for that slice, and keep every SAT ORT-confirmed as today.
• Fail-loud: any NaN/Inf in a cell bound must abort to unknown, never flow into a "refuted" comparison.

Validation plan

• Cross-check per-cell network intervals against dense sampling (1e5 points per cell on a few cells).
• Property-level test: on a known-SAT instance, assert the grid never refutes the cell containing the confirmed counterexample.
• Full-category dev run at the official 100 s budget: 0 flips of existing verdicts; count new unsats; validate 2-3 by independent fine-grid interval evaluation.

References

• code/nnv/examples/Submission/VNN_COMP2026/run_vnncomp_instance.m:128-156
• code/nnv/examples/Submission/VNN_COMP2026/adaptive_cruise_falsify.py
• code/nnv/engine/nn/gpu_bab/gpu_bab_crown_tight.m:1

---

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