-
Logarithmic systolic growth for hyperbolic surfaces in every genus
Authors:
Mikhail G. Katz,
Stephane Sabourau
Abstract:
More than thirty years ago, Brooks and Buser-Sarnak constructed sequences of closed hyperbolic surfaces with logarithmic systolic growth in the genus. Recently, Liu and Petri showed that such logarithmic systolic lower bound holds for every genus (not merely for genera in some infinite sequence) using random surfaces. In this article, we show a similar result through a more direct approach relying…
▽ More
More than thirty years ago, Brooks and Buser-Sarnak constructed sequences of closed hyperbolic surfaces with logarithmic systolic growth in the genus. Recently, Liu and Petri showed that such logarithmic systolic lower bound holds for every genus (not merely for genera in some infinite sequence) using random surfaces. In this article, we show a similar result through a more direct approach relying on the original Brooks/Buser-Sarnak surfaces.
△ Less
Submitted 2 July, 2024;
originally announced July 2024.
-
Formal Verification of Object Detection
Authors:
Avraham Raviv,
Yizhak Y. Elboher,
Michelle Aluf-Medina,
Yael Leibovich Weiss,
Omer Cohen,
Roy Assa,
Guy Katz,
Hillel Kugler
Abstract:
Deep Neural Networks (DNNs) are ubiquitous in real-world applications, yet they remain vulnerable to errors and adversarial attacks. This work tackles the challenge of applying formal verification to ensure the safety of computer vision models, extending verification beyond image classification to object detection. We propose a general formulation for certifying the robustness of object detection…
▽ More
Deep Neural Networks (DNNs) are ubiquitous in real-world applications, yet they remain vulnerable to errors and adversarial attacks. This work tackles the challenge of applying formal verification to ensure the safety of computer vision models, extending verification beyond image classification to object detection. We propose a general formulation for certifying the robustness of object detection models using formal verification and outline implementation strategies compatible with state-of-the-art verification tools. Our approach enables the application of these tools, originally designed for verifying classification models, to object detection. We define various attacks for object detection, illustrating the diverse ways adversarial inputs can compromise neural network outputs. Our experiments, conducted on several common datasets and networks, reveal potential errors in object detection models, highlighting system vulnerabilities and emphasizing the need for expanding formal verification to these new domains. This work paves the way for further research in integrating formal verification across a broader range of computer vision applications.
△ Less
Submitted 1 July, 2024;
originally announced July 2024.
-
Verification-Guided Shielding for Deep Reinforcement Learning
Authors:
Davide Corsi,
Guy Amir,
Andoni Rodriguez,
Cesar Sanchez,
Guy Katz,
Roy Fox
Abstract:
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. Various methods have been put forth to address this issue by providing formal safety guarantees. Two main approaches include shielding and ver…
▽ More
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. 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 overrides 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.
△ Less
Submitted 20 June, 2024; v1 submitted 10 June, 2024;
originally announced June 2024.
-
Shield Synthesis for LTL Modulo Theories
Authors:
Andoni Rodriguez,
Guy Amir,
Davide Corsi,
Cesar Sanchez,
Guy Katz
Abstract:
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 deployment in safety-critical systems. To cope with this issue, ample research focuses on develo** methods that guarantee the safe behaviour of a given ML model. A prominent example is shielding which incorporates an…
▽ More
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 deployment in safety-critical systems. To cope with this issue, ample research focuses on develo** methods that guarantee the safe behaviour of a given ML model. A prominent example is shielding which incorporates an external component (a "shield") that blocks unwanted behavior. Despite significant progress, shielding suffers from a main setback: it is currently geared towards properties encoded solely in propositional logics (e.g., LTL) and is unsuitable for richer logics. This, in turn, limits the widespread applicability of shielding in many real-world systems. In this work, we address this gap, and extend shielding to LTL modulo theories, by building upon recent advances in reactive synthesis modulo theories. This allowed us to develop a novel approach for generating shields conforming to complex safety specifications in these more expressive, logics. We evaluated our shields and demonstrate their ability to handle rich data with temporal dynamics. To the best of our knowledge, this is the first approach for synthesizing shields for such expressivity.
△ Less
Submitted 6 June, 2024;
originally announced June 2024.
-
Local vs. Global Interpretability: A Computational Complexity Perspective
Authors:
Shahaf Bassan,
Guy Amir,
Guy Katz
Abstract:
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 remain informal or lack sufficient mathematical rigor. We propose a framework for bridging this gap, by using computational complexity theory to assess local and global perspectives of interpreting ML models. We begin by pro…
▽ More
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 remain informal or lack sufficient mathematical rigor. We propose a framework for bridging this gap, by using computational complexity theory to assess local and global perspectives of interpreting ML models. We begin by proposing proofs for two novel insights that are essential for our analysis: (1) a duality between local and global forms of explanations; and (2) the inherent uniqueness of certain global explanation forms. We then use these insights to evaluate the complexity of computing explanations, across three model types representing the extremes of the interpretability spectrum: (1) linear models; (2) decision trees; and (3) neural networks. Our findings offer insights into both the local and global interpretability of these models. For instance, under standard complexity assumptions such as P != NP, we prove that selecting global sufficient subsets in linear models is computationally harder than selecting local subsets. Interestingly, with neural networks and decision trees, the opposite is true: it is harder to carry out this task locally than globally. We believe that our findings demonstrate how examining explainability through a computational complexity lens can help us develop a more rigorous grasp of the inherent interpretability of ML models.
△ Less
Submitted 7 June, 2024; v1 submitted 5 June, 2024;
originally announced June 2024.
-
Verifying the Generalization of Deep Learning to Out-of-Distribution Domains
Authors:
Guy Amir,
Osher Maayan,
Tom Zelazny,
Guy Katz,
Michael Schapira
Abstract:
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 their success, DNN-based models may occasionally exhibit challenges with generalization, i.e., may fail to handle inputs that were not encountered during training. This limitation is a significant challenge when it comes t…
▽ More
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 their success, DNN-based models may occasionally exhibit challenges with generalization, i.e., may fail to handle inputs that were not encountered during training. This limitation is a significant challenge when it comes to deploying deep learning for safety-critical tasks, as well as in real-world settings characterized by substantial variability. We introduce a novel approach for harnessing DNN verification technology to identify DNN-driven decision rules that exhibit robust generalization to previously unencountered input domains. Our method assesses generalization within an input domain by measuring the level of agreement between independently trained deep neural networks for inputs in this domain. We also efficiently realize our approach by using off-the-shelf DNN verification engines, and extensively evaluate it on both supervised and unsupervised DNN benchmarks, including a deep reinforcement learning (DRL) system for Internet congestion control -- demonstrating the applicability of our approach for real-world settings. Moreover, our research introduces a fresh objective for formal verification, offering the prospect of mitigating the challenges linked to deploying DNN-driven systems in real-world scenarios.
△ Less
Submitted 30 June, 2024; v1 submitted 4 June, 2024;
originally announced June 2024.
-
Mutually unbiased bases via complex projective trigonometry
Authors:
Mikhail G. Katz
Abstract:
We give a synthetic construction of a complete system of mutually unbiased bases in $\mathbb{C}^3$.
We give a synthetic construction of a complete system of mutually unbiased bases in $\mathbb{C}^3$.
△ Less
Submitted 31 May, 2024;
originally announced May 2024.
-
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
Authors:
Udayan Mandal,
Guy Amir,
Haoze Wu,
Ieva Daukantas,
Fletcher Lee Newell,
Umberto J. Ravaioli,
Baoluo Meng,
Michael Durling,
Milan Ganai,
Tobey Shim,
Guy Katz,
Clark Barrett
Abstract:
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 limits their deployment in real-world safety-critical applications. A promising approach for providing strong guarantees on an agent's behavior is to use Neural Lyapunov Barrier (NLB) certificates, which are learned functions…
▽ More
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 limits their deployment in real-world safety-critical applications. A promising approach for providing strong guarantees on an agent's behavior is to use Neural Lyapunov Barrier (NLB) certificates, which are learned functions over the system whose properties indirectly imply that an agent behaves as desired. However, NLB-based certificates are typically difficult to learn and even more difficult to verify, especially for complex systems. In this work, we present a novel method for training and verifying NLB-based certificates for discrete-time systems. Specifically, we introduce a technique for certificate composition, which simplifies the verification of highly-complex systems by strategically designing a sequence of certificates. When jointly verified with neural network verification engines, these certificates provide a formal guarantee that a DRL agent both achieves its goals and avoids unsafe behavior. Furthermore, we introduce a technique for certificate filtering, which significantly simplifies the process of producing formally verified certificates. We demonstrate the merits of our approach with a case study on providing safety and liveness guarantees for a DRL-controlled spacecraft.
△ Less
Submitted 22 May, 2024;
originally announced May 2024.
-
A Certified Proof Checker for Deep Neural Network Verification
Authors:
Remi Desmartin,
Omri Isac,
Ekaterina Komendantskaya,
Kathrin Stark,
Grant Passmore,
Guy Katz
Abstract:
Recent advances in the verification of deep neural networks (DNNs) have opened the way for broader usage of DNN verification technology in many application areas, including safety-critical ones. DNN verifiers are themselves complex programs that have been shown to be susceptible to errors and imprecisions; this in turn has raised the question of trust in DNN verifiers. One prominent attempt to add…
▽ More
Recent advances in the verification of deep neural networks (DNNs) have opened the way for broader usage of DNN verification technology in many application areas, including safety-critical ones. DNN verifiers are themselves complex programs that have been shown to be susceptible to errors and imprecisions; this in turn has raised the question of trust in DNN verifiers. One prominent attempt to address this issue is enhancing DNN verifiers with the capability of producing proofs of their results that are subject to independent algorithmic certification (proof checking). Formulations of proof production and proof checking already exist on top of the state-of-the-art Marabou DNN verifier. The native implementation of the proof checking algorithm for Marabou was done in C++ and itself raised the question of trust in the code (e.g., in the precision of floating point calculations or guarantees for implementation soundness). Here, we present an alternative implementation of the Marabou proof checking algorithm in Imandra -- an industrial functional programming language and prover -- that allows us to obtain an implementation with formal guarantees, including proofs of mathematical results underlying the algorithm, such as the use of the Farkas lemma.
△ Less
Submitted 17 May, 2024;
originally announced May 2024.
-
Markov flow policy -- deep MC
Authors:
Nitsan Soffair,
Gilad Katz
Abstract:
Discounted algorithms often encounter evaluation errors due to their reliance on short-term estimations, which can impede their efficacy in addressing simple, short-term tasks and impose undesired temporal discounts (\(γ\)). Interestingly, these algorithms are often tested without applying a discount, a phenomenon we refer as the \textit{train-test bias}. In response to these challenges, we propos…
▽ More
Discounted algorithms often encounter evaluation errors due to their reliance on short-term estimations, which can impede their efficacy in addressing simple, short-term tasks and impose undesired temporal discounts (\(γ\)). Interestingly, these algorithms are often tested without applying a discount, a phenomenon we refer as the \textit{train-test bias}. In response to these challenges, we propose the Markov Flow Policy, which utilizes a non-negative neural network flow to enable comprehensive forward-view predictions. Through integration into the TD7 codebase and evaluation using the MuJoCo benchmark, we observe significant performance improvements, positioning MFP as a straightforward, practical, and easily implementable solution within the domain of average rewards algorithms.
△ Less
Submitted 2 June, 2024; v1 submitted 1 May, 2024;
originally announced May 2024.
-
Explicit Lipschitz Value Estimation Enhances Policy Robustness Against Perturbation
Authors:
Xulin Chen,
Ruipeng Liu,
Garrett E. Katz
Abstract:
In robotic control tasks, policies trained by reinforcement learning (RL) in simulation often experience a performance drop when deployed on physical hardware, due to modeling error, measurement error, and unpredictable perturbations in the real world. Robust RL methods account for this issue by approximating a worst-case value function during training, but they can be sensitive to approximation e…
▽ More
In robotic control tasks, policies trained by reinforcement learning (RL) in simulation often experience a performance drop when deployed on physical hardware, due to modeling error, measurement error, and unpredictable perturbations in the real world. Robust RL methods account for this issue by approximating a worst-case value function during training, but they can be sensitive to approximation errors in the value function and its gradient before training is complete. In this paper, we hypothesize that Lipschitz regularization can help condition the approximated value function gradients, leading to improved robustness after training. We test this hypothesis by combining Lipschitz regularization with an application of Fast Gradient Sign Method to reduce approximation errors when evaluating the value function under adversarial perturbations. Our empirical results demonstrate the benefits of this approach over prior work on a number of continuous control benchmarks.
△ Less
Submitted 24 May, 2024; v1 submitted 22 April, 2024;
originally announced April 2024.
-
Nonpositively curved surfaces are Loewner
Authors:
Mikhail G. Katz,
Stephane Sabourau
Abstract:
We show that every closed nonpositively curved surface satisfies Loewner's systolic inequality. The proof relies on a combination of the Gauss-Bonnet formula with an averaging argument using the invariance of the Liouville measure under the geodesic flow. This enables us to find a disk with large total curvature around its center yielding a large area.
We show that every closed nonpositively curved surface satisfies Loewner's systolic inequality. The proof relies on a combination of the Gauss-Bonnet formula with an averaging argument using the invariance of the Liouville measure under the geodesic flow. This enables us to find a disk with large total curvature around its center yielding a large area.
△ Less
Submitted 3 July, 2024; v1 submitted 31 March, 2024;
originally announced April 2024.
-
Leveraging Symmetries in Gaits for Reinforcement Learning: A Case Study on Quadrupedal Gaits
Authors:
Jiayu Ding,
Xulin Chen,
Garret E. Katz,
Zhenyu Gan
Abstract:
In this research, we address the complex task of develo** versatile and agile quadrupedal gaits for robotic platforms, a domain predominantly governed by model-based trajectory optimization methods. We propose an innovative, reference-free reinforcement learning framework that exploits the intrinsic symmetries of dynamic systems to synthesize a broad array of naturalistic quadrupedal locomotion…
▽ More
In this research, we address the complex task of develo** versatile and agile quadrupedal gaits for robotic platforms, a domain predominantly governed by model-based trajectory optimization methods. We propose an innovative, reference-free reinforcement learning framework that exploits the intrinsic symmetries of dynamic systems to synthesize a broad array of naturalistic quadrupedal locomotion patterns. By capitalizing on distinct symmetry characteristics - namely temporal, morphological, and time-reversal - our approach efficiently facilitates the generation and transition among diverse gaits such as pronking, bounding half-bounding and gallo**, across a spectrum of velocities, circumventing the necessity for expert-generated trajectories or complex reward structures. Implemented on the Petoi Bittle robotic model, our methodology illustrates robust and adaptable gait generation capabilities, significantly broadening the scope for robotic mobility and speed adaptability. This contribution not only advances our comprehension of quadrupedal locomotion mechanisms but also underscores the pivotal role of symmetry in the development of scalable and effective robotic gait strategies. Our findings hold substantial implications for robotic design and control, potentially enhancing operational versatility and efficiency across a variety of deployment environments.
△ Less
Submitted 14 June, 2024; v1 submitted 15 March, 2024;
originally announced March 2024.
-
NLP Verification: Towards a General Methodology for Certifying Robustness
Authors:
Marco Casadio,
Tanvi Dinkar,
Ekaterina Komendantskaya,
Luca Arnaboldi,
Matthew L. Daggitt,
Omri Isac,
Guy Katz,
Verena Rieser,
Oliver Lemon
Abstract:
Deep neural networks have exhibited substantial success in the field of Natural Language Processing and ensuring their safety and reliability is crucial: there are safety critical contexts where such models must be robust to variability or attack, and give guarantees over their output. Unlike Computer Vision, NLP lacks a unified verification methodology and, despite recent advancements in literatu…
▽ More
Deep neural networks have exhibited substantial success in the field of Natural Language Processing and ensuring their safety and reliability is crucial: there are safety critical contexts where such models must be robust to variability or attack, and give guarantees over their output. Unlike Computer Vision, NLP lacks a unified verification methodology and, despite recent advancements in literature, they are often light on the pragmatical issues of NLP verification. In this paper, we attempt to distil and evaluate general components of an NLP verification pipeline, that emerges from the progress in the field to date. Our contributions are two-fold. Firstly, we give a general (i.e. algorithm-independent) characterisation of verifiable subspaces that result from embedding sentences into continuous spaces. We identify, and give an effective method to deal with, the technical challenge of semantic generalisability of verified subspaces; and propose it as a standard metric in the NLP verification pipelines (alongside with the standard metrics of model accuracy and model verifiability). Secondly, we propose a general methodology to analyse the effect of the embedding gap -- a problem that refers to the discrepancy between verification of geometric subspaces, and the semantic meaning of sentences which the geometric subspaces are supposed to represent. In extreme cases, poor choices in embedding of sentences may invalidate verification results. We propose a number of practical NLP methods that can help to quantify the effects of the embedding gap; and in particular we propose the metric of falsifiability of semantic subspaces as another fundamental metric to be reported as part of the NLP verification pipeline. We believe that together these general principles pave the way towards a more consolidated and effective development of this new domain.
△ Less
Submitted 31 May, 2024; v1 submitted 15 March, 2024;
originally announced March 2024.
-
Analyzing Adversarial Inputs in Deep Reinforcement Learning
Authors:
Davide Corsi,
Guy Amir,
Guy Katz,
Alessandro Farinelli
Abstract:
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, even the state-of-the-art DRL models have been shown to suffer from reliability concerns -- for example, their susceptibility to adversarial inputs, i.e., small and abundant input perturbations that can fool the models i…
▽ More
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, even the state-of-the-art DRL models have been shown to suffer from reliability concerns -- for example, their susceptibility to adversarial inputs, i.e., small and abundant input perturbations that can fool the models into making unpredictable and potentially dangerous decisions. This drawback limits the deployment of DRL systems in safety-critical contexts, where even a small error cannot be tolerated. In this work, we present a comprehensive analysis of the characterization of adversarial inputs, through the lens of formal verification. Specifically, we introduce a novel metric, the Adversarial Rate, to classify models based on their susceptibility to such perturbations, and present a set of tools and algorithms for its computation. Our analysis empirically demonstrates how adversarial inputs can affect the safety of a given DRL system with respect to such perturbations. Moreover, we analyze the behavior of these configurations to suggest several useful practices and guidelines to help mitigate the vulnerability of trained DRL networks.
△ Less
Submitted 7 February, 2024;
originally announced February 2024.
-
Exploring Felix Klein's contested modernism
Authors:
Peter Heinig,
Mikhail G. Katz,
Karl Kuhlemann,
Jan Peter Schaefermeyer,
David Sherry
Abstract:
An alleged opposition between David Hilbert and Felix Klein as modern vs countermodern has been pursued by marxist historian Herbert Mehrtens and others. Scholars such as Epple, Grattan-Guinness, Gray, Quinn, Rowe, and recently Siegmund-Schultze and Mazzotti have voiced a range of opinions concerning Mehrtens' dialectical methodology. We explore contrasting perspectives on Klein's contested modern…
▽ More
An alleged opposition between David Hilbert and Felix Klein as modern vs countermodern has been pursued by marxist historian Herbert Mehrtens and others. Scholars such as Epple, Grattan-Guinness, Gray, Quinn, Rowe, and recently Siegmund-Schultze and Mazzotti have voiced a range of opinions concerning Mehrtens' dialectical methodology. We explore contrasting perspectives on Klein's contested modernism, as well as Hilbert's and Klein's views on intuition, logic, and physics. We analyze Jeremy Gray's comment on Klein's ethnographic speculations concerning Jewish mathematicians and find it to be untenable. We argue that Mehrtens was looking for countermoderns at the wrong address.
△ Less
Submitted 31 January, 2024;
originally announced February 2024.
-
Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing
Authors:
Yizhak Elboher,
Raya Elsaleh,
Omri Isac,
Mélanie Ducoffe,
Audrey Galametz,
Guillaume Povéda,
Ryma Boumazouza,
Noémie Cohen,
Guy Katz
Abstract:
As deep neural networks (DNNs) are becoming the prominent solution for many computational problems, the aviation industry seeks to explore their potential in alleviating pilot workload and in improving operational safety. However, the use of DNNs in this type of safety-critical applications requires a thorough certification process. This need can be addressed through formal verification, which pro…
▽ More
As deep neural networks (DNNs) are becoming the prominent solution for many computational problems, the aviation industry seeks to explore their potential in alleviating pilot workload and in improving operational safety. However, the use of DNNs in this type of safety-critical applications requires a thorough certification process. This need can be addressed through formal verification, which provides rigorous assurances -- e.g.,~by proving the absence of certain mispredictions. In this case-study paper, we demonstrate this process using an image-classifier DNN currently under development at Airbus and intended for use during the aircraft taxiing phase. We use formal methods to assess this DNN's robustness to three common image perturbation types: noise, brightness and contrast, and some of their combinations. This process entails multiple invocations of the underlying verifier, which might be computationally expensive; and we therefore propose a method that leverages the monotonicity of these robustness properties, as well as the results of past verification queries, in order to reduce the overall number of verification queries required by nearly 60%. Our results provide an indication of the level of robustness achieved by the DNN classifier under study, and indicate that it is considerably more vulnerable to noise than to brightness or contrast perturbations.
△ Less
Submitted 28 June, 2024; v1 submitted 8 January, 2024;
originally announced February 2024.
-
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Authors:
Haoze Wu,
Omri Isac,
Aleksandar Zeljić,
Teruhiro Tagomori,
Matthew Daggitt,
Wen Kokke,
Idan Refaeli,
Guy Amir,
Kyle Julian,
Shahaf Bassan,
Pei Huang,
Ori Lahav,
Min Wu,
Min Zhang,
Ekaterina Komendantskaya,
Guy Katz,
Clark Barrett
Abstract:
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 and highlight the major features and components introduced since its initial release.
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 and highlight the major features and components introduced since its initial release.
△ Less
Submitted 20 May, 2024; v1 submitted 25 January, 2024;
originally announced January 2024.
-
DEM: A Method for Certifying Deep Neural Network Classifier Outputs in Aerospace
Authors:
Guy Katz,
Natan Levy,
Idan Refaeli,
Raz Yerushalmi
Abstract:
Software development in the aerospace domain requires adhering to strict, high-quality standards. While there exist regulatory guidelines for commercial software in this domain (e.g., ARP-4754 and DO-178), these do not apply to software with deep neural network (DNN) components. Consequently, it is unclear how to allow aerospace systems to benefit from the deep learning revolution. Our work here s…
▽ More
Software development in the aerospace domain requires adhering to strict, high-quality standards. While there exist regulatory guidelines for commercial software in this domain (e.g., ARP-4754 and DO-178), these do not apply to software with deep neural network (DNN) components. Consequently, it is unclear how to allow aerospace systems to benefit from the deep learning revolution. Our work here seeks to address this challenge with a novel, output-centric approach for DNN certification. Our method employs statistical verification techniques, and has the key advantage of being able to flag specific inputs for which the DNN's output may be unreliable - so that they may be later inspected by a human expert. To achieve this, our method conducts a statistical analysis of the DNN's predictions for other, nearby inputs, in order to detect inconsistencies. This is in contrast to existing techniques, which typically attempt to certify the entire DNN, as opposed to individual outputs. Our method uses the DNN as a black-box, and makes no assumptions about its topology. We hope that this work constitutes another step towards integrating DNNs in safety-critical applications - especially in the aerospace domain, where high standards of quality and reliability are crucial.
△ Less
Submitted 25 June, 2024; v1 submitted 4 January, 2024;
originally announced January 2024.
-
On Augmenting Scenario-Based Modeling with Generative AI
Authors:
David Harel,
Guy Katz,
Assaf Marron,
Smadar Szekely
Abstract:
The manual modeling of complex systems is a daunting task; and although a plethora of methods exist that mitigate this issue, the problem remains very difficult. Recent advances in generative AI have allowed the creation of general-purpose chatbots, capable of assisting software engineers in various modeling tasks. However, these chatbots are often inaccurate, and an unstructured use thereof could…
▽ More
The manual modeling of complex systems is a daunting task; and although a plethora of methods exist that mitigate this issue, the problem remains very difficult. Recent advances in generative AI have allowed the creation of general-purpose chatbots, capable of assisting software engineers in various modeling tasks. However, these chatbots are often inaccurate, and an unstructured use thereof could result in erroneous system models. In this paper, we outline a method for the safer and more structured use of chatbots as part of the modeling process. To streamline this integration, we propose leveraging scenario-based modeling techniques, which are known to facilitate the automated analysis of models. We argue that through iterative invocations of the chatbot and the manual and automatic inspection of the resulting models, a more accurate system model can eventually be obtained. We describe favorable preliminary results, which highlight the potential of this approach.
△ Less
Submitted 4 January, 2024;
originally announced January 2024.
-
Detecting Anomalous Network Communication Patterns Using Graph Convolutional Networks
Authors:
Yizhak Vaisman,
Gilad Katz,
Yuval Elovici,
Asaf Shabtai
Abstract:
To protect an organizations' endpoints from sophisticated cyberattacks, advanced detection methods are required. In this research, we present GCNetOmaly: a graph convolutional network (GCN)-based variational autoencoder (VAE) anomaly detector trained on data that include connection events among internal and external machines. As input, the proposed GCN-based VAE model receives two matrices: (i) th…
▽ More
To protect an organizations' endpoints from sophisticated cyberattacks, advanced detection methods are required. In this research, we present GCNetOmaly: a graph convolutional network (GCN)-based variational autoencoder (VAE) anomaly detector trained on data that include connection events among internal and external machines. As input, the proposed GCN-based VAE model receives two matrices: (i) the normalized adjacency matrix, which represents the connections among the machines, and (ii) the feature matrix, which includes various features (demographic, statistical, process-related, and Node2vec structural features) that are used to profile the individual nodes/machines. After training the model on data collected for a predefined time window, the model is applied on the same data; the reconstruction score obtained by the model for a given machine then serves as the machine's anomaly score. GCNetOmaly was evaluated on real, large-scale data logged by Carbon Black EDR from a large financial organization's automated teller machines (ATMs) as well as communication with Active Directory (AD) servers in two setups: unsupervised and supervised. The results of our evaluation demonstrate GCNetOmaly's effectiveness in detecting anomalous behavior of machines on unsupervised data.
△ Less
Submitted 30 November, 2023;
originally announced November 2023.
-
When does a hyperbola meet its asymptote? Bounded infinities, fictions, and contradictions in Leibniz
Authors:
Mikhail G. Katz,
David Sherry,
Monica Ugaglia
Abstract:
In his 1676 text De Quadratura Arithmetica, Leibniz distinguished infinita terminata from infinita interminata. The text also deals with the notion, originating with Desargues, of the perspective point of intersection at infinite distance for parallel lines. We examine contrasting interpretations of these notions in the context of Leibniz's analysis of asymptotes for logarithmic curves and hyperbo…
▽ More
In his 1676 text De Quadratura Arithmetica, Leibniz distinguished infinita terminata from infinita interminata. The text also deals with the notion, originating with Desargues, of the perspective point of intersection at infinite distance for parallel lines. We examine contrasting interpretations of these notions in the context of Leibniz's analysis of asymptotes for logarithmic curves and hyperbolas. We point out difficulties that arise due to conflating these notions of infinity. As noted by Rodriguez Hurtado et al., a significant difference exists between the Cartesian model of magnitudes and Leibniz's search for a qualitative model for studying perspective, including ideal points at infinity. We show how respecting the distinction between these notions enables a consistent interpretation thereof.
△ Less
Submitted 10 November, 2023;
originally announced November 2023.
-
Peano and Osgood theorems via effective infinitesimals
Authors:
Karel Hrbacek,
Mikhail G. Katz
Abstract:
We provide choiceless proofs using infinitesimals of the global versions of Peano's existence theorem and Osgood's theorem on maximal solutions. We characterize all solutions in terms of infinitesimal perturbations. Our proofs are more effective than traditional non-infinitesimal proofs found in the literature. The background logical structure is the internal set theory SPOT, conservative over ZF.
We provide choiceless proofs using infinitesimals of the global versions of Peano's existence theorem and Osgood's theorem on maximal solutions. We characterize all solutions in terms of infinitesimal perturbations. Our proofs are more effective than traditional non-infinitesimal proofs found in the literature. The background logical structure is the internal set theory SPOT, conservative over ZF.
△ Less
Submitted 30 November, 2023; v1 submitted 2 November, 2023;
originally announced November 2023.
-
Evolution of Leibniz's thought in the matter of fictions and infinitesimals
Authors:
Monica Ugaglia,
Mikhail G. Katz
Abstract:
In this paper we offer a reconstruction of the evolution of Leibniz's thought concerning the problem of the infinite divisibility of bodies, the tension between actuality, unassignability and syncategorematicity, and the closely related question of the possibility of infinitesimal quantities, both in physics and in mathematics.
Some scholars have argued that syncategorematicity is a mature acqui…
▽ More
In this paper we offer a reconstruction of the evolution of Leibniz's thought concerning the problem of the infinite divisibility of bodies, the tension between actuality, unassignability and syncategorematicity, and the closely related question of the possibility of infinitesimal quantities, both in physics and in mathematics.
Some scholars have argued that syncategorematicity is a mature acquisition, to which Leibniz resorts to solve the question of his infinitesimals namely the idea that infinitesimals are just signs for Archimedean exhaustions, and their unassignability is a nominalist maneuver. On the contrary, we show that sycategorematicity, as a traditional idea of classical scholasticism, is a feature of young Leibniz's thinking, from which he moves away in order to solve the same problem, as he gains mathematical knowledge.
We have divided Leibniz's path toward his mature view of infinitesimals into five phases, which are especially significant for reconstructing the entire evolution. In our reconstruction, an important role is played by Leibniz's text De Quadratura Arithmetica. Based on this and other texts we dispute the thesis that fictionality coincides with syncategorematicity, and that unassignability can be bypassed. On the contrary, we maintain that unassignability, as incompatible with the principle of harmony, is the ultimate reason for the fictionality of infinitesimals.
△ Less
Submitted 22 October, 2023;
originally announced October 2023.
-
Recovering contact forms from boundary data
Authors:
Gabriel Katz
Abstract:
Let $X$ be a compact connected smooth manifold with boundary. The paper deals with contact $1$-forms $β$ on $X$, whose Reeb vector fields $v_β$ admit Lyapunov functions $f$. We prove that any odd-dimensional $X$ admits such a contact form.
We tackle the question: how to recover $X$ and $β$ from the appropriate data along the boundary $\partial X$? We describe such boundary data and prove that th…
▽ More
Let $X$ be a compact connected smooth manifold with boundary. The paper deals with contact $1$-forms $β$ on $X$, whose Reeb vector fields $v_β$ admit Lyapunov functions $f$. We prove that any odd-dimensional $X$ admits such a contact form.
We tackle the question: how to recover $X$ and $β$ from the appropriate data along the boundary $\partial X$? We describe such boundary data and prove that they allow for a reconstruction of the pair $(X, β)$, up to a diffeomorphism of $X$. We use the term ``holography" for the reconstruction. We say that objects or structures inside $X$ are {\it holographic}, if they can be reconstructed from their $v_β$-flow induced ``shadows" on the boundary $\partial X$.
We also introduce numerical invariants that measure how ``wrinkled" the boundary $\partial X$ is with respect to the $v_β$-flow and study their holographic properties under the contact forms preserving embeddings of equidimensional contact manifolds with boundary. We get some ``non-squeezing results" about such contact embedding, which are reminiscent of Gromov's non-squeezing theorem in symplectic geometry.
△ Less
Submitted 11 March, 2024; v1 submitted 25 September, 2023;
originally announced September 2023.
-
On Reducing Undesirable Behavior in Deep Reinforcement Learning Models
Authors:
Ophir M. Carmel,
Guy Katz
Abstract:
Deep reinforcement learning (DRL) has proven extremely useful in a large variety of application domains. However, even successful DRL-based software can exhibit highly undesirable behavior. This is due to DRL training being based on maximizing a reward function, which typically captures general trends but cannot precisely capture, or rule out, certain behaviors of the system. In this paper, we pro…
▽ More
Deep reinforcement learning (DRL) has proven extremely useful in a large variety of application domains. However, even successful DRL-based software can exhibit highly undesirable behavior. This is due to DRL training being based on maximizing a reward function, which typically captures general trends but cannot precisely capture, or rule out, certain behaviors of the system. In this paper, we propose a novel framework aimed at drastically reducing the undesirable behavior of DRL-based software, while maintaining its excellent performance. In addition, our framework can assist in providing engineers with a comprehensible characterization of such undesirable behavior. Under the hood, our approach is based on extracting decision tree classifiers from erroneous state-action pairs, and then integrating these trees into the DRL training loop, penalizing the system whenever it performs an error. We provide a proof-of-concept implementation of our approach, and use it to evaluate the technique on three significant case studies. We find that our approach can extend existing frameworks in a straightforward manner, and incurs only a slight overhead in training time. Further, it incurs only a very slight hit to performance, or even in some cases - improves it, while significantly reducing the frequency of undesirable behavior.
△ Less
Submitted 11 September, 2023; v1 submitted 6 September, 2023;
originally announced September 2023.
-
On immersions and embeddings with trivial normal line bundles
Authors:
Gabriel Katz
Abstract:
Let $Z$ be a smooth compact $(n+1)$-manifold. We study smooth embeddings and immersions $β: M \to Z$ of compact or closed $n$-manifolds $M$ such that the normal line bundle $ν^β$ is trivialized. For a fixed $Z$, we introduce an equivalence relation between such $β$'s; it is a crossover between pseudo-isotopies and bordisms. We call this equivalence relation ``{\sf quasitopy}". It comes in two flav…
▽ More
Let $Z$ be a smooth compact $(n+1)$-manifold. We study smooth embeddings and immersions $β: M \to Z$ of compact or closed $n$-manifolds $M$ such that the normal line bundle $ν^β$ is trivialized. For a fixed $Z$, we introduce an equivalence relation between such $β$'s; it is a crossover between pseudo-isotopies and bordisms. We call this equivalence relation ``{\sf quasitopy}". It comes in two flavors: $\mathsf{IMM}(Z)$ and $\mathsf{EMB}(Z)$, based on immersions and embeddings into $Z$, respectively. We prove that the natural map $\mathsf{A}:\mathsf{EMB}(Z) \to \mathsf{IMM}(Z)$ is injective and admits a right inverse $\mathsf{R}:\mathsf{IMM}(Z) \to \mathsf{EMB}(Z)$, induced by the resolution of self-intersections. As a result, we get a map $$\mathcal BΣ:\; \mathsf{IMM}(Z) \big/ \mathsf{A}(\mathsf{EMB}(Z)) \longrightarrow \bigoplus_{k \in [2, n+1]} \mathbf B_{n+1-k}(Z)$$ whose target is a collection of smooth bordism groups of the space $Z$ and which differentiate between immersions and embeddings.
△ Less
Submitted 11 August, 2023;
originally announced August 2023.
-
Formally Explaining Neural Networks within Reactive Systems
Authors:
Shahaf Bassan,
Guy Amir,
Davide Corsi,
Idan Refaeli,
Guy Katz
Abstract:
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 actions. To mitigate this issue, there has been a surge of interest in explainable AI (XAI) techniques, capable of pinpointing the input features that caused the DNN to act as it did. Existing XAI techniques typically f…
▽ More
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 actions. To mitigate this issue, there has been a surge of interest in explainable AI (XAI) techniques, capable of pinpointing the input features that caused the DNN to act as it did. Existing XAI techniques typically face two limitations: (i) they are heuristic, and do not provide formal guarantees that the explanations are correct; and (ii) they often apply to ``one-shot'' systems, where the DNN is invoked independently of past invocations, as opposed to reactive systems. Here, we begin bridging this gap, and propose a formal DNN-verification-based XAI technique for reasoning about multi-step, reactive systems. We suggest methods for efficiently calculating succinct explanations, by exploiting the system's transition constraints in order to curtail the search space explored by the underlying verifier. We evaluate our approach on two popular benchmarks from the domain of automated navigation; and observe that our methods allow the efficient computation of minimal and minimum explanations, significantly outperforming the state of the art. We also demonstrate that our methods produce formal explanations that are more reliable than competing, non-verification-based XAI techniques.
△ Less
Submitted 5 October, 2023; v1 submitted 31 July, 2023;
originally announced August 2023.
-
Towards a Certified Proof Checker for Deep Neural Network Verification
Authors:
Remi Desmartin,
Omri Isac,
Grant Passmore,
Kathrin Stark,
Guy Katz,
Ekaterina Komendantskaya
Abstract:
Recent developments in deep neural networks (DNNs) have led to their adoption in safety-critical systems, which in turn has heightened the need for guaranteeing their safety. These safety properties of DNNs can be proven using tools developed by the verification community. However, these tools are themselves prone to implementation bugs and numerical stability problems, which make their reliabilit…
▽ More
Recent developments in deep neural networks (DNNs) have led to their adoption in safety-critical systems, which in turn has heightened the need for guaranteeing their safety. These safety properties of DNNs can be proven using tools developed by the verification community. However, these tools are themselves prone to implementation bugs and numerical stability problems, which make their reliability questionable. To overcome this, some verifiers produce proofs of their results which can be checked by a trusted checker. In this work, we present a novel implementation of a proof checker for DNN verification. It improves on existing implementations by offering numerical stability and greater verifiability. To achieve this, we leverage two key capabilities of Imandra, an industrial theorem prover: its support of infinite precision real arithmetic and its formal verification infrastructure. So far, we have implemented a proof checker in Imandra, specified its correctness properties and started to verify the checker's compliance with them. Our ongoing work focuses on completing the formal verification of the checker and further optimizing its performance.
△ Less
Submitted 13 February, 2024; v1 submitted 12 July, 2023;
originally announced July 2023.
-
Doodles and blobs on a lined page: convex quasi-envelops of traversing flows on surfaces
Authors:
Gabriel Katz
Abstract:
Let $A$ denote the cylinder $\mathbb R \times S^1$ or the band $\mathbb R \times I$, where $I$ stands for the closed interval. We consider $2$-{\sf moderate immersions} of closed curves (``{\sf doodles}") and compact surfaces (``{\sf blobs}") in $A$, up to cobordisms that also are $2$-moderate immersions in $A \times [0, 1]$ of surfaces and solids. By definition, the $2$-moderate immersions of cur…
▽ More
Let $A$ denote the cylinder $\mathbb R \times S^1$ or the band $\mathbb R \times I$, where $I$ stands for the closed interval. We consider $2$-{\sf moderate immersions} of closed curves (``{\sf doodles}") and compact surfaces (``{\sf blobs}") in $A$, up to cobordisms that also are $2$-moderate immersions in $A \times [0, 1]$ of surfaces and solids. By definition, the $2$-moderate immersions of curves and surfaces do not have tangencies of order $\geq 3$ to the fibers of the obvious projections $A \to S^1$,\; $A \times [0, 1] \to S^1 \times [0, 1]$ or $A \to I$,\; $A \times [0, 1] \to I \times [0, 1]$. These bordisms come in different flavors: in particular, we consider one flavor based on {\sf regular embeddings} of doodles and blobs in $A$. We compute the bordisms of regular embeddings and construct many invariants that distinguish between the bordisms of immersions and embeddings. In the case of oriented doodles on $A= \mathbb R \times I$, our computations of $2$-moderate immersion bordisms $\mathbf{OC}^{\mathsf{imm}}_{\mathsf{moderate \leq 2}}(A)$ are near complete: we show that they can be described by an exact sequence of abelian groups $$0 \to \mathbf K \to \mathbf{OC}^{\mathsf{imm}}_{\mathsf{moderate \leq 2}}(A)\big/\mathbf{OC}^{\mathsf{emb}}_{\mathsf{moderate \leq 2}}(A) \stackrel{\mathcal I ρ}{\longrightarrow} \mathbb Z \times \mathbb Z \to 0,$$ where $\mathbf{OC}^{\mathsf{emb}}_{\mathsf{moderate \leq 2}}(A) \approx \mathbb Z \times \mathbb Z$, the epimorphism $\mathcal I ρ$ counts different types of crossings of immersed doodles, and the kernel $\mathbf K$ contains the group $(\mathbb Z)^\infty$ whose generators are described explicitly.
△ Less
Submitted 5 February, 2024; v1 submitted 4 July, 2023;
originally announced July 2023.
-
DelBugV: Delta-Debugging Neural Network Verifiers
Authors:
Raya Elsaleh,
Guy Katz
Abstract:
Deep neural networks (DNNs) are becoming a key component in diverse systems across the board. However, despite their success, they often err miserably; and this has triggered significant interest in formally verifying them. Unfortunately, DNN verifiers are intricate tools, and are themselves susceptible to soundness bugs. Due to the complexity of DNN verifiers, as well as the sizes of the DNNs bei…
▽ More
Deep neural networks (DNNs) are becoming a key component in diverse systems across the board. However, despite their success, they often err miserably; and this has triggered significant interest in formally verifying them. Unfortunately, DNN verifiers are intricate tools, and are themselves susceptible to soundness bugs. Due to the complexity of DNN verifiers, as well as the sizes of the DNNs being verified, debugging such errors is a daunting task. Here, we present a novel tool, named DelBugV, that uses automated delta debugging techniques on DNN verifiers. Given a malfunctioning DNN verifier and a correct verifier as a point of reference (or, in some cases, just a single, malfunctioning verifier), DelBugV can produce much simpler DNN verification instances that still trigger undesired behavior -- greatly facilitating the task of debugging the faulty verifier. Our tool is modular and extensible, and can easily be enhanced with additional network simplification methods and strategies. For evaluation purposes, we ran DelBugV on 4 DNN verification engines, which were observed to produce incorrect results at the 2021 neural network verification competition (VNN-COMP'21). We were able to simplify many of the verification queries that trigger these faulty behaviors, by as much as 99%. We regard our work as a step towards the ultimate goal of producing reliable and trustworthy DNN-based software.
△ Less
Submitted 29 May, 2023;
originally announced May 2023.
-
Effective infinitesimals in R
Authors:
Karel Hrbacek,
Mikhail G. Katz
Abstract:
We survey the effective foundations for analysis with infinitesimals developed by Hrbacek and Katz in 2021, and detail some applications. Theories SPOT and SCOT are conservative over respectively ZF and ZF+ADC. The range of applications of these theories illustrates the fact that analysis with infinitesimals requires no more choice than traditional analysis. The theory SCOT incorporates in particu…
▽ More
We survey the effective foundations for analysis with infinitesimals developed by Hrbacek and Katz in 2021, and detail some applications. Theories SPOT and SCOT are conservative over respectively ZF and ZF+ADC. The range of applications of these theories illustrates the fact that analysis with infinitesimals requires no more choice than traditional analysis. The theory SCOT incorporates in particular all the axioms of Nelson's Radically Elementary Probability Theory, which is therefore conservative over ZF+ADC.
△ Less
Submitted 23 May, 2023; v1 submitted 8 May, 2023;
originally announced May 2023.
-
ReMark: Receptive Field based Spatial WaterMark Embedding Optimization using Deep Network
Authors:
Natan Semyonov,
Rami Puzis,
Asaf Shabtai,
Gilad Katz
Abstract:
Watermarking is one of the most important copyright protection tools for digital media. The most challenging type of watermarking is the imperceptible one, which embeds identifying information in the data while retaining the latter's original quality. To fulfill its purpose, watermarks need to withstand various distortions whose goal is to damage their integrity. In this study, we investigate a no…
▽ More
Watermarking is one of the most important copyright protection tools for digital media. The most challenging type of watermarking is the imperceptible one, which embeds identifying information in the data while retaining the latter's original quality. To fulfill its purpose, watermarks need to withstand various distortions whose goal is to damage their integrity. In this study, we investigate a novel deep learning-based architecture for embedding imperceptible watermarks. The key insight guiding our architecture design is the need to correlate the dimensions of our watermarks with the sizes of receptive fields (RF) of modules of our architecture. This adaptation makes our watermarks more robust, while also enabling us to generate them in a way that better maintains image quality. Extensive evaluations on a wide variety of distortions show that the proposed method is robust against most common distortions on watermarks including collusive distortion.
△ Less
Submitted 11 May, 2023;
originally announced May 2023.
-
DNN Verification, Reachability, and the Exponential Function Problem
Authors:
Omri Isac,
Yoni Zohar,
Clark Barrett,
Guy Katz
Abstract:
Deep neural networks (DNNs) are increasingly being deployed to perform safety-critical tasks. The opacity of DNNs, which prevents humans from reasoning about them, presents new safety and security challenges. To address these challenges, the verification community has begun develo** techniques for rigorously analyzing DNNs, with numerous verification algorithms proposed in recent years. While a…
▽ More
Deep neural networks (DNNs) are increasingly being deployed to perform safety-critical tasks. The opacity of DNNs, which prevents humans from reasoning about them, presents new safety and security challenges. To address these challenges, the verification community has begun develo** techniques for rigorously analyzing DNNs, with numerous verification algorithms proposed in recent years. While a significant amount of work has gone into develo** these verification algorithms, little work has been devoted to rigorously studying the computability and complexity of the underlying theoretical problems. Here, we seek to contribute to the bridging of this gap. We focus on two kinds of DNNs: those that employ piecewise-linear activation functions (e.g., ReLU), and those that employ piecewise-smooth activation functions (e.g., Sigmoids). We prove the two following theorems: 1) The decidability of verifying DNNs with a particular set of piecewise-smooth activation functions is equivalent to a well-known, open problem formulated by Tarski; and 2) The DNN verification problem for any quantifier-free linear arithmetic specification can be reduced to the DNN reachability problem, whose approximation is NP-complete. These results answer two fundamental questions about the computability and complexity of DNN verification, and the ways it is affected by the network's activation functions and error tolerance; and could help guide future efforts in develo** DNN verification tools.
△ Less
Submitted 10 July, 2023; v1 submitted 10 May, 2023;
originally announced May 2023.
-
Verifying Generalization in Deep Learning
Authors:
Guy Amir,
Osher Maayan,
Tom Zelazny,
Guy Katz,
Michael Schapira
Abstract:
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 notoriously prone to poor generalization, i.e., may prove inadequate on inputs not encountered during training. This limitation poses a significant obstacle to employing deep learning for mission-critical tasks, and also in r…
▽ More
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 notoriously prone to poor generalization, i.e., may prove inadequate on inputs not encountered during training. This limitation poses a significant obstacle to employing deep learning for mission-critical tasks, and also in real-world environments that exhibit high variability. We propose a novel, verification-driven methodology for identifying DNN-based decision rules that generalize well to new input domains. Our approach quantifies generalization to an input domain by the extent to which decisions reached by independently trained DNNs are in agreement for inputs in this domain. We show how, by harnessing the power of DNN verification, our approach can be efficiently and effectively realized. We evaluate our verification-based approach on three deep reinforcement learning (DRL) benchmarks, including a system for Internet congestion control. Our results establish the usefulness of our approach. More broadly, our work puts forth a novel objective for formal verification, with the potential for mitigating the risks associated with deploying DNN-based systems in the wild.
△ Less
Submitted 9 May, 2023; v1 submitted 11 February, 2023;
originally announced February 2023.
-
Algebras of smooth functions and holography of traversing flows
Authors:
Gabriel Katz
Abstract:
Let $X$ be a smooth compact manifold and $v$ a vector field on $X$ which admits a smooth function $f: X \to \mathbf R$ such that $df(v) > 0$. Let $\partial X$ be the boundary of $X$. We denote by $C^\infty(X)$ the algebra of smooth functions on $X$ and by $C^\infty(\partial X)$ the algebra of smooth functions on $\partial X$. With the help of $(v, f)$, we introduce two subalgebras $\mathcal A(v)$…
▽ More
Let $X$ be a smooth compact manifold and $v$ a vector field on $X$ which admits a smooth function $f: X \to \mathbf R$ such that $df(v) > 0$. Let $\partial X$ be the boundary of $X$. We denote by $C^\infty(X)$ the algebra of smooth functions on $X$ and by $C^\infty(\partial X)$ the algebra of smooth functions on $\partial X$. With the help of $(v, f)$, we introduce two subalgebras $\mathcal A(v)$ and $\mathcal B(f)$ of $C^\infty(\partial X)$ and prove (under mild hypotheses) that $C^\infty(X) \approx \mathcal A(v) \hat\otimes \mathcal B(f)$, the topological tensor product. Thus the topological algebras $\mathcal A(v)$ and $\mathcal B(f)$, \emph{viewed as boundary data}, allow for a reconstruction of $C^\infty(X)$. As a result, $\mathcal A(v)$ and $\mathcal B(f)$ allow for the recovery of the smooth topological type of the bulk $X$.
△ Less
Submitted 1 March, 2023; v1 submitted 10 February, 2023;
originally announced February 2023.
-
Extremal spherical polytopes and Borsuk's conjecture
Authors:
Mikhail Katz,
Facundo Mémoli,
Qingsong Wang
Abstract:
We generate anti-self-polar polytopes via a numerical implementation of the gradient flow induced by the diameter functional on the space of all finite subsets of the sphere, and prove related results on the critical points of the diameter functional as well as results about the combinatorics of such polytopes. We also discuss potential connections to Borsuk's conjecture.
We generate anti-self-polar polytopes via a numerical implementation of the gradient flow induced by the diameter functional on the space of all finite subsets of the sphere, and prove related results on the critical points of the diameter functional as well as results about the combinatorics of such polytopes. We also discuss potential connections to Borsuk's conjecture.
△ Less
Submitted 2 February, 2023; v1 submitted 30 January, 2023;
originally announced January 2023.
-
OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks
Authors:
Xingwu Guo,
Ziwei Zhou,
Yueling Zhang,
Guy Katz,
Min Zhang
Abstract:
Occlusion is a prevalent and easily realizable semantic perturbation to deep neural networks (DNNs). It can fool a DNN into misclassifying an input image by occluding some segments, possibly resulting in severe errors. Therefore, DNNs planted in safety-critical systems should be verified to be robust against occlusions prior to deployment. However, most existing robustness verification approaches…
▽ More
Occlusion is a prevalent and easily realizable semantic perturbation to deep neural networks (DNNs). It can fool a DNN into misclassifying an input image by occluding some segments, possibly resulting in severe errors. Therefore, DNNs planted in safety-critical systems should be verified to be robust against occlusions prior to deployment. However, most existing robustness verification approaches for DNNs are focused on non-semantic perturbations and are not suited to the occlusion case. In this paper, we propose the first efficient, SMT-based approach for formally verifying the occlusion robustness of DNNs. We formulate the occlusion robustness verification problem and prove it is NP-complete. Then, we devise a novel approach for encoding occlusions as a part of neural networks and introduce two acceleration techniques so that the extended neural networks can be efficiently verified using off-the-shelf, SMT-based neural network verification tools. We implement our approach in a prototype called OccRob and extensively evaluate its performance on benchmark datasets with various occlusion variants. The experimental results demonstrate our approach's effectiveness and efficiency in verifying DNNs' robustness against various occlusions, and its ability to generate counterexamples when these DNNs are not robust.
△ Less
Submitted 27 January, 2023;
originally announced January 2023.
-
Enhancing Deep Learning with Scenario-Based Override Rules: a Case Study
Authors:
Adiel Ashrov,
Guy Katz
Abstract:
Deep neural networks (DNNs) have become a crucial instrument in the software development toolkit, due to their ability to efficiently solve complex problems. Nevertheless, DNNs are highly opaque, and can behave in an unexpected manner when they encounter unfamiliar input. One promising approach for addressing this challenge is by extending DNN-based systems with hand-crafted override rules, which…
▽ More
Deep neural networks (DNNs) have become a crucial instrument in the software development toolkit, due to their ability to efficiently solve complex problems. Nevertheless, DNNs are highly opaque, and can behave in an unexpected manner when they encounter unfamiliar input. One promising approach for addressing this challenge is by extending DNN-based systems with hand-crafted override rules, which override the DNN's output when certain conditions are met. Here, we advocate crafting such override rules using the well-studied scenario-based modeling paradigm, which produces rules that are simple, extensible, and powerful enough to ensure the safety of the DNN, while also rendering the system more translucent. We report on two extensive case studies, which demonstrate the feasibility of the approach; and through them, propose an extension to scenario-based modeling, which facilitates its integration with DNN components. We regard this work as a step towards creating safer and more reliable DNN-based systems and models.
△ Less
Submitted 19 January, 2023;
originally announced January 2023.
-
gRoMA: a Tool for Measuring the Global Robustness of Deep Neural Networks
Authors:
Natan Levy,
Raz Yerushalmi,
Guy Katz
Abstract:
Deep neural networks (DNNs) are at the forefront of cutting-edge technology, and have been achieving remarkable performance in a variety of complex tasks. Nevertheless, their integration into safety-critical systems, such as in the aerospace or automotive domains, poses a significant challenge due to the threat of adversarial inputs: perturbations in inputs that might cause the DNN to make grievou…
▽ More
Deep neural networks (DNNs) are at the forefront of cutting-edge technology, and have been achieving remarkable performance in a variety of complex tasks. Nevertheless, their integration into safety-critical systems, such as in the aerospace or automotive domains, poses a significant challenge due to the threat of adversarial inputs: perturbations in inputs that might cause the DNN to make grievous mistakes. Multiple studies have demonstrated that even modern DNNs are susceptible to adversarial inputs, and this risk must thus be measured and mitigated to allow the deployment of DNNs in critical settings. Here, we present gRoMA (global Robustness Measurement and Assessment), an innovative and scalable tool that implements a probabilistic approach to measure the global categorial robustness of a DNN. Specifically, gRoMA measures the probability of encountering adversarial inputs for a specific output category. Our tool operates on pre-trained, black-box classification DNNs, and generates input samples belonging to an output category of interest. It measures the DNN's susceptibility to adversarial inputs around these inputs, and aggregates the results to infer the overall global categorial robustness of the DNN up to some small bounded statistical error.
We evaluate our tool on the popular Densenet DNN model over the CIFAR10 dataset. Our results reveal significant gaps in the robustness of the different output categories. This experiment demonstrates the usefulness and scalability of our approach and its potential for allowing DNNs to be deployed within critical systems of interest.
△ Less
Submitted 28 December, 2023; v1 submitted 5 January, 2023;
originally announced January 2023.
-
Constructing nonstandard hulls and Loeb measures in internal set theories
Authors:
Karel Hrbacek,
Mikhail G. Katz
Abstract:
Currently the two popular ways to practice Robinson's nonstandard analysis are the model-theoretic approach and the axiomatic/syntactic approach. It is sometimes claimed that the internal axiomatic approach is unable to handle constructions relying on external sets. We show that internal frameworks provide successful accounts of nonstandard hulls and Loeb measures. The basic fact this work relies…
▽ More
Currently the two popular ways to practice Robinson's nonstandard analysis are the model-theoretic approach and the axiomatic/syntactic approach. It is sometimes claimed that the internal axiomatic approach is unable to handle constructions relying on external sets. We show that internal frameworks provide successful accounts of nonstandard hulls and Loeb measures. The basic fact this work relies on is that the ultrapower of the standard universe by a standard ultrafilter is naturally isomorphic to a subuniverse of the internal universe.
△ Less
Submitted 1 January, 2023;
originally announced January 2023.
-
Is pluralism in the history of mathematics possible?
Authors:
Jacques Bair,
Alexandre Borovik,
Vladimir Kanovei,
Mikhail G. Katz,
Semen S. Kutateladze,
Sam Sanders,
David Sherry,
Monica Ugaglia,
Mark van Atten
Abstract:
Leibniz scholarship is currently an area of lively debate. We respond to some recent criticisms by Archibald et al.
Leibniz scholarship is currently an area of lively debate. We respond to some recent criticisms by Archibald et al.
△ Less
Submitted 22 March, 2023; v1 submitted 15 December, 2022;
originally announced December 2022.
-
veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System
Authors:
Guy Amir,
Ziv Freund,
Guy Katz,
Elad Mandelbaum,
Idan Refaeli
Abstract:
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 reliability of a real-world, safety-critical system. The system we target is an airborne platform for wildfire detection, which incorporates two deep neural networks. We describe the system and its properties of interest, and disc…
▽ More
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 reliability of a real-world, safety-critical system. The system we target is an airborne platform for wildfire detection, which incorporates two deep neural networks. We describe the system and its properties of interest, and discuss our attempts to verify the system's consistency, i.e., its ability to continue and correctly classify a given input, even if the wildfire it describes increases in intensity. We regard this work as a step towards the incorporation of academic-oriented verification tools into real-world systems of interest.
△ Less
Submitted 6 December, 2022;
originally announced December 2022.
-
Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
Authors:
Jiaxu Tian,
Dapeng Zhi,
Si Liu,
Peixin Wang,
Guy Katz,
Min Zhang
Abstract:
The intrinsic complexity of deep neural networks (DNNs) makes it challenging to verify not only the networks themselves but also the hosting DNN-controlled systems. Reachability analysis of these systems faces the same challenge. Existing approaches rely on over-approximating DNNs using simpler polynomial models. However, they suffer from low efficiency and large overestimation, and are restricted…
▽ More
The intrinsic complexity of deep neural networks (DNNs) makes it challenging to verify not only the networks themselves but also the hosting DNN-controlled systems. Reachability analysis of these systems faces the same challenge. Existing approaches rely on over-approximating DNNs using simpler polynomial models. However, they suffer from low efficiency and large overestimation, and are restricted to specific types of DNNs. This paper presents a novel abstraction-based approach to bypass the crux of over-approximating DNNs in reachability analysis. Specifically, we extend conventional DNNs by inserting an additional abstraction layer, which abstracts a real number to an interval for training. The inserted abstraction layer ensures that the values represented by an interval are indistinguishable to the network for both training and decision-making. Leveraging this, we devise the first black-box reachability analysis approach for DNN-controlled systems, where trained DNNs are only queried as black-box oracles for the actions on abstract states. Our approach is sound, tight, efficient, and agnostic to any DNN type and size. The experimental results on a wide range of benchmarks show that the DNNs trained by using our approach exhibit comparable performance, while the reachability analysis of the corresponding systems becomes more amenable with significant tightness and efficiency improvement over the state-of-the-art white-box approaches.
△ Less
Submitted 31 October, 2023; v1 submitted 20 November, 2022;
originally announced November 2022.
-
Efficiently Finding Adversarial Examples with DNN Preprocessing
Authors:
Avriti Chauhan,
Mohammad Afzal,
Hrishikesh Karmarkar,
Yizhak Elboher,
Kumar Madhukar,
Guy Katz
Abstract:
Deep Neural Networks (DNNs) are everywhere, frequently performing a fairly complex task that used to be unimaginable for machines to carry out. In doing so, they do a lot of decision making which, depending on the application, may be disastrous if gone wrong. This necessitates a formal argument that the underlying neural networks satisfy certain desirable properties. Robustness is one such key pro…
▽ More
Deep Neural Networks (DNNs) are everywhere, frequently performing a fairly complex task that used to be unimaginable for machines to carry out. In doing so, they do a lot of decision making which, depending on the application, may be disastrous if gone wrong. This necessitates a formal argument that the underlying neural networks satisfy certain desirable properties. Robustness is one such key property for DNNs, particularly if they are being deployed in safety or business critical applications. Informally speaking, a DNN is not robust if very small changes to its input may affect the output in a considerable way (e.g. changes the classification for that input). The task of finding an adversarial example is to demonstrate this lack of robustness, whenever applicable. While this is doable with the help of constrained optimization techniques, scalability becomes a challenge due to large-sized networks. This paper proposes the use of information gathered by preprocessing the DNN to heavily simplify the optimization problem. Our experiments substantiate that this is effective, and does significantly better than the state-of-the-art.
△ Less
Submitted 16 November, 2022;
originally announced November 2022.
-
NeuroCERIL: Robotic Imitation Learning via Hierarchical Cause-Effect Reasoning in Programmable Attractor Neural Networks
Authors:
Gregory P. Davis,
Garrett E. Katz,
Rodolphe J. Gentili,
James A. Reggia
Abstract:
Imitation learning allows social robots to learn new skills from human teachers without substantial manual programming, but it is difficult for robotic imitation learning systems to generalize demonstrated skills as well as human learners do. Contemporary neurocomputational approaches to imitation learning achieve limited generalization at the cost of data-intensive training, and often produce opa…
▽ More
Imitation learning allows social robots to learn new skills from human teachers without substantial manual programming, but it is difficult for robotic imitation learning systems to generalize demonstrated skills as well as human learners do. Contemporary neurocomputational approaches to imitation learning achieve limited generalization at the cost of data-intensive training, and often produce opaque models that are difficult to understand and debug. In this study, we explore the viability of develo** purely-neural controllers for social robots that learn to imitate by reasoning about the underlying intentions of demonstrated behaviors. We present NeuroCERIL, a brain-inspired neurocognitive architecture that uses a novel hypothetico-deductive reasoning procedure to produce generalizable and human-readable explanations for demonstrated behavior. This approach combines bottom-up abductive inference with top-down predictive verification, and captures important aspects of human causal reasoning that are relevant to a broad range of cognitive domains. Our empirical results demonstrate that NeuroCERIL can learn various procedural skills in a simulated robotic imitation learning domain. We also show that its causal reasoning procedure is computationally efficient, and that its memory use is dominated by highly transient short-term memories, much like human working memory. We conclude that NeuroCERIL is a viable neural model of human-like imitation learning that can improve human-robot collaboration and contribute to investigations of the neurocomputational basis of human cognition.
△ Less
Submitted 11 November, 2022;
originally announced November 2022.
-
Historical infinitesimalists and modern historiography of infinitesimals
Authors:
Jacques Bair,
Alexandre Borovik,
Vladimir Kanovei,
Mikhail G. Katz,
Semen Kutateladze,
Sam Sanders,
David Sherry,
Monica Ugaglia
Abstract:
In the history of infinitesimal calculus, we trace innovation from Leibniz to Cauchy and reaction from Berkeley to Mansion and beyond. We explore 19th century infinitesimal lores, including the approaches of Simeon-Denis Poisson, Gaspard-Gustave de Coriolis, and Jean-Nicolas Noel. We examine contrasting historiographic approaches to such lores, in the work of Laugwitz, Schubring, Spalt, and others…
▽ More
In the history of infinitesimal calculus, we trace innovation from Leibniz to Cauchy and reaction from Berkeley to Mansion and beyond. We explore 19th century infinitesimal lores, including the approaches of Simeon-Denis Poisson, Gaspard-Gustave de Coriolis, and Jean-Nicolas Noel. We examine contrasting historiographic approaches to such lores, in the work of Laugwitz, Schubring, Spalt, and others, and address a recent critique by Archibald et al. We argue that the element of contingency in this history is more prominent than many modern historians seem willing to acknowledge.
△ Less
Submitted 14 March, 2023; v1 submitted 26 October, 2022;
originally announced October 2022.
-
Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks
Authors:
Shahaf Bassan,
Guy Katz
Abstract:
With the rapid growth of machine learning, deep neural networks (DNNs) are now being used in numerous domains. Unfortunately, DNNs are "black-boxes", and cannot be interpreted by humans, which is a substantial concern in safety-critical systems. To mitigate this issue, researchers have begun working on explainable AI (XAI) methods, which can identify a subset of input features that are the cause o…
▽ More
With the rapid growth of machine learning, deep neural networks (DNNs) are now being used in numerous domains. Unfortunately, DNNs are "black-boxes", and cannot be interpreted by humans, which is a substantial concern in safety-critical systems. To mitigate this issue, researchers have begun working on explainable AI (XAI) methods, which can identify a subset of input features that are the cause of a DNN's decision for a given input. Most existing techniques are heuristic, and cannot guarantee the correctness of the explanation provided. In contrast, recent and exciting attempts have shown that formal methods can be used to generate provably correct explanations. Although these methods are sound, the computational complexity of the underlying verification problem limits their scalability; and the explanations they produce might sometimes be overly complex. Here, we propose a novel approach to tackle these limitations. We (1) suggest an efficient, verification-based method for finding minimal explanations, which constitute a provable approximation of the global, minimum explanation; (2) show how DNN verification can assist in calculating lower and upper bounds on the optimal explanation; (3) propose heuristics that significantly improve the scalability of the verification process; and (4) suggest the use of bundles, which allows us to arrive at more succinct and interpretable explanations. Our evaluation shows that our approach significantly outperforms state-of-the-art techniques, and produces explanations that are more useful to humans. We thus regard this work as a step toward leveraging verification technology in producing DNNs that are more reliable and comprehensible.
△ Less
Submitted 9 February, 2023; v1 submitted 25 October, 2022;
originally announced October 2022.
-
Tighter Abstract Queries in Neural Network Verification
Authors:
Elazar Cohen,
Yizhak Yisrael Elboher,
Clark Barrett,
Guy Katz
Abstract:
Neural networks have become critical components of reactive systems in various domains within computer science. Despite their excellent performance, using neural networks entails numerous risks that stem from our lack of ability to understand and reason about their behavior. Due to these risks, various formal methods have been proposed for verifying neural networks; but unfortunately, these typica…
▽ More
Neural networks have become critical components of reactive systems in various domains within computer science. Despite their excellent performance, using neural networks entails numerous risks that stem from our lack of ability to understand and reason about their behavior. Due to these risks, various formal methods have been proposed for verifying neural networks; but unfortunately, these typically struggle with scalability barriers. Recent attempts have demonstrated that abstraction-refinement approaches could play a significant role in mitigating these limitations; but these approaches can often produce networks that are so abstract, that they become unsuitable for verification. To deal with this issue, we present CEGARETTE, a novel verification mechanism where both the system and the property are abstracted and refined simultaneously. We observe that this approach allows us to produce abstract networks which are both small and sufficiently accurate, allowing for quick verification times while avoiding a large number of refinement steps. For evaluation purposes, we implemented CEGARETTE as an extension to the recently proposed CEGAR-NN framework. Our results are very promising, and demonstrate a significant improvement in performance over multiple benchmarks.
△ Less
Submitted 14 May, 2023; v1 submitted 23 October, 2022;
originally announced October 2022.
-
A Transferable and Automatic Tuning of Deep Reinforcement Learning for Cost Effective Phishing Detection
Authors:
Orel Lavie,
Asaf Shabtai,
Gilad Katz
Abstract:
Many challenging real-world problems require the deployment of ensembles multiple complementary learning models to reach acceptable performance levels. While effective, applying the entire ensemble to every sample is costly and often unnecessary. Deep Reinforcement Learning (DRL) offers a cost-effective alternative, where detectors are dynamically chosen based on the output of their predecessors,…
▽ More
Many challenging real-world problems require the deployment of ensembles multiple complementary learning models to reach acceptable performance levels. While effective, applying the entire ensemble to every sample is costly and often unnecessary. Deep Reinforcement Learning (DRL) offers a cost-effective alternative, where detectors are dynamically chosen based on the output of their predecessors, with their usefulness weighted against their computational cost. Despite their potential, DRL-based solutions are not widely used in this capacity, partly due to the difficulties in configuring the reward function for each new task, the unpredictable reactions of the DRL agent to changes in the data, and the inability to use common performance metrics (e.g., TPR/FPR) to guide the algorithm's performance. In this study we propose methods for fine-tuning and calibrating DRL-based policies so that they can meet multiple performance goals. Moreover, we present a method for transferring effective security policies from one dataset to another. Finally, we demonstrate that our approach is highly robust against adversarial attacks.
△ Less
Submitted 19 September, 2022;
originally announced September 2022.