Research map / Adversarial robustness and security / Certified and empirical robustness
Relational DNN Verification With Cross Executional Bound Refinement
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes RACoon, a relational DNN verifier that jointly refines parametric ReLU bounds across multiple executions via a differentiable closed-form dual, improving k-UAP accuracy and worst-case hamming distance bounds over the I/O formulation baseline.
Problem
Verifying relational properties over multiple executions of the same DNN (e.g., universal adversarial perturbation robustness and worst-case hamming distance), where existing verifiers treat executions independently or only track input-layer dependencies and thus lose precision.
Approach
Jointly optimize parametric linear bounds of ReLU across multiple executions using a closed-form differentiable Lagrangian dual G(lambda) that couples executions' linear approximations, then formulate a MILP with only O(k x n_l) integer variables over the output specification.
Key results
- RACoon gains up to +16.5% UAP accuracy on MNIST and up to +22% on CIFAR10 over the I/O formulation baseline.
- RACoon reduces worst-case hamming distance by up to 8 (up to 40% for binary strings of size 20) relative to I/O formulation.
- For ConvBig networks RACoon takes under 8 s on MNIST (20 executions) and under 12 s on CIFAR10 (10 executions).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use RACoon cross-execution refinement instead of I/O Formulation | Relational verification of MNIST and CIFAR10 k-UAP · MNIST and CIFAR10 k-UAP | Avg. UAP accuracy (%): up to +16.5%; up to +22% | Helped |
| Use RACoon cross-execution refinement instead of I/O Formulation | Relational verification of MNIST worst-case Hamming distance · MNIST worst-case Hamming distance | Avg. Hamming distance: up to 8 | Helped |
| Add cross-executional bound refinement rather than individual bound refinement (ablation) | RACoon, 2-UAP verification · MNIST DiffAI, 2-UAP | LP bound t: -0.2 -> -0.05 | Helped |
| Increase hyperparameters k0 and k1 (ablation) | RACoon · Relational verification | precision | Helped |
| Increase hyperparameters k0 and k1 (ablation) | RACoon · Relational verification | runtime | Hurt |
Surprising findings
- Individual bound refinement with alpha-CROWN fails to prove absence of common perturbation in all four tested cases where cross-execution refinement succeeds.
- Standard-trained networks show the I/O formulation outperforming individual refinement, while cross-execution refinement remains more precise.
Limitations
- Incomplete verifier; may fail to prove properties that hold.
- Does not scale to larger datasets such as ImageNet.
- Slower than the I/O formulation baseline.
Experimental setup
Datasets: MNIST CIFAR10
Benchmarks: MNIST CIFAR10
Metrics: worst-case UAP accuracy worst-case hamming distance runtime (sec)
Baselines: I/O formulation auto_LiRPA non-relational verifier alpha-CROWN individual refinement
Builds on: alpha-CROWN auto_LiRPA I/O formulation relational verifier MILP-based verification
Closest papers by meaning
- Relational Verification Leaps Forward with RABBit (NeurIPS 2024 · similarity 0.92)
- RelGNN: Composite Message Passing for Relational Deep Learning (ICML 2025 · similarity 0.84)
- Provable Editing of Deep Neural Networks using Parametric Linear Relaxation (NeurIPS 2024 · similarity 0.83)
- VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees (ICML 2024 · similarity 0.83)
- Certified but Private: Scalable Zero-Knowledge Proofs for the Formal Verification of Neural Networks (NeurIPS 2026 · similarity 0.83)
- Interpreting Robustness Proofs of Deep Neural Networks (ICLR 2024 · similarity 0.83)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.