Advanced Neural Networks Verification for Safe and Explainable Intelligent Systems

Deep neural networks (DNNs) have revolutionized artificial intelligence (AI), enabling breakthroughs across domains ranging from medical robotics to sustainable energy management. Yet, their fragility to adversarial perturbations and their opacity as “black boxes” pose significant risks when deployed in safety-critical contexts. In this thesis, we address these challenges by advancing the field of neural network verification, with a particular focus on enhancing the safety and explainability of intelligent systems. A first set of contributions develops novel verification techniques that address the limitations of existing approaches. Through abstract interpretation and probabilistic reasoning, this work introduces scalable methods that not only provide sound guarantees but also extend verification to richer, semantically grounded safety properties. In particular, the introduction of the #DNN-Verification and AllDNN-Verification problems establishes new theoretical foundations that enable quantifying and localizing unsafe regions within the input space, thereby linking verification with interpretability. Building upon these theoretical advances, this work demonstrates how verification can be effectively integrated into deep reinforcement learning (DRL) scenarios. From post-training verification for model selection to verification-informed training, we show how safety assurances can guide policy optimization in safety-critical applications such as robotic navigation and medical procedures. Crucially, these methods further allow the automatic collection of task-level safety properties, reducing reliance on brittle, hand-designed specifications. Finally, this thesis extends the role of verification toward explainability by providing the first rigorous complexity analysis of generating robust Counterfactual Explanations (CEs). Leveraging probabilistic verification methods, we propose new algorithms that produce counterfactuals with provable probabilistic robustness guarantees, ensuring explanations that remain valid after fine-tuning the model. Together, these contributions establish verification as a unifying tool at the intersection of safety and explainability of intelligent systems. By bridging theory with practical deployment in the real world, this thesis advances the vision of trustworthy, transparent, and reliable AI systems.