Showing 1–50 of 243 results for author: Katz, G

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.

Comments: 8 pages. To appear in Proceedings of the American Mathematical Society

MSC Class: 53C45

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.

Comments: Accepted in the 1st Reinforcement Learning Conference (RLC), 2024. [Corsi and Amir contributed equally]

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.

Comments: To appear in ICML 2024 (Spotlight)

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.

Comments: To appear in the Journal of Automated Reasoning (JAR), 2024. This is an extended version of a CAV 2023 paper, titled: "Verifying Generalization in Deep Learning"

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.

Comments: 6 pages, to appear in Open Mathematics

MSC Class: 53C35; 53C20

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.

Comments: Paper do not ready

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.

Comments: 10 pages. To appear in Journal of Geometric Analysis

MSC Class: Primary 53C20; Secondary 53C23

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.

Comments: 32 pages

MSC Class: 01A60; 01A61

Journal ref: Antiquitates Mathematicae 17 (2023), 29-65

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.

Comments: This is a preprint version of the paper in the proceedings of 43rd Digital Avionics Systems Conference (DASC)

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.

Comments: Condensed version accepted at CAV'24

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.

Comments: This is a preprint version of a paper that will appear at 43rd Digital Avionics Systems Conference (DASC 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.

Comments: This is a preprint version of a paper that will appear at Modelsward 2024

MSC Class: 68N19

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.

Comments: 19 pages

MSC Class: 01A45

Journal ref: REVISTA LATINOAMERICANA de FILOSOF\'\IA 49 (2023), no. 2, 241-258

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.

Comments: 19 pages, Journal of Logic and Analysis

MSC Class: 26E35; 34A12

Journal ref: Journal of Logic and Analysis 15:6 (2023), 1-19

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.

Comments: 36 pages

MSC Class: 01A45

Journal ref: B. Sriraman (ed.), Handbook of the History and Philosophy of Mathematical Practice, Springer, 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.

Comments: 47 pages, 3 figures

MSC Class: 53D10; 53D12

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.

Comments: 8 pages, 2 figures

MSC Class: 57R42; 57R90

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.

Comments: To appear in Proc. 23rd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD)

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.

Comments: This is a preprint version of the paper that appeared at LOPSTR 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.

Comments: 42 pages, 12 figures

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.

Comments: 15 pages, to appear in Real Analysis Exchange

MSC Class: 26E35; 03A05; 03C25; 03C62; 03E70; 03H05

Journal ref: Real Analysis Exchange 48 (2023), no. 2, 365-380

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.

Comments: This is a preprint version of the paper that appears at CONCUR 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.

Comments: To appear in Proc. 35th Int. Conf. on Computer Aided Verification (CAV)

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.

Comments: Updated funding information

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.

Comments: A preprint of a paper with the same title, to appear at MODELSWARD 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.

Comments: 4 pages, 1 figure

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.

Comments: 34 pages, to appear in Bulletin of Symbolic Logic

MSC Class: 26E35

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.

Comments: 2 pages, appeared in The Mathematical Intelligencer

MSC Class: 01A45; 01A85

Journal ref: The Mathematical Intelligencer 45 (2023), no. 1, 8

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.

Comments: To appear in Proceedings of the 25th International Symposium on Formal Methods (FM)

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.

Comments: 60 pages

MSC Class: 01A45; 01A61; 01A85; 01A90; 26E35

Journal ref: Antiquitates Mathematicae 16 (2022), 189-257

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.

Comments: To appear in Proc. 29th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)

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.