-
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.
-
Product Line Management with Graphical MBSE Views
Authors:
Pascal Krapf,
Sébastien Berthier,
Nicole Levy
Abstract:
Reducing the cost and delay and improving quality are major issues for product and software development, especially in the automotive domain. Product line engineering is a wellknown approach to engineer systems with the aim to reduce costs and development time as well as to improve the product quality. Feature models enable to make logical selection of features and obtain a filtered set of assets…
▽ More
Reducing the cost and delay and improving quality are major issues for product and software development, especially in the automotive domain. Product line engineering is a wellknown approach to engineer systems with the aim to reduce costs and development time as well as to improve the product quality. Feature models enable to make logical selection of features and obtain a filtered set of assets that compose the product. We propose to use a color code in feature models to make possible decisions visual in the feature tree. The color code is explained and its use is illustrated. The completeness of the approach is discussed.
△ Less
Submitted 31 October, 2023;
originally announced October 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.
-
Management and Detection System for Medical Surgical Equipment
Authors:
Alexandra Hadar,
Natan Levy,
Michael Winokur
Abstract:
Retained surgical bodies (RSB) are any foreign bodies left inside the patient after a medical procedure. RSB is often caused by human mistakes or miscommunication between medical staff during the procedure. Infection, medical complications, and even death are possible consequences of RSB, and it is a significant risk for patients, hospitals, and surgical staff. In this paper. we describe the engin…
▽ More
Retained surgical bodies (RSB) are any foreign bodies left inside the patient after a medical procedure. RSB is often caused by human mistakes or miscommunication between medical staff during the procedure. Infection, medical complications, and even death are possible consequences of RSB, and it is a significant risk for patients, hospitals, and surgical staff. In this paper. we describe the engineering process we have done to explore the design space, define a feasible solution, and simulate, verify, and validate a state-of-the-art Cyber-Physical System that can significantly decrease the incidence of RSB and thus increase patients' survivability rate. This system might save patients' suffering and lives and reduce medical staff negligence lawsuits while improving the hospital's reputation. The paper illustrates each step of the process with examples and describes the chosen solution in detail.
△ Less
Submitted 4 November, 2022;
originally announced November 2022.
-
PyBryt: auto-assessment and auto-grading for computational thinking
Authors:
Christopher Pyles,
Francois van Schalkwyk,
Gerard J. Gorman,
Marijan Beg,
Lee Stott,
Nir Levy,
Ran Gilad-Bachrach
Abstract:
We continuously interact with computerized systems to achieve goals and perform tasks in our personal and professional lives. Therefore, the ability to program such systems is a skill needed by everyone. Consequently, computational thinking skills are essential for everyone, which creates a challenge for the educational system to teach these skills at scale and allow students to practice these ski…
▽ More
We continuously interact with computerized systems to achieve goals and perform tasks in our personal and professional lives. Therefore, the ability to program such systems is a skill needed by everyone. Consequently, computational thinking skills are essential for everyone, which creates a challenge for the educational system to teach these skills at scale and allow students to practice these skills. To address this challenge, we present a novel approach to providing formative feedback to students on programming assignments. Our approach uses dynamic evaluation to trace intermediate results generated by student's code and compares them to the reference implementation provided by their teachers. We have implemented this method as a Python library and demonstrate its use to give students relevant feedback on their work while allowing teachers to challenge their students' computational thinking skills.
△ Less
Submitted 3 December, 2021;
originally announced December 2021.
-
RoMA: a Method for Neural Network Robustness Measurement and Assessment
Authors:
Natan Levy,
Guy Katz
Abstract:
Neural network models have become the leading solution for a large variety of tasks, such as classification, language processing, protein folding, and others. However, their reliability is heavily plagued by adversarial inputs: small input perturbations that cause the model to produce erroneous outputs. Adversarial inputs can occur naturally when the system's environment behaves randomly, even in…
▽ More
Neural network models have become the leading solution for a large variety of tasks, such as classification, language processing, protein folding, and others. However, their reliability is heavily plagued by adversarial inputs: small input perturbations that cause the model to produce erroneous outputs. Adversarial inputs can occur naturally when the system's environment behaves randomly, even in the absence of a malicious adversary, and are a severe cause for concern when attempting to deploy neural networks within critical systems. In this paper, we present a new statistical method, called Robustness Measurement and Assessment (RoMA), which can measure the expected robustness of a neural network model. Specifically, RoMA determines the probability that a random input perturbation might cause misclassification. The method allows us to provide formal guarantees regarding the expected frequency of errors that a trained model will encounter after deployment. Our approach can be applied to large-scale, black-box neural networks, which is a significant advantage compared to recently proposed verification methods. We apply our approach in two ways: comparing the robustness of different models, and measuring how a model's robustness is affected by the magnitude of input perturbation. One interesting insight obtained through this work is that, in a classification network, different output labels can exhibit very different robustness levels. We term this phenomenon categorial robustness. Our ability to perform risk and robustness assessments on a categorial basis opens the door to risk mitigation, which may prove to be a significant step towards neural network certification in safety-critical applications.
△ Less
Submitted 1 October, 2022; v1 submitted 21 October, 2021;
originally announced October 2021.
-
Knowing When to Quit: Selective Cascaded Regression with Patch Attention for Real-Time Face Alignment
Authors:
Gil Shapira,
Noga Levy,
Ishay Goldin,
Roy J. Jevnisek
Abstract:
Facial landmarks (FLM) estimation is a critical component in many face-related applications. In this work, we aim to optimize for both accuracy and speed and explore the trade-off between them. Our key observation is that not all faces are created equal. Frontal faces with neutral expressions converge faster than faces with extreme poses or expressions. To differentiate among samples, we train our…
▽ More
Facial landmarks (FLM) estimation is a critical component in many face-related applications. In this work, we aim to optimize for both accuracy and speed and explore the trade-off between them. Our key observation is that not all faces are created equal. Frontal faces with neutral expressions converge faster than faces with extreme poses or expressions. To differentiate among samples, we train our model to predict the regression error after each iteration. If the current iteration is accurate enough, we stop iterating, saving redundant iterations while kee** the accuracy in check. We also observe that as neighboring patches overlap, we can infer all facial landmarks (FLMs) with only a small number of patches without a major accuracy sacrifice. Architecturally, we offer a multi-scale, patch-based, lightweight feature extractor with a fine-grained local patch attention module, which computes a patch weighting according to the information in the patch itself and enhances the expressive power of the patch features. We analyze the patch attention data to infer where the model is attending when regressing facial landmarks and compare it to face attention in humans. Our model runs in real-time on a mobile device GPU, with 95 Mega Multiply-Add (MMA) operations, outperforming all state-of-the-art methods under 1000 MMA, with a normalized mean error of 8.16 on the 300W challenging dataset.
△ Less
Submitted 3 August, 2021; v1 submitted 1 August, 2021;
originally announced August 2021.
-
Real-Time Video Super-Resolution by Joint Local Inference and Global Parameter Estimation
Authors:
Noam Elron,
Alex Itskovich,
Shahar S. Yuval,
Noam Levy
Abstract:
The state of the art in video super-resolution (SR) are techniques based on deep learning, but they perform poorly on real-world videos (see Figure 1). The reason is that training image-pairs are commonly created by downscaling a high-resolution image to produce a low-resolution counterpart. Deep models are therefore trained to undo downscaling and do not generalize to super-resolving real-world i…
▽ More
The state of the art in video super-resolution (SR) are techniques based on deep learning, but they perform poorly on real-world videos (see Figure 1). The reason is that training image-pairs are commonly created by downscaling a high-resolution image to produce a low-resolution counterpart. Deep models are therefore trained to undo downscaling and do not generalize to super-resolving real-world images. Several recent publications present techniques for improving the generalization of learning-based SR, but are all ill-suited for real-time application.
We present a novel approach to synthesizing training data by simulating two digital-camera image-capture processes at different scales. Our method produces image-pairs in which both images have properties of natural images. Training an SR model using this data leads to far better generalization to real-world images and videos.
In addition, deep video-SR models are characterized by a high operations-per-pixel count, which prohibits their application in real-time. We present an efficient CNN architecture, which enables real-time application of video SR on low-power edge-devices. We split the SR task into two sub-tasks: a control-flow which estimates global properties of the input video and adapts the weights and biases of a processing-CNN that performs the actual processing. Since the process-CNN is tailored to the statistics of the input, its capacity kept low, while retaining effectivity. Also, since video-statistics evolve slowly, the control-flow operates at a much lower rate than the video frame-rate. This reduces the overall computational load by as much as two orders of magnitude. This framework of decoupling the adaptivity of the algorithm from the pixel processing, can be applied in a large family of real-time video enhancement applications, e.g., video denoising, local tone-map**, stabilization, etc.
△ Less
Submitted 6 May, 2021;
originally announced May 2021.
-
Blind Image Restoration without Prior Knowledge
Authors:
Noam Elron,
Shahar S. Yuval,
Dmitry Rudoy,
Noam Levy
Abstract:
Many image restoration techniques are highly dependent on the degradation used during training, and their performance declines significantly when applied to slightly different input. Blind and universal techniques attempt to mitigate this by producing a trained model that can adapt to varying conditions. However, blind techniques to date require prior knowledge of the degradation process, and assu…
▽ More
Many image restoration techniques are highly dependent on the degradation used during training, and their performance declines significantly when applied to slightly different input. Blind and universal techniques attempt to mitigate this by producing a trained model that can adapt to varying conditions. However, blind techniques to date require prior knowledge of the degradation process, and assumptions regarding its parameter-space. In this paper we present the Self-Normalization Side-Chain (SCNC), a novel approach to blind universal restoration in which no prior knowledge of the degradation is needed. This module can be added to any existing CNN topology, and is trained along with the rest of the network in an end-to-end manner. The imaging parameters relevant to the task, as well as their dynamics, are deduced from the variety in the training data. We apply our solution to several image restoration tasks, and demonstrate that the SNSC encodes the degradation-parameters, improving restoration performance.
△ Less
Submitted 8 March, 2020; v1 submitted 3 March, 2020;
originally announced March 2020.
-
Modeling infection methods of computer malware in the presence of vaccinations using epidemiological models: An analysis of real-world data
Authors:
Elad Yom-Tov,
Nir Levy,
Amir Rubin
Abstract:
Computer malware and biological pathogens often use similar mechanisms of infections. For this reason, it has been suggested to model malware spread using epidemiological models developed to characterize the spread of biological pathogens. However, most work examining the similarities between malware and pathogens using such methods was based on theoretical analysis and simulation.
Here we exten…
▽ More
Computer malware and biological pathogens often use similar mechanisms of infections. For this reason, it has been suggested to model malware spread using epidemiological models developed to characterize the spread of biological pathogens. However, most work examining the similarities between malware and pathogens using such methods was based on theoretical analysis and simulation.
Here we extend the classical Susceptible-Infected-Recovered (SIR) epidemiological model to describe two of the most common infection methods used by malware. We fit the proposed model to malware collected over a period of one year from a major anti-malware vendor. We show that by fitting the proposed model it is possible to identify the method of transmission used by the malware, its rate of infection, and the number of machines which will be infected unless blocked by anti-virus software. The Spearman correlation between the number of actual and predicted infected machines is 0.84.
Examining cases where an anti-malware "signature" was transmitted to susceptible computers by the anti-virus provider, we show that the time to remove the malware will be short and independent of the number of infected computers if fewer than approximately 60% of susceptible computers have been infected. If more computers were infected, the time to removal will be approximately 3.2 greater, and will depend on the fraction of infected computers.
Our results show that the application of epidemiological models of infection to malware can provide anti-virus providers with information on malware spread and its potential damage. We further propose that similarities between computer malware and biological pathogens, the availability of data on the former and the dearth of data on the latter, make malware an extremely useful model for testing interventions which could later be applied to improve medicine.
△ Less
Submitted 26 August, 2019;
originally announced August 2019.
-
Modeling influenza-like illnesses through composite compartmental models
Authors:
Nir Levy,
Michael Iv,
Elad Yom-Tov
Abstract:
Epidemiological models for the spread of pathogens in a population are usually only able to describe a single pathogen. This makes their application unrealistic in cases where multiple pathogens with similar symptoms are spreading concurrently within the same population. Here we describe a method which makes possible the application of multiple single-strain models under minimal conditions. As suc…
▽ More
Epidemiological models for the spread of pathogens in a population are usually only able to describe a single pathogen. This makes their application unrealistic in cases where multiple pathogens with similar symptoms are spreading concurrently within the same population. Here we describe a method which makes possible the application of multiple single-strain models under minimal conditions. As such, our method provides a bridge between theoretical models of epidemiology and data-driven approaches for modeling of influenza and other similar viruses.
Our model extends the Susceptible-Infected-Recovered model to higher dimensions, allowing the modeling of a population infected by multiple viruses. We further provide a method, based on an overcomplete dictionary of feasible realizations of SIR solutions, to blindly partition the time series representing the number of infected people in a population into individual components, each representing the effect of a single pathogen.
We demonstrate the applicability of our proposed method on five years of seasonal influenza-like illness (ILI) rates, estimated from Twitter data. We demonstrate that our method describes, on average, 44\% of the variance in the ILI time series. The individual infectious components derived from our model are matched to known viral profiles in the populations, which we demonstrate matches that of independently collected epidemiological data. We further show that the basic reproductive numbers ($R0$) of the matched components are in range known for these pathogens.
Our results suggest that the proposed method can be applied to other pathogens and geographies, providing a simple method for estimating the parameters of epidemics in a population.
△ Less
Submitted 7 June, 2017;
originally announced June 2017.
-
Towards correct-by-construction product variants of a software product line: GFML, a formal language for feature modules
Authors:
Thi-Kim-Zung Pham,
Catherine Dubois,
Nicole Levy
Abstract:
Software Product Line Engineering (SPLE) is a software engineering paradigm that focuses on reuse and variability. Although feature-oriented programming (FOP) can implement software product line efficiently, we still need a method to generate and prove correctness of all product variants more efficiently and automatically. In this context, we propose to manipulate feature modules which contain thr…
▽ More
Software Product Line Engineering (SPLE) is a software engineering paradigm that focuses on reuse and variability. Although feature-oriented programming (FOP) can implement software product line efficiently, we still need a method to generate and prove correctness of all product variants more efficiently and automatically. In this context, we propose to manipulate feature modules which contain three kinds of artifacts: specification, code and correctness proof. We depict a methodology and a platform that help the user to automatically produce correct-by-construction product variants from the related feature modules. As a first step of this project, we begin by proposing a language, GFML, allowing the developer to write such feature modules. This language is designed so that the artifacts can be easily reused and composed. GFML files contain the different artifacts mentioned above.The idea is to compile them into FoCaLiZe, a language for specification, implementation and formal proof with some object-oriented flavor. In this paper, we define and illustrate this language. We also introduce a way to compose the feature modules on some examples.
△ Less
Submitted 14 April, 2015;
originally announced April 2015.
-
Cognitive Wyner Networks with Clustered Decoding
Authors:
Amos Lapidoth,
Nathan Levy,
Shlomo Shamai,
Michele Wigger
Abstract:
We study an interference network where equally-numbered transmitters and receivers lie on two parallel lines, each transmitter opposite its intended receiver. We consider two short-range interference models: the "asymmetric network," where the signal sent by each transmitter is interfered only by the signal sent by its left neighbor (if present), and a "symmetric network," where it is interfered b…
▽ More
We study an interference network where equally-numbered transmitters and receivers lie on two parallel lines, each transmitter opposite its intended receiver. We consider two short-range interference models: the "asymmetric network," where the signal sent by each transmitter is interfered only by the signal sent by its left neighbor (if present), and a "symmetric network," where it is interfered by both its left and its right neighbors. Each transmitter is cognizant of its own message, the messages of the $t_\ell$ transmitters to its left, and the messages of the $t_r$ transmitters to its right. Each receiver decodes its message based on the signals received at its own antenna, at the $r_\ell$ receive antennas to its left, and the $r_r$ receive antennas to its right. For such networks we provide upper and lower bounds on the multiplexing gain, i.e., on the high-SNR asymptotic logarithmic growth of the sum-rate capacity. In some cases our bounds meet, e.g., for the asymmetric network. Our results exhibit an equivalence between the transmitter side-information parameters $t_\ell, t_r$ and the receiver side-information parameters $r_\ell, r_r$ in the sense that increasing/decreasing $t_\ell$ or $t_r$ by a positive integer $δ$ has the same effect on the multiplexing gain as increasing/decreasing $r_\ell$ or $r_r$ by $δ$. Moreover---even in asymmetric networks---there is an equivalence between the left side-information parameters $t_\ell, r_\ell$ and the right side-information parameters $t_r, r_r$.
△ Less
Submitted 9 October, 2013; v1 submitted 16 March, 2012;
originally announced March 2012.
-
On Information Rates of the Fading Wyner Cellular Model via the Thouless Formula for the Strip
Authors:
Nathan Levy,
Ofer Zeitouni,
Shlomo Shamai
Abstract:
We apply the theory of random Schrödinger operators to the analysis of multi-users communication channels similar to the Wyner model, that are characterized by short-range intra-cell broadcasting. With $H$ the channel transfer matrix, $HH^\dagger$ is a narrow-band matrix and in many aspects is similar to a random Schrödinger operator. We relate the per-cell sum-rate capacity of the channel to th…
▽ More
We apply the theory of random Schrödinger operators to the analysis of multi-users communication channels similar to the Wyner model, that are characterized by short-range intra-cell broadcasting. With $H$ the channel transfer matrix, $HH^\dagger$ is a narrow-band matrix and in many aspects is similar to a random Schrödinger operator. We relate the per-cell sum-rate capacity of the channel to the integrated density of states of a random Schrödinger operator; the latter is related to the top Lyapunov exponent of a random sequence of matrices via a version of the Thouless formula. Unlike related results in classical random matrix theory, limiting results do depend on the underlying fading distributions. We also derive several bounds on the limiting per-cell sum-rate capacity, some based on the theory of random Schrödinger operators, and some derived from information theoretical considerations. Finally, we get explicit results in the high-SNR regime for some particular cases.
△ Less
Submitted 18 June, 2008;
originally announced June 2008.
-
On Certain Large Random Hermitian Jacobi Matrices with Applications to Wireless Communications
Authors:
Nathan Levy,
Oren Somekh,
Shlomo Shamai,
Ofer Zeitouni
Abstract:
In this paper we study the spectrum of certain large random Hermitian Jacobi matrices. These matrices are known to describe certain communication setups. In particular we are interested in an uplink cellular channel which models mobile users experiencing a soft-handoff situation under joint multicell decoding. Considering rather general fading statistics we provide a closed form expression for t…
▽ More
In this paper we study the spectrum of certain large random Hermitian Jacobi matrices. These matrices are known to describe certain communication setups. In particular we are interested in an uplink cellular channel which models mobile users experiencing a soft-handoff situation under joint multicell decoding. Considering rather general fading statistics we provide a closed form expression for the per-cell sum-rate of this channel in high-SNR, when an intra-cell TDMA protocol is employed. Since the matrices of interest are tridiagonal, their eigenvectors can be considered as sequences with second order linear recurrence. Therefore, the problem is reduced to the study of the exponential growth of products of two by two matrices. For the case where $K$ users are simultaneously active in each cell, we obtain a series of lower and upper bound on the high-SNR power offset of the per-cell sum-rate, which are considerably tighter than previously known bounds.
△ Less
Submitted 16 June, 2008;
originally announced June 2008.
