# On Improving Deep Active Learning with Formal Verification

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 27 of its 48 references that are in the map.
- First posted on arXiv 16 Dec 2025.

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

- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [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)
- [Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms](https://mlsanity.com/paper/1708.07747/) (2017)
- [DeepFool: a simple and accurate method to fool deep neural networks](https://mlsanity.com/paper/1511.04599/) (2015)
- [Revisiting Unreasonable Effectiveness of Data in Deep Learning Era](https://mlsanity.com/paper/1707.02968/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Deep Batch Active Learning by Diverse, Uncertain Gradient Lower Bounds](https://mlsanity.com/paper/1906.03671/) (2019)
- [Deep Learning Scaling is Predictable, Empirically](https://mlsanity.com/paper/1712.00409/) (2017)
- [A Survey of Deep Active Learning](https://mlsanity.com/paper/2009.00236/) (2020)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Adversarial Active Learning for Deep Networks: a Margin Based Approach](https://mlsanity.com/paper/1802.09841/) (2018)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [Pruning and Slicing Neural Networks using Formal Verification](https://mlsanity.com/paper/2105.13649/) (2021)
- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [Verification-Guided Shielding for Deep Reinforcement Learning](https://mlsanity.com/paper/2406.06507/) (2024)
- [Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations](https://mlsanity.com/paper/2506.08505/) (2025)
- [DNN Verification, Reachability, and the Exponential Function Problem](https://mlsanity.com/paper/2305.06064/) (2023)
- [Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing](https://mlsanity.com/paper/2402.00035/) (2024)
- [A Certified Proof Checker for Deep Neural Network Verification in Imandra](https://mlsanity.com/paper/2405.10611/) (2024)
- [Abstraction-Based Proof Production in Formal Verification of Neural Networks](https://mlsanity.com/paper/2506.09455/) (2025)
- [Safe and Reliable Training of Learning-Based Aerospace Controllers](https://mlsanity.com/paper/2407.07088/) (2024)
- [Proof Minimization in Neural Network Verification](https://mlsanity.com/paper/2511.08198/) (2025)
- [Verifying the Generalization of Deep Learning to Out-of-Distribution Domains](https://mlsanity.com/paper/2406.02024/) (2024)

## Abstract (arXiv)

Deep Active Learning (DAL) aims to reduce labeling costs in neural-network training by prioritizing the most informative unlabeled samples for annotation. Beyond selecting which samples to label, several DAL approaches further enhance data efficiency by augmenting the training set with synthetic inputs that do not require additional manual labeling. In this work, we investigate how augmenting the training data with adversarial inputs that violate robustness constraints can improve DAL performance. We show that adversarial examples generated via formal verification contribute substantially more than those produced by standard, gradient-based attacks. We apply this extension to multiple modern DAL techniques, as well as to a new technique that we propose, and show that it yields significant improvements in model generalization across standard benchmarks.