8 citations · 37 across the 26 of their papers we have counts for
27 papers
veriFIRE: an Industrial Case Study in Verifying Consistency Properties for a DNN-Based Wildfire Detection System
Idan Refaeli, Maya Swisa, Itay Buchnik +5
We present our ongoing work on the veriFIRE project: a collaboration between industry and academia, aimed at applying verification to increase the reliability of a real-world, safe…
Agent Security is a Systems Problem
Mihai Christodorescu, Earlence Fernandes, Ashish Hooda +11
We take the position that agent security must be approached as a systems problem: the AI model powering the agent must be treated as an untrusted component, and security invariants…
NEST: Network Enforced Session Types (Technical Report)
Jens Kanstrup Larsen, Alceste Scalas, Guy Amir +3
This paper introduces NEST (Network-Enforced Session Types), a runtime verification framework that moves application-level protocol monitoring into the network fabric. Unlike prior…
Formal Policy Enforcement for Agentic Systems
Nils Palumbo, Sarthak Choudhary, Jihye Choi +4
As agentic computing systems grow increasingly popular, they raise serious security concerns due to their susceptibility to various attacks. While prior research efforts aim to mit…
Deciding Serializability in Network Systems
Guy Amir, Mark Barbone, Nicolas Amat +1
We present the SER modeling language for automatically verifying serializability of concurrent programs, i.e., whether every concurrent execution of the program is equivalent to so…
On Improving Deep Active Learning with Formal Verification
Jonathan Spiegelman, Guy Amir, Guy Katz
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 sa…
What makes an Ensemble (Un) Interpretable?
Shahaf Bassan, Guy Amir, Meirav Zehavi +1
Ensemble models are widely recognized in the ML community for their limited interpretability. For instance, while a single decision tree is considered interpretable, ensembles of t…
Hard to Explain: On the Computational Hardness of In-Distribution Model Interpretation
Guy Amir, Shahaf Bassan, Guy Katz
The ability to interpret Machine Learning (ML) models is becoming increasingly essential. However, despite significant progress in the field, there remains a lack of rigorous chara…
Safe and Reliable Training of Learning-Based Aerospace Controllers
Udayan Mandal, Guy Amir, Haoze Wu +10
In recent years, deep reinforcement learning (DRL) approaches have generated highly successful controllers for a myriad of complex domains. However, the opaque nature of these mode…
Verifying the Generalization of Deep Learning to Out-of-Distribution Domains
Guy Amir, Osher Maayan, Tom Zelazny +2
Deep neural networks (DNNs) play a crucial role in the field of machine learning, demonstrating state-of-the-art performance across various application domains. However, despite th…
Verification-Guided Shielding for Deep Reinforcement Learning
Davide Corsi, Guy Amir, Andoni Rodriguez +3
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 fro…
Local vs. Global Interpretability: A Computational Complexity Perspective
Shahaf Bassan, Guy Amir, Guy Katz
The local and global interpretability of various ML models has been studied extensively in recent years. However, despite significant progress in the field, many known results rema…
Shield Synthesis for LTL Modulo Theories
Andoni Rodriguez, Guy Amir, Davide Corsi +2
In recent years, Machine Learning (ML) models have achieved remarkable success in various domains. However, these models also tend to demonstrate unsafe behaviors, precluding their…
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
Udayan Mandal, Guy Amir, Haoze Wu +9
Deep reinforcement learning (DRL) is a powerful machine learning paradigm for generating agents that control autonomous systems. However, the ``black box'' nature of DRL agents lim…
Analyzing Adversarial Inputs in Deep Reinforcement Learning
Davide Corsi, Guy Amir, Guy Katz +1
In recent years, Deep Reinforcement Learning (DRL) has become a popular paradigm in machine learning due to its successful applications to real-world and complex systems. However,…
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Haoze Wu, Omri Isac, Aleksandar Zeljić +14
This paper serves as a comprehensive system description of version 2.0 of the Marabou framework for formal analysis of neural networks. We discuss the tool's architectural design a…
Formally Explaining Neural Networks within Reactive Systems
Shahaf Bassan, Guy Amir, Davide Corsi +2
Deep neural networks (DNNs) are increasingly being used as controllers in reactive systems. However, DNNs are highly opaque, which renders it difficult to explain and justify their…
Verifying Generalization in Deep Learning
Guy Amir, Osher Maayan, Tom Zelazny +2
Deep neural networks (DNNs) are the workhorses of deep learning, which constitutes the state of the art in numerous application domains. However, DNN-based decision rules are notor…
veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System
Guy Amir, Ziv Freund, Guy Katz +2
In this short paper, we present our ongoing work on the veriFIRE project -- a collaboration between industry and academia, aimed at using verification for increasing the reliabilit…
Constrained Reinforcement Learning for Robotics via Scenario-Based Programming
Davide Corsi, Raz Yerushalmi, Guy Amir +3
Deep reinforcement learning (DRL) has achieved groundbreaking successes in a wide variety of robotic applications. A natural consequence is the adoption of this paradigm for safety…
Verifying Learning-Based Robotic Navigation Systems
Guy Amir, Davide Corsi, Raz Yerushalmi +4
Deep reinforcement learning (DRL) has become a dominant deep-learning paradigm for tasks where complex policies are learned within reactive systems. Unfortunately, these policies a…
Scenario-Assisted Deep Reinforcement Learning
Raz Yerushalmi, Guy Amir, Achiya Elyasaf +3
Deep reinforcement learning has proven remarkably useful in training agents from unstructured data. However, the opacity of the produced agents makes it difficult to ensure that th…
Verification-Aided Deep Ensemble Selection
Guy Amir, Tom Zelazny, Guy Katz +1
Deep neural networks (DNNs) have become the technology of choice for realizing a variety of complex tasks. However, as highlighted by many recent studies, even an imperceptible per…
Towards Scalable Verification of Deep Reinforcement Learning
Guy Amir, Michael Schapira, Guy Katz
Deep neural networks (DNNs) have gained significant popularity in recent years, becoming the state of the art in a variety of domains. In particular, deep reinforcement learning (D…