Publications
Peer-reviewed or pre-print publications. Check my Google scholar for the complete list.
(* indicates equal contribution)
2026
- PhD ThesisAdvanced Neural Networks Verification for Safe and Explainable Intelligent SystemsLuca MarzariDepartment of Computer Science, University of Verona, 2026
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.
- AAAIOn the Probabilistic Learnability of Compact Neural Network Preimage BoundsLuca Marzari, Manuele Bicego, Ferdinando Cicalese, and Alessandro FarinelliProceedings of the AAAI Conference on Artificial Intelligence (AAAI), 2026
Although recent provable methods have been developed to compute preimage bounds for neural networks, their scalability is fundamentally limited by the #P-hardness of the problem. In this work, we adopt a novel probabilistic perspective, aiming to deliver solutions with high-confidence guarantees and bounded error. To this end, we investigate the potential of bootstrap-based and randomized approaches that are capable of capturing complex patterns in high-dimensional spaces, including input regions where a given output property holds. In detail, we introduce *R*andom *F*orest *Pro*perty *Ve*rifier (RF-ProVe), a method that exploits an ensemble of randomized decision trees to generate candidate input regions satisfying a desired output property and refines them through active resampling. Our theoretical derivations offer formal statistical guarantees on region purity and global coverage, providing a practical, scalable solution for computing compact preimage approximations in cases where exact solvers fail to scale.
2025
- AIJProbabilistically Robust Counterfactual Explanations under Model ChangesLuca Marzari, Francesco Leofante, Ferdinando Cicalese, and Alessandro FarinelliArtificial Intelligence Journal (AIJ), 2025
We study the problem of generating robust counterfactual explanations for deep learning models subject to model changes. We focus on plausible model changes altering model parameters and propose a novel framework to reason about the robustness property in this setting. To motivate our solution, we begin by showing for the first time that computing the robustness of counterfactuals with respect to model changes is NP-hard. As this (practically) rules out the existence of scalable algorithms for exactly computing robustness, we propose a novel probabilistic approach which is able to provide tight estimates of robustness with strong guarantees while preserving scalability. Remarkably, and differently from existing solutions targeting plausible model changes, our approach does not impose requirements on the network to be analysed, thus enabling robustness analysis on a wider range of architectures, including state-of-the-art tabular transformers. A thorough experimental analysis on four binary classification datasets reveals that our method improves the state of the art in generating robust explanations, outperforming existing methods.
- ACM TISTVerifying Online Safety Properties for Safe Deep Reinforcement LearningLuca Marzari, Ferdinando Cicalese, Alessandro Farinelli, Christopher Amato, and Enrico MarchesiniACM Transactions on Intelligent Systems and Technology (TIST), 2025
Ensuring safety in reinforcement learning (RL) is critical for deploying agents in real-world applications. During training, current safe RL approaches often rely on indicator cost functions that provide sparse feedback, resulting in two key limitations: (i) poor sample efficiency due to the lack of safety information in neighboring states, and (ii) dependence on cost-value functions, leading to brittle convergence and suboptimal performance. After training, safety is guaranteed via formal verification methods for deep neural networks (FV), whose computational complexity hinders their application during training. We address the limitations of using cost functions via verification by proposing a safe RL method based on a violation value—the risk associated with policy decisions in a portion of the state space. Our approach verifies safety properties (i.e., state-action pairs) that may lead to unsafe behavior, and quantifies the size of the state space where properties are violated. This violation value is then used to penalize the agent during training to encourage safer policy behavior. Given the NP-hard nature of FV, we propose an efficient, sample-based approximation with probabilistic guarantees to compute the violation value. Extensive experiments on standard benchmarks and real-world robotic navigation tasks show that violation-augmented approaches significantly improve safety by reducing the number of unsafe states encountered while achieving superior performance compared to existing methods.
- ArXivFormal Verification of Variational Quantum CircuitsNicola Assolini*, Luca Marzari*, Isabella Mastroeni, and Alessandra PierroarXiv preprint arXiv:2507.10635, 2025
Variational quantum circuits (VQCs) are a central component of many quantum machine learning algorithms, offering a hybrid quantum-classical framework that, under certain aspects, can be considered similar to classical deep neural networks. A shared aspect is, for instance, their vulnerability to adversarial inputs, small perturbations that can lead to incorrect predictions. While formal verification techniques have been extensively developed for classical models, no comparable framework exists for certifying the robustness of VQCs. Here, we present the first in-depth theoretical and practical study of the formal verification problem for VQCs. Inspired by abstract interpretation methods used in deep learning, we analyze the applicability and limitations of interval-based reachability techniques in the quantum setting. We show that quantum-specific aspects, such as state normalization, introduce inter-variable dependencies that challenge existing approaches. We investigate these issues by introducing a novel semantic framework based on abstract interpretation, where the verification problem for VQCs can be formally defined, and its complexity analyzed. Finally, we demonstrate our approach on standard verification benchmarks.
- JAIRProbabilistically Tightened Linear Relaxation-based Perturbation Analysis for Neural Network VerificationLuca Marzari, Ferdinando Cicalese, and Alessandro FarinelliJournal of Artificial Intelligence Research (JAIR), 2025
We present *P*robabilistically *T*ightened *Li*near *R*elaxation-based *P*erturbation *A*nalysis (PT-LiRPA), a novel framework that combines over-approximation techniques from LiRPA-based approaches with a sampling-based method to compute tight intermediate reachable sets. In detail, we show that with negligible computational overhead, PT-LiRPA exploiting the estimated reachable sets, significantly tightens the lower and upper linear bounds of a neural network’s output, reducing the computational cost of formal verification tools while providing probabilistic guarantees on verification soundness. Extensive experiments on standard formal verification benchmarks, including the International Verification of Neural Networks Competition, show that our PT-LiRPA-based verifier improves robustness certificates by up to 3.31X and 2.26X compared to related work. Importantly, our probabilistic approach results in a valuable solution for challenging competition entries where state-of-the-art formal verification methods fail, allowing us to provide answers with high confidence (i.e., at least 99%).
- ECAIAdvancing Neural Network Verification through Hierarchical Safety Abstract InterpretationLuca Marzari, Isabella Mastroeni, and Alessandro FarinelliProceedings of the 28th European Conference on Artificial Intelligence (ECAI), 2025
Traditional methods for formal verification (FV) of deep neural networks (DNNs) are constrained by a binary encoding of safety properties, where a model is classified as either safe or unsafe (robust or not robust). This binary encoding fails to capture the nuanced safety levels within a model, often resulting in either overly restrictive or too permissive requirements. In this paper, we introduce a novel problem formulation called Abstract DNN-Verification, which verifies a hierarchical structure of unsafe outputs, providing a more granular analysis of the safety aspect for a given DNN. Crucially, by leveraging abstract interpretation and reasoning about output reachable sets, our approach enables assessing multiple safety levels during the FV process, requiring the same (in the worst case) or even potentially less computational effort than the traditional binary verification approach. Specifically, we demonstrate how this formulation allows rank adversarial inputs according to their abstract safety level violation, offering a more detailed evaluation of the model’s safety and robustness. Our contributions include a theoretical exploration of the relationship between our novel abstract safety formulation and existing approaches that employ abstract interpretation for robustness verification, complexity analysis of the novel problem introduced, and an empirical evaluation considering both a complex deep reinforcement learning task (based on Habitat 3.0) and standard DNN-Verification benchmarks.
- RA-LDesigning Control Barrier Function via Probabilistic Enumeration for Safe Reinforcement Learning NavigationLuca Marzari, Francesco Trotti, Enrico Marchesini, and Alessandro FarinelliIEEE Robotics and Automation Letters (RA-L), 2025
Achieving safe autonomous navigation systems is critical for deploying robots in dynamic and uncertain real-world environments. In this paper, we propose a hierarchical control framework leveraging neural network verification techniques to design control barrier functions (CBFs) and policy correction mechanisms that ensure safe reinforcement learning navigation policies. Our approach relies on probabilistic enumeration to identify unsafe regions of operation, which are then used to construct a safe CBF-based control layer applicable to arbitrary policies. We validate our framework both in simulation and on a real robot, using a standard mobile robot benchmark and a highly dynamic aquatic environmental monitoring task. These experiments demonstrate the ability of the proposed solution to correct unsafe actions while preserving efficient navigation behavior. Our results show the promise of developing hierarchical verification-based systems to enable safe and robust navigation behaviors in complex scenarios.
- CAVModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural NetworksTianhao Wei, Hanjiang Hu*, Luca Marzari*, Kai S Yun*, Peizhi Niu*, Xusheng Luo, and Changliu Liu37th International Conference on Computer Aided Verification (CAV), 2025
Deep Neural Networks (DNN) are crucial in approximating nonlinear functions across diverse applications, ranging from image classification to control. Verifying specific input-output properties can be a highly challenging task due to the lack of a single, self-contained framework that allows a complete range of verification types. To this end, we present ModelVerification.jl (MV), the first comprehensive, cutting-edge toolbox that contains a suite of state-of-the-art methods for verifying different types of DNNs and safety specifications. This versatile toolbox is designed to empower developers and machine learning practitioners with robust tools for verifying and ensuring the trustworthiness of their DNN models.
- IJCAIRobustX: Robust Counterfactual Explanations Made EasyJunqi Jiang*, Luca Marzari*, Aaryan Purohit, and Francesco LeofanteInternational Joint Conference on Artificial Intelligence (IJCAI), 2025
The increasing use of Machine Learning (ML) models to aid decision-making in high-stakes industries demands explainability to facilitate trust. Counterfactual Explanations (CEs) are ideally suited for this, as they can offer insights into the predictions of an ML model by illustrating how changes in its input data may lead to different outcomes. However, for CEs to realise their explanatory potential, significant challenges remain in ensuring their robustness under slight changes in the scenario being explained. Despite the widespread recognition of CEs’ robustness as a fundamental requirement, a lack of standardised tools and benchmarks hinders a comprehensive and effective comparison of robust CE generation methods. In this paper, we introduce RobustX, an open-source Python library implementing a collection of CE generation and evaluation methods, with a focus on the robustness property. RobustX provides interfaces to several existing methods from the literature, enabling streamlined access to state-of-the-art techniques. The library is also easily extensible, allowing fast prototyping of novel robust CE generation and evaluation methods.
- AAMASImproving Policy Optimization via ε-RetrainLuca Marzari, Priya L Donti, Changliu Liu, and Enrico MarchesiniProceedings of the International Conference on Autonomous Agents and MultiAgent Systems (AAMAS), 2025
We present ε-retrain, an exploration strategy designed to encourage a behavioral preference while optimizing policies with monotonic improvement guarantees. To this end, we introduce an iterative procedure for collecting retrain areas – parts of the state space where an agent did not follow the behavioral preference. Our method then switches between the typical uniform restart state distribution and the retrain areas using a decaying factor ε, allowing agents to retrain on situations where they violated the preference. Experiments over hundreds of seeds across locomotion, navigation, and power network tasks show that our method yields agents that exhibit significant performance and sample efficiency improvements. Moreover, we employ formal verification of neural networks to provably quantify the degree to which agents adhere to behavioral preferences.
2024
- ECAIRigorous Probabilistic Guarantees for Robust Counterfactual ExplanationsLuca Marzari, Francesco Leofante, Ferdinando Cicalese, and Alessandro FarinelliProceedings of the 27th European Conference on Artificial Intelligence (ECAI), 2024
We study the problem of assessing the robustness of counterfactual explanations for deep learning models. We focus on plausible model shifts altering model parameters and propose a novel framework to reason about the robustness property in this setting. To motivate our solution, we begin by showing for the first time that computing the robustness of counterfactuals with respect to plausible model shifts is NP-complete. As this (practically) rules out the existence of scalable algorithms for exactly computing robustness, we propose a novel probabilistic approach which is able to provide tight estimates of robustness with strong guarantees while preserving scalability. Remarkably, and differently from existing solutions targeting plausible model shifts, our approach does not impose requirements on the network to be analyzed, thus enabling robustness analysis on a wider range of architectures. Experiments on four binary classification datasets indicate that our method improves the state of the art in generating robust explanations, outperforming existing methods on a range of metrics.
- AAAIEnumerating Safe Regions in Deep Neural Networks with Provable Probabilistic GuaranteesLuca Marzari, Davide Corsi, Enrico Marchesini, Alessandro Farinelli, and Ferdinando CicaleseProceedings of the AAAI Conference on Artificial Intelligence (AAAI), 2024
Identifying safe areas is a key point to guarantee trust for systems that are based on Deep Neural Networks (DNNs). To this end, we introduce the AllDNN-Verification problem: given a safety property and a DNN, enumerate the set of all the regions of the property input domain which are safe, i.e., where the property does hold. Due to the #P-hardness of the problem, we propose an efficient approximation method called ε-ProVe. Our approach exploits a controllable underestimation of the output reachable sets obtained via statistical prediction of tolerance limits, and can provide a tight (with provable probabilistic guarantees) lower estimate of the safe areas. Our empirical evaluation on different standard benchmarks shows the scalability and effectiveness of our method, offering valuable insights for this new type of verification of DNNs.
2023
- AIROScaling #DNN-Verification Tools with Efficient Bound Propagation and Parallel ComputingLuca Marzari, Gabriele Roncolato, and Alessandro Farinelli2023
Deep Neural Networks (DNNs) are powerful tools that have shown extraordinary results in many scenarios, ranging from pattern recognition to complex robotic problems. However, their intricate designs and lack of transparency raise safety concerns when applied in real-world applications. In this context, Formal Verification (FV) of DNNs has emerged as a valuable solution to provide provable guarantees on the safety aspect. Nonetheless, the binary answer (i.e., safe or unsafe) could be not informative enough for direct safety interventions such as safety model ranking or selection. To address this limitation, the FV problem has recently been extended to the counting version, called #DNN-Verification, for the computation of the size of the unsafe regions in a given safety property’s domain. Still, due to the complexity of the problem, existing solutions struggle to scale on real-world robotic scenarios, where the DNN can be large and complex. To address this limitation, inspired by advances in FV, in this work, we propose a novel strategy based on reachability analysis combined with Symbolic Linear Relaxation and parallel computing to enhance the efficiency of existing exact and approximate FV for DNN counters. The empirical evaluation on standard FV benchmarks and realistic robotic scenarios shows a remarkable improvement in scalability and efficiency, enabling the use of such techniques even for complex robotic applications.
- WFVML ICMLFormal Verification for Counting Unsafe Inputs in Deep Neural NetworksLuca Marzari*, Davide Corsi*, Ferdinando Cicalese, and Alessandro Farinelli2nd Workshop on Formal Verification of Machine Learning (ICML), 2023
Traditionally, Formal Verification (FV) of Deep Neural Networks (DNN) can be employed to check whether a DNN is unsafe w.r.t. some given property (i.e., whether there is at least one un- safe input configuration). However, the binary answer typically returned could be not informa- tive enough for other purposes, such as shielding, model selection, or training improvements. In this paper, we summarize the contribution of our work (Marzari et al., 2023) focused on the #DNN-Verification problem, which involves counting the number of input configurations of a DNN that result in a violation of a particular safety property. We analyze the complexity of this problem and show a novel approach that returns the exact count of violations. Due to the #P-completeness of the problem, we also propose a randomized, approximate method that provides a provable probabilistic bound of the correct count while significantly reducing compu- tational requirements tested on a set of safety- critical benchmarks.
- IJCAIThe #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural NetworksLuca Marzari, Davide Corsi, Ferdinando Cicalese, and Alessandro FarinelliInternation Joint Conference on Artificial Intelligence (IJCAI), 2023
Deep Neural Networks are increasingly adopted in critical tasks that require a high level of safety, e.g., autonomous driving. While state-of-the-art verifiers can be employed to check whether a DNN is unsafe w.r.t. some given property (i.e., whether there is at least one unsafe input configuration), their yes/no output is not informative enough for other purposes, such as shielding, model selection, or training improvements. In this paper, we introduce the #DNN-Verification problem, which involves counting the number of input configurations of a DNN that result in a violation of a particular safety property. We analyze the complexity of this problem and propose a novel approach that returns the exact count of violations. Due to the #P-completeness of the problem, we also propose a randomized, approximate method that provides a provable probabilistic bound of the correct count while significantly reducing computational requirements. We present experimental results on a set of safety-critical benchmarks that demonstrate the effectiveness of our approximate method and evaluate the tightness of the bound.
- IROSConstrained Reinforcement Learning and Formal Verification for Safe Colonoscopy NavigationDavide Corsi*, Luca Marzari*, Ameya Pore*, Alessandro Farinelli, Alicia Casals, Paolo Fiorini, and Diego Dall’AlbaInternational Conference on Intelligent Robots and Systems (IROS), 2023
The field of robotic Flexible Endoscopes (FEs) has progressed significantly, offering a promising solution to reduce patient discomfort. However, the limited autonomy of most robotic FEs results in non-intuitive and challenging manoeuvres, constraining their application in clinical settings. While previous studies have employed lumen tracking for autonomous navigation, they fail to adapt to the presence of obstructions and sharp turns when the endoscope faces the colon wall. In this work, we propose a Deep Reinforcement Learning (DRL)-based navigation strategy that eliminates the need for lumen tracking. However, the use of DRL methods poses safety risks as they do not account for potential hazards associated with the actions taken. To ensure safety, we exploit a Constrained Reinforcement Learning (CRL) method to restrict the policy in a predefined safety regime. Moreover, we present a model selection strategy that utilises Formal Verification (FV) to choose a policy that is entirely safe before deployment. We validate our approach in a virtual colonoscopy environment and report that out of the 300 trained policies, we could identify three policies that are entirely safe. Our work demonstrates that CRL, combined with model selection through FV, can improve the robustness and safety of robotic behaviour in surgical applications.
- TACASVerifying Learning-Based Robotic Navigation SystemsGuy Amir, Davide Corsi, Raz Yerushalmi, Luca Marzari, David Harel, Alessandro Farinelli, and Guy KatzIn Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2023
Deep reinforcement learning (DRL) has become a dominant deep-learning paradigm for tasks where complex policies are learned within reactive systems. Unfortunately, these policies are known to be susceptible to bugs. Despite significant progress in DNN verification, there has been little work demonstrating the use of modern verification tools on real-world, DRL-controlled systems. In this case study, we attempt to begin bridging this gap, and focus on the important task of mapless robotic navigation — a classic robotics problem, in which a robot, usually controlled by a DRL agent, needs to efficiently and safely navigate through an unknown arena towards a target. We demonstrate how modern verification engines can be used for effective model selection, i.e., selecting the best available policy for the robot in question from a pool of candidate policies. Specifically, we use verification to detect and rule out policies that may demonstrate suboptimal behavior, such as collisions and infinite loops. We also apply verification to identify models with overly conservative behavior, thus allowing users to choose superior policies, which might be better at finding shorter paths to a target. To validate our work, we conducted extensive experiments on an actual robot, and confirmed that the suboptimal policies detected by our method were indeed flawed. We also demonstrate the superiority of our verification-driven approach over state-of-the-art, gradient attacks. Our work is the first to establish the usefulness of DNN verification in identifying and filtering out suboptimal DRL policies in real-world robots, and we believe that the methods presented here are applicable to a wide range of systems that incorporate deep-learning-based agents.
- AAMASSafe Deep Reinforcement Learning by Verifying Task-Level PropertiesEnrico Marchesini*, Luca Marzari*, Alessandro Farinelli, and Christopher AmatoIn Proceedings of the 22nd International Conference on Autonomous Agents and MultiAgent Systems (AAMAS), 2023
Cost functions are commonly employed in Safe Deep Reinforcement Learning (DRL). However, the cost is typically encoded as an indicator function due to the difficulty of quantifying the risk of policy decisions in the state space. Such an encoding requires the agent to visit numerous unsafe states to learn a cost-value function to drive the learning process toward safety. Hence, increasing the number of unsafe interactions and decreasing sample efficiency. In this paper, we investigate an alternative approach that uses domain knowledge to quantify the risk in the proximity of such states by defining a violation metric. This metric is computed by verifying task-level properties, shaped as input-output conditions, and it is used as a penalty to bias the policy away from unsafe states without learning an additional value function. We investigate the benefits of using the violation metric in standard Safe DRL benchmarks and robotic mapless navigation tasks. The navigation experiments bridge the gap between Safe DRL and robotics, introducing a framework that allows rapid testing on real robots. Our experiments show that policies trained with the violation penalty achieve higher performance over Safe DRL baselines and significantly reduce the number of visited unsafe states.
- ICRAOnline Safety Property Collection and Refinement for Safe Deep Reinforcement Learning in Mapless NavigationLuca Marzari*, Enrico Marchesini*, and Alessandro FarinelliIn 2023 International Conference on Robotics and Automation (ICRA), 2023
Safety is essential for deploying Deep Reinforcement Learning (DRL) algorithms in real-world scenarios.Recently, verification approaches have been proposed to allow quantifying the number of violations of a DRL policy over input-output relationships, called properties. However, such properties are hard-coded and require task-level knowledge, making their application intractable in challenging safety-critical tasks. To this end, we introduce the Collection and Refinement of Online Properties (CROP) framework to design properties at training time. CROP employs a cost signal to identify unsafe interactions and use them to shape safety properties. Hence, we propose a refinement strategy to combine properties that model similar unsafe interactions.Our evaluation compares the benefits of computing the number of violations using standard hard-coded properties and the ones generated with CROP. We evaluate our approach in several robotic mapless navigation tasks and demonstrate that the violation metric computed with CROP allows higher returns and lower violations over previous Safe DRL approaches.
2022
2021
- IEEE ICAR