On Improving Deep Active Learning with Formal Verification

2025/12/16 by Jonathan Spiegelman, Spiegelman, Jonathan, Guy Amir +3
Computer Science · #Adversarial Robustness in Machine Learning #Machine Learning and Algorithms #Machine Learning and Data Classification

paper · pdf · doi:10.48550/arxiv.2512.14170

Abstract

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.

Citations

• Proof Minimization in Neural Network Verification
• Abstraction-Based Proof Production in Formal Verification of Neural Networks
• Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
• Safe and Reliable Training of Learning-Based Aerospace Controllers
• Verification-Guided Shielding for Deep Reinforcement Learning
• Verifying the Generalization of Deep Learning to Out-of-Distribution Domains
• Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
• A Certified Proof Checker for Deep Neural Network Verification in Imandra
• Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
• Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing
• Formally Explaining Neural Networks within Reactive Systems
• DNN Verification, Reachability, and the Exponential Function Problem
• Verifying Learning-Based Robotic Navigation Systems
• Pruning and Slicing Neural Networks using Formal Verification
• A Survey of Deep Active Learning
• Adversarial Active Learning for Deep Networks: a Margin Based Approach
• Deep Learning Scaling is Predictable, Empirically
• Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms
• Revisiting Unreasonable Effectiveness of Data in Deep Learning Era
• Towards Deep Learning Models Resistant to Adversarial Attacks
• Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
• Safety Verification of Deep Neural Networks
• DeepFool: a simple and accurate method to fool deep neural networks
• Explaining and Harnessing Adversarial Examples
• Intriguing properties of neural networks
• ImageNet classification with deep convolutional neural networks
• BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding

Related

• Soften to Defend: Towards Adversarial Robustness via Self-Guided Label Refinement
• VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees
• Active Learning Under Malicious Mislabeling and Poisoning Attacks
• Adversarial Representation Active Learning
• Exploring Adversarial Examples for Efficient Active Learning in Machine Learning Classifiers