Luca Marzari

📍University of Verona

Verona, Italy 🇮🇹

I am a second-year PhD student in Computer Science at the University of Verona, advised by Prof. Alessandro Farinelli and Prof. Ferdinando Cicalese. I am also a visiting researcher in the Robotics Institute at Carnegie Mellon University (CMU), under the supervision of Prof. Changliu Liu.

My Research Interests focus on developing efficient and reliable methods for provably verifying the correctness of Deep Neural Networks (DNNs), particularly in the context of Deep Reinforcement Learning (DRL) applications. I am also developing approximation algorithms with strong theoretical guarantees to bridge the gap between Formal Verification of DNNs and safe DRL. You can visit the publications page for more information on my research activity.

Outside of work, I am a rock climber🧗🏻 and I also love hiking⛰️ and photography📸.

News 📢

2024	January Our paper “Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees” has been selected for an oral presentation at AAAI 2024 🤩.
2023	Dec New paper accepted at AAAI 2024: “Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees”. Nov “Scaling #DNN-Verification Tools with Efficient Bound Propagation and Parallel Computing” has been accepted at the 10th Italian Workshop on Artificial Intelligence and Robotics (AIRO 2023) , co-located with the 22nd International Conference of the Italian Association for Artificial Intelligence (AIIA 2023). Jun* Our paper “Formal Verification for Counting Unsafe Inputs in Deep Neural Networks” has been accepted at the 2nd Workshop on Formal Verification of Machine Learning (WFVML 2023) at ICML 2023! Our paper “Constrained Reinforcement Learning and Formal Verification for Safe Colonoscopy Navigation” has been accepted at IROS 2023! 🤖 May Excited to share that in July I’ll start a research visit at the Intelligent Controll Lab part of the Robotics Institute at Carnegie Mellon University(CMU) 🇺🇸, under the supervision of Prof. Changliu Liu. April Our paper “The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks” has been accepted at IJCAI 2023 (15% acceptance rate) 🤩. January Our paper “Verifying Learning-Based Robotic Navigation Systems” in collaboration with The Katz Lab has been accepted at ETAPS TACAS 2023 🚀. Our paper “Online Safety Property Collection and Refinement for Safe Deep Reinforcement Learning in Mapless Navigation” has been accepted at ICRA 2023. Our paper “Safe Deep Reinforcement Learning by Verifying Task-Level Properties” has been accepted at AAMAS 2023.
2022	October Excited to start a PhD in Computer Science advised by Prof. Alessandro Farinelli and Prof. Ferdinando Cicalese at the Department of Computer Science, Verona. April I Started a Research Fellowship under the supervision of Prof. Alessandro Farinelli at the Department of Computer Science, Verona.
2021	December 1 poster paper accepted at ACM SAC IRMAS (< 25% acceptance rate) on “Curriculum Learning For Safe Mapless Navigation”. September 1 paper accepted at IEEE ICAR on “Towards Hierarchical Task Decomposition using Deep Reinforcement Learning for Pick and Place Subtasks”.

Selected publications 📚

AAAI

Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees

Luca Marzari, Davide Corsi, Enrico Marchesini, Alessandro Farinelli, and Ferdinando Cicalese

Proceedings of the AAAI Conference on Artificial Intelligence (AAAI), 2024

Abs HTML PDF

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.
IJCAI

The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks

Luca Marzari*, Davide Corsi*, Ferdinando Cicalese, and Alessandro Farinelli

Internation Joint Conference on Artificial Intelligence (IJCAI), 2023

Abs HTML PDF

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.
IROS

Constrained Reinforcement Learning and Formal Verification for Safe Colonoscopy Navigation

Davide Corsi*, Luca Marzari*, Ameya Pore*, Alessandro Farinelli, Alicia Casals, Paolo Fiorini, and Diego Dall’Alba

International Conference on Intelligent Robots and Systems (IROS), 2023

Abs HTML PDF

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.