# SpecRepair: Counter-Example Guided Safety Repair of Deep Neural Networks

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 37 references that are in the map.
- First posted on arXiv 3 Jun 2021.

## Builds on (most cited first, 14 of 14)

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [HopSkipJumpAttack: A Query-Efficient Decision-Based Attack](https://mlsanity.com/paper/1904.02144/) (2019)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Parsimonious Black-Box Adversarial Attacks via Efficient Combinatorial Optimization](https://mlsanity.com/paper/1905.06635/) (2019)
- [Provable Repair of Deep Neural Networks](https://mlsanity.com/paper/2104.04413/) (2021)
- [Outside the Box: Abstraction-Based Monitoring of Neural Networks](https://mlsanity.com/paper/1911.09032/) (2019)
- [NNrepair: Constraint-based Repair of Neural Network Classifiers](https://mlsanity.com/paper/2103.12535/) (2021)
- [Into the Unknown: Active Monitoring of Neural Networks](https://mlsanity.com/paper/2009.06429/) (2020)
- [Towards Repairing Neural Networks Correctly](https://mlsanity.com/paper/2012.01872/) (2020)
- [Provably-Robust Runtime Monitoring of Neuron Activation Patterns](https://mlsanity.com/paper/2011.11959/) (2020)

## Built on by (most cited first, 6 of 6)

- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound](https://mlsanity.com/paper/2405.17556/) (2024)
- [A Robust Optimisation Perspective on Counterexample-Guided Repair of Neural Networks](https://mlsanity.com/paper/2301.11342/) (2023)
- [Counterexample-Guided Repair of Reinforcement Learning Systems Using Safety Critics](https://mlsanity.com/paper/2405.15430/) (2024)
- [Bad Genius: Counterfactual-Guided Harness Evolution Beyond Task-Specific Shortcuts](https://mlsanity.com/paper/2609.18366/) (2026)
- [Verifying Global Neural Network Specifications using Hyperproperties](https://mlsanity.com/paper/2306.12495/) (2023)

## Abstract (arXiv)

Deep neural networks (DNNs) are increasingly applied in safety-critical domains, such as self-driving cars, unmanned aircraft, and medical diagnosis. It is of fundamental importance to certify the safety of these DNNs, i.e. that they comply with a formal safety specification. While safety certification tools exactly answer this question, they are of no help in debugging unsafe DNNs, requiring the developer to iteratively verify and modify the DNN until safety is eventually achieved. Hence, a repair technique needs to be developed that can produce a safe DNN automatically. To address this need, we present SpecRepair, a tool that efficiently eliminates counter-examples from a DNN and produces a provably safe DNN without harming its classification accuracy. SpecRepair combines specification-based counter-example search and resumes training of the DNN, penalizing counter-examples and certifying the resulting DNN. We evaluate SpecRepair's effectiveness on the ACAS Xu benchmark, a DNN-based controller for unmanned aircraft, and two image classification benchmarks. The results show that SpecRepair is more successful in producing safe DNNs than comparable methods, has a shorter runtime, and produces safe DNNs while preserving their classification accuracy.