Davide Corsi

📍 Irvine, CA, USA

I am a Postdoctoral Researcher at University of California: Irvine, in the Intelligent Dynamics Lab under the supervision of Prof. Roy Fox. Previously, I worked as a visiting researcher under the supervision of Prof. Guy Katz at the Hebrew University of Jerusalem. I obtained my PhD at the University of Verona advised by Prof. Alessandro Farinelli.

My research interests center on advancing deep reinforcement learning for robotics in safety-critical settings. I work on both sides of safety: training-time methods (constrained RL and safety shields) and post-training assurance via formal verification of neural networks. Recently, I’ve been integrating foundation models (LLMs and VLMs/VLAMs) with RL for robotic control, and developing world models so agents can not only react but predict. A key focus is sim-to-real transfer and low-latency deployment on real platforms (drones, manipulators, aquatic robots), with an emphasis on measurable reliability and open, reproducible artifacts. My goal is to bridge theory and practice to deliver robust systems with clear safety guarantees. For more, see the publications page.publications page.

Places (📍) :

🇺🇸 University of California: Irvine, United States
🇮🇱 The Hebrew University of Jerusalem, Israel
🇮🇹 University of Verona, Italy

News 📢

2025	July Excited to share two new papers this month! ✨ Our work “Analyzing Adversarial Inputs in Deep Reinforcement Learning” has been accepted at AISoLA 2025. You can find it here. Another highlight: “Efficient Dynamic Shielding for Parametric Safety Specifications” has been accepted at ATVA 2025! You can read it here. June Really excited to kick off my participation in the DARPA SAFRON project 🤖. In this project, we will investigate how to integrate foundation models (LLMs, VLMs, and VLAMs) for robotic control, with a special emphasis on the safety of these systems. These models cannot simply be treated as black boxes, and I’m thrilled to explore new ways to make them safer and more reliable! May Thrilled to announce that our paper “Explanations for Unrealizability of Infinite-State Safety Shields” has been accepted at KR 2025 🎉. You can check it out here. February Our paper “Realizable Continuous-Space Shields for Safe Reinforcement Learning” has been accepted at L4DC 2025 🚀. See the paper here.
2024	December Thrilled to announce that our paper “Shield Synthesis for LTL Modulo Theories” has been accepted at AAAI 2025 🎉. You can find the paper here. Many thanks to my amazing collaborators from Israel and Spain for this work! September The result of my collaboration with the Hebrew University of Jerusalem has been accepted at ICONIP 2024, we are excited to present our new paper Enforcing Specific Behaviours via Constrained DRL and Scenario-Based Programming! 🚀 July Excited to share that my first work at the University of California: Irvine has been accepted in RLC 2024 😍. What an amazing collaboration with colleagues from all over the world Verification-Guided Shielding for Deep Reinforcement Learning! January Start of a new job at the University of California: Irvine in the Intelligent Dynamics Lab headed by Prof. Roy Fox. Really excited about this new adventure! 🇺🇸 Delight to share that our new paper “Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees” has been accepted at AAAI 2024 ✈️.
2023	July Our paper “Formal Explainability of DNN-Based Reactive Systems” has been accepted at FMCAD 2023 😍. June Our paper “Constrained Reinforcement Learning and Formal Verification for Safe Colonoscopy Navigation” has been accepted at IROS 2023 🤖. May I successfully defended my PhD thesis. A big thanks to my advisor Prof. Alessandro Farinelli and to the thesis committee Prof. Matthijs Spaan, Prof. Roberto Capobianco, and Prof. Domenico Bloisi 🎓. 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 🚀.
2022	September As a result of the research visit at the Hebrew University of Jerusalem, we submitted the papers “Verifying Learning-Based Robotic Navigation Systems” and “Constrained Reinforcement Learning for Robotics via Scenario-Based Programming” at two international conferences. February Excited to share that I’ll start a reaserach visit at the Hebrew University of Jerusalem, under the supervision of Prof. Guy Katz. 🇮🇱 January Our paper “Exploring Safer Behaviors for Deep Reinforcement Learning” has been accepted at AAAI 2022 (15% acceptance rate) 🤩.
2021	June Our two papers “Benchmarking Safe Deep Reinforcement Learning in Aquatic Navigation” and “Safe Reinforcement Learning using Formal Verification for Tissue Retraction in Autonomous Robotic-Assisted Surgery” have been accepted at IROS 2021 🤖. May Proud to share that my first main author paper “Formal Verification of Neural Networks for Safety-Critical Tasks in Deep Reinforcement Learning” has been accepted at UAI 2021 😍. Our paper “Genetic Soft Updates for Policy Evolution in Deep Reinforcement Learning” has been accepted at ICLR 2021.

