star: differential star reachability for network-equivalence queries (isomorphic_acasxu)

[ttj]

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

Motivation (measured)

isomorphic_acasxu (VNN-COMP 2026 extended category) is an epsilon-equivalence benchmark: prove max|f(x) − g(x)| < 0.05 for pairs of nearly-identical ACAS-style networks. NNV currently abstains — 0%, and the category is worth +40-50 instances = +80-100 breadth points, the single biggest prize on the board. The measured facts that define the problem:

• A 12-instance sampling probe found true max|f − g| ∈ [0.0024, 0.035] — ALL below the 0.05 tolerance, so every instance is a true UNSAT; there is no SAT to falsify. Only a sound proof method scores here.
• A block-diagonal product-network builder (f and g stacked, shared input, output = concatenation) exists and is numerically exact (1.3e-08 consistency vs separate execution).
• Approx-star on the product net bounds the difference at ±750 vs the true ~0.035 — ~20,000x too loose, because f's and g's ReLUs are relaxed INDEPENDENTLY and the difference of two independent relaxations destroys exactly the correlation the query is about.
• Exact-star on the product net explodes at the FIRST ReLU layer (~100 unstable neurons; path count ≈ |stars_f| × |stars_g|).

Proposed research (ReluDiff/NeuralDiff lineage)

Propagate the DIFFERENCE jointly through the paired networks: a relational star carrying (activation of f, activation of g, and their difference in one basis over a shared predicate space). Per layer: where f's and g's corresponding ReLUs provably agree in sign (the overwhelmingly common case for small weight perturbations — the weights differ by tiny deltas), the difference propagates through a COMMON linearization with a bounded second-order term; split only on the rare sign-disagreement neurons. This keeps the split tree proportional to disagreement count instead of |stars_f| × |stars_g|, and keeps the difference bound tied to the weight-delta magnitude instead of the absolute activation magnitude.

Milestones: (1) prototype the relational transformer on one acas pair, report the achieved |f − g| bound vs the ±750 baseline and the true ~0.035; (2) sign-agreement statistics per layer across the 50 pairs (validates the split-budget assumption); (3) scale to the full category within the official budget; (4) write-up (publishable — no MATLAB tool has a differential star domain).

Soundness notes (0-wrong rule)

• The verdict direction is favorable: an over-approximation of |f − g| that is too loose yields false UNKNOWN only, never false UNSAT — soundness reduces to the transformer being a genuine over-approximation (fence with dense sample-trace containment: every sampled (f(x), g(x), f(x)−g(x)) triple inside the relational set at every layer).
• Known −150 trap to keep fenced: instance PAIRING. A mis-paired query (f stacked against itself instead of against g) makes every instance trivially "equivalent" → wrong UNSAT at category scale. The existing two-network tuple normalization and its reject-to-unknown guard must be preserved; never bypass the parser guard to "unlock" the category.
• Fail-loud on NaN/Inf bounds before any tolerance comparison.

Validation plan

Per-instance: dense-sampling lower bound on max|f−g| must not exceed the certified upper bound; category dev run emits unsat only when the certified bound < 0.05 with margin; cross-check 3 instances against an independent MILP/LP encoding of the difference network on a reduced input box.

References

• Failure-mode baselines to beat: approx-star product-net diff bound ±750 (vs true ~0.035); exact-star first-layer explosion (~100 unstable, |stars_f|×|stars_g| paths).
• Star machinery: code/nnv/engine/set/Star.m (basis/predicate representation), code/nnv/engine/nn/funcs/PosLin.m (ReLU transformers to be generalized relationally).
• Literature: ReluDiff (ICSE 2020), NeuralDiff — differential verification of nearly-identical networks.

---

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