# Improving Neural Network Verification through Spurious Region Guided Refinement

arXiv: https://arxiv.org/abs/2010.07722 · HTML: https://mlsanity.com/paper/2010.07722/

## Key facts

- Cited by 31 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Oct 2020.

## Built on by (most cited first, 30 of 31)

- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Scalable Verification of GNN-based Job Schedulers](https://mlsanity.com/paper/2203.03153/) (2022)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [Provable Preimage Under-Approximation for Neural Networks (Full Version)](https://mlsanity.com/paper/2305.03686/) (2023)
- [Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning](https://mlsanity.com/paper/2101.10102/) (2021)
- [QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks](https://mlsanity.com/paper/2212.11138/) (2022)
- [Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks](https://mlsanity.com/paper/2207.00759/) (2022)
- [QEBVerif: Quantization Error Bound Verification of Neural Networks](https://mlsanity.com/paper/2212.02781/) (2022)
- [Tighter Abstract Queries in Neural Network Verification](https://mlsanity.com/paper/2210.12871/) (2022)
- [TrajPAC: Towards Robustness Verification of Pedestrian Trajectory Prediction Models](https://mlsanity.com/paper/2308.05985/) (2023)
- [PREMAP: A Unifying PREiMage APproximation Framework for Neural Networks](https://mlsanity.com/paper/2408.09262/) (2024)
- [When to Trust AI: Advances and Challenges for Certification of Neural Networks](https://mlsanity.com/paper/2309.11196/) (2023)
- [DeepCDCL: An CDCL-based Neural Network Verification Framework](https://mlsanity.com/paper/2403.07956/) (2024)
- [Out of the Shadows: Exploring a Latent Space for Neural Network Verification](https://mlsanity.com/paper/2505.17854/) (2025)
- [Specifying and Testing k-Safety Properties for Machine-Learning Models](https://mlsanity.com/paper/2206.06054/) (2022)
- [Safety Verification for Neural Networks Based on Set-boundary Analysis](https://mlsanity.com/paper/2210.04175/) (2022)
- [Repairing Deep Neural Networks Based on Behavior Imitation](https://mlsanity.com/paper/2305.03365/) (2023)
- [FairQuant: Certifying and Quantifying Fairness of Deep Neural Networks](https://mlsanity.com/paper/2409.03220/) (2024)
- [Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks](https://mlsanity.com/paper/2302.06455/) (2023)
- [Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification](https://mlsanity.com/paper/2505.00963/) (2025)
- [Efficient Preimage Approximation for Neural Network Certification](https://mlsanity.com/paper/2505.22798/) (2025)
- [Verifying Safety of Neural Networks from Topological Perspectives](https://mlsanity.com/paper/2306.15403/) (2023)
- [Expediting Neural Network Verification via Network Reduction](https://mlsanity.com/paper/2308.03330/) (2023)
- [Efficiently Finding Adversarial Examples with DNN Preprocessing](https://mlsanity.com/paper/2211.08706/) (2022)
- [UR4NNV: Neural Network Verification, Under-approximation Reachability Works!](https://mlsanity.com/paper/2401.12550/) (2024)
- [Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees](https://mlsanity.com/paper/2507.17453/) (2025)
- [Provable Repair of Deep Neural Network Defects by Preimage Synthesis and Property Refinement](https://mlsanity.com/paper/2511.07741/) (2025)
- [Quantitative Verification of Fairness in Tree Ensembles](https://mlsanity.com/paper/2512.16386/) (2025)
- [Provable Fairness Repair for Deep Neural Networks](https://mlsanity.com/paper/2605.19549/) (2026)
- [Neural Network Verification using Partial Multi-Neuron Relaxation](https://mlsanity.com/paper/2605.30155/) (2026)

## Abstract (arXiv)

We propose a spurious region guided refinement approach for robustness verification of deep neural networks. Our method starts with applying the DeepPoly abstract domain to analyze the network. If the robustness property cannot be verified, the result is inconclusive. Due to the over-approximation, the computed region in the abstraction may be spurious in the sense that it does not contain any true counterexample. Our goal is to identify such spurious regions and use them to guide the abstraction refinement. The core idea is to make use of the obtained constraints of the abstraction to infer new bounds for the neurons. This is achieved by linear programming techniques. With the new bounds, we iteratively apply DeepPoly, aiming to eliminate spurious regions. We have implemented our approach in a prototypical tool DeepSRGR. Experimental results show that a large amount of regions can be identified as spurious, and as a result, the precision of DeepPoly can be significantly improved. As a side contribution, we show that our approach can be applied to verify quantitative robustness properties.