Selected publications 📚

L4DC

Realizable Continuous-Space Shields for Safe Reinforcement Learning

Kim Kyungmin, Davide Corsi, Andoni Rodriguez, JB Lanier, Benjami Parellada, Pierre Baldi, Cesar Sanchez, and 1 more author

In 7th Annual Conference on Learning for Dynamics and Control, 2025

Abs HTML PDF

While Deep Reinforcement Learning (DRL) has achieved remarkable success across various domains, it remains vulnerable to occasional catastrophic failures without additional safeguards. An effective solution to prevent these failures is to use a shield that validates and adjusts the agent’s actions to ensure compliance with a provided set of safety specifications. For real-world robotic domains, it is essential to define safety specifications over continuous state and action spaces to accurately account for system dynamics and compute new actions that minimally deviate from the agent’s original decision. In this paper, we present the first shielding approach specifically designed to ensure the satisfaction of safety requirements in continuous state and action spaces, making it suitable for practical robotic applications. Our method builds upon realizability, an essential property that confirms the shield will always be able to generate a safe action for any state in the environment. We formally prove that realizability can be verified for stateful shields, enabling the incorporation of non-Markovian safety requirements, such as loop avoidance. Finally, we demonstrate the effectiveness of our approach in ensuring safety without compromising the policy’s success rate by applying it to a navigation problem and a multi-agent particle environment1. Keywords: Shielding, Reinforcement Learning, Safety, Robotics
RLC

Verification-Guided Shielding for Deep Reinforcement Learning

Davide Corsi, Guy Amir, Andoni Rodriguez, Cesar Sanchez, Guy Katz, and Roy Fox

In The 1st Reinforcement Learning Conference, 2024

Abs HTML PDF

In recent years, Deep Reinforcement Learning (DRL) has emerged as an effective approach to solving real-world tasks. However, despite their successes, DRL-based policies suffer from poor reliability, which limits their deployment in safety-critical domains. As a result, various methods have been put forth to address this issue by providing formal safety guarantees. Two main approaches include shielding and verification. While shielding ensures the safe behavior of the policy by employing an external online component (i.e., a “shield”) that overruns potentially dangerous actions, this approach has a significant computational cost as the shield must be invoked at runtime to validate every decision. On the other hand, verification is an offline process that can identify policies that are unsafe, prior to their deployment, yet, without providing alternative actions when such a policy is deemed unsafe. In this work, we present verification-guided shielding – a novel approach that bridges the DRL reliability gap by integrating these two methods. Our approach combines both formal and probabilistic verification tools to partition the input domain into safe and unsafe regions. In addition, we employ clustering and symbolic representation procedures that compress the unsafe regions into a compact representation. This, in turn, allows to temporarily activate the shield solely in (potentially) unsafe regions, in an efficient manner. Our novel approach allows to significantly reduce runtime overhead while still preserving formal safety guarantees. We extensively evaluate our approach on two benchmarks from the robotic navigation domain, as well as provide an in-depth analysis of its scalability and completeness.
AAAI

Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees

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

In The 38th AAAI Conference on Artificial Intelligence, 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.
IROS

Safe Reinforcement Learning Using Formal Verification for Tissue Retraction in Autonomous Robotic-Assisted Surgery

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

In IEEE International Conference on Intelligent Robots and Systems, 2021

Abs HTML

Deep Reinforcement Learning (DRL) is a viable solution for automating repetitive surgical subtasks due to its ability to learn complex behaviours in a dynamic environment. This task automation could lead to reduced surgeon’s cognitive workload, increased precision in critical aspects of the surgery, and fewer patient-related complications. However, current DRL methods do not guarantee any safety criteria as they maximise cumulative rewards without considering the risks associated with the actions performed. Due to this limitation, the application of DRL in the safety-critical paradigm of robot-assisted Minimally Invasive Surgery (MIS) has been constrained. In this work, we introduce a Safe-DRL framework that incorporates safety constraints for the automation of surgical subtasks via DRL training. We validate our approach in a virtual scene that replicates a tissue retraction task commonly occurring in multiple phases of an MIS. Furthermore, to evaluate the safe behaviour of the robotic arms, we formulate a formal verification tool for DRL methods that provides the probability of unsafe configurations. Our results indicate that a formal analysis guarantees safety with high confidence such that the robotic instruments operate within the safe workspace and avoid hazardous interaction with other anatomical structures.