-
Multimodal Deep Learning for Low-Resource Settings: A Vector Embedding Alignment Approach for Healthcare Applications
Authors:
David Restrepo,
Chenwei Wu,
Sebastián Andrés Cajas,
Luis Filipe Nakayama,
Leo Anthony Celi,
Diego M López
Abstract:
Large-scale multi-modal deep learning models have revolutionized domains such as healthcare, highlighting the importance of computational power. However, in resource-constrained regions like Low and Middle-Income Countries (LMICs), limited access to GPUs and data poses significant challenges, often leaving CPUs as the sole resource. To address this, we advocate for leveraging vector embeddings to…
▽ More
Large-scale multi-modal deep learning models have revolutionized domains such as healthcare, highlighting the importance of computational power. However, in resource-constrained regions like Low and Middle-Income Countries (LMICs), limited access to GPUs and data poses significant challenges, often leaving CPUs as the sole resource. To address this, we advocate for leveraging vector embeddings to enable flexible and efficient computational methodologies, democratizing multimodal deep learning across diverse contexts.
Our paper investigates the efficiency and effectiveness of using vector embeddings from single-modal foundation models and multi-modal Vision-Language Models (VLMs) for multimodal deep learning in low-resource environments, particularly in healthcare. Additionally, we propose a simple yet effective inference-time method to enhance performance by aligning image-text embeddings. Comparing these approaches with traditional methods, we assess their impact on computational efficiency and model performance using metrics like accuracy, F1-score, inference time, training time, and memory usage across three medical modalities: BRSET (ophthalmology), HAM10000 (dermatology), and SatelliteBench (public health).
Our findings show that embeddings reduce computational demands without compromising model performance. Furthermore, our alignment method improves performance in medical tasks. This research promotes sustainable AI practices by optimizing resources in constrained environments, highlighting the potential of embedding-based approaches for efficient multimodal learning. Vector embeddings democratize multimodal deep learning in LMICs, particularly in healthcare, enhancing AI adaptability in varied use cases.
△ Less
Submitted 1 June, 2024;
originally announced June 2024.
-
DF-DM: A foundational process model for multimodal data fusion in the artificial intelligence era
Authors:
David Restrepo,
Chenwei Wu,
Constanza Vásquez-Venegas,
Luis Filipe Nakayama,
Leo Anthony Celi,
Diego M López
Abstract:
In the big data era, integrating diverse data modalities poses significant challenges, particularly in complex fields like healthcare. This paper introduces a new process model for multimodal Data Fusion for Data Mining, integrating embeddings and the Cross-Industry Standard Process for Data Mining with the existing Data Fusion Information Group model. Our model aims to decrease computational cost…
▽ More
In the big data era, integrating diverse data modalities poses significant challenges, particularly in complex fields like healthcare. This paper introduces a new process model for multimodal Data Fusion for Data Mining, integrating embeddings and the Cross-Industry Standard Process for Data Mining with the existing Data Fusion Information Group model. Our model aims to decrease computational costs, complexity, and bias while improving efficiency and reliability. We also propose "disentangled dense fusion", a novel embedding fusion method designed to optimize mutual information and facilitate dense inter-modality feature interaction, thereby minimizing redundant information.
We demonstrate the model's efficacy through three use cases: predicting diabetic retinopathy using retinal images and patient metadata, domestic violence prediction employing satellite imagery, internet, and census data, and identifying clinical and demographic features from radiography images and clinical notes. The model achieved a Macro F1 score of 0.92 in diabetic retinopathy prediction, an R-squared of 0.854 and sMAPE of 24.868 in domestic violence prediction, and a macro AUC of 0.92 and 0.99 for disease prediction and sex classification, respectively, in radiological analysis.
These results underscore the Data Fusion for Data Mining model's potential to significantly impact multimodal data processing, promoting its adoption in diverse, resource-constrained settings.
△ Less
Submitted 2 June, 2024; v1 submitted 18 April, 2024;
originally announced April 2024.
-
Case Study: Neural Network Malware Detection Verification for Feature and Image Datasets
Authors:
Preston K. Robinette,
Diego Manzanas Lopez,
Serena Serbinowska,
Kevin Leach,
Taylor T. Johnson
Abstract:
Malware, or software designed with harmful intent, is an ever-evolving threat that can have drastic effects on both individuals and institutions. Neural network malware classification systems are key tools for combating these threats but are vulnerable to adversarial machine learning attacks. These attacks perturb input data to cause misclassification, bypassing protective systems. Existing defens…
▽ More
Malware, or software designed with harmful intent, is an ever-evolving threat that can have drastic effects on both individuals and institutions. Neural network malware classification systems are key tools for combating these threats but are vulnerable to adversarial machine learning attacks. These attacks perturb input data to cause misclassification, bypassing protective systems. Existing defenses often rely on enhancing the training process, thereby increasing the model's robustness to these perturbations, which is quantified using verification. While training improvements are necessary, we propose focusing on the verification process used to evaluate improvements to training. As such, we present a case study that evaluates a novel verification domain that will help to ensure tangible safeguards against adversaries and provide a more reliable means of evaluating the robustness and effectiveness of anti-malware systems. To do so, we describe malware classification and two types of common malware datasets (feature and image datasets), demonstrate the certified robustness accuracy of malware classifiers using the Neural Network Verification (NNV) and Neural Network Enumeration (nnenum) tools, and outline the challenges and future considerations necessary for the improvement and refinement of the verification of malware classification. By evaluating this novel domain as a case study, we hope to increase its visibility, encourage further research and scrutiny, and ultimately enhance the resilience of digital systems against malicious attacks.
△ Less
Submitted 8 April, 2024;
originally announced April 2024.
-
Online Reachability Analysis and Space Convexification for Autonomous Racing
Authors:
Sergiy Bogomolov,
Taylor T. Johnson,
Diego Manzanas Lopez,
Patrick Musau,
Paulius Stankaitis
Abstract:
This paper presents an optimisation-based approach for an obstacle avoidance problem within an autonomous vehicle racing context. Our control regime leverages online reachability analysis and sensor data to compute the maximal safe traversable region that an agent can traverse within the environment. The idea is to first compute a non-convex safe region, which then can be convexified via a novel…
▽ More
This paper presents an optimisation-based approach for an obstacle avoidance problem within an autonomous vehicle racing context. Our control regime leverages online reachability analysis and sensor data to compute the maximal safe traversable region that an agent can traverse within the environment. The idea is to first compute a non-convex safe region, which then can be convexified via a novel coupled separating hyperplane algorithm. This derived safe area is then used to formulate a nonlinear model-predictive control problem that seeks to find an optimal and safe driving trajectory. We evaluate the proposed approach through a series of diverse experiments and assess the runtime requirements of our proposed approach through an analysis of the effects of a set of varying optimisation objectives for generating these coupled hyperplanes.
△ Less
Submitted 16 November, 2023;
originally announced November 2023.
-
Robustness Verification of Deep Neural Networks using Star-Based Reachability Analysis with Variable-Length Time Series Input
Authors:
Neelanjana Pal,
Diego Manzanas Lopez,
Taylor T Johnson
Abstract:
Data-driven, neural network (NN) based anomaly detection and predictive maintenance are emerging research areas. NN-based analytics of time-series data offer valuable insights into past behaviors and estimates of critical parameters like remaining useful life (RUL) of equipment and state-of-charge (SOC) of batteries. However, input time series data can be exposed to intentional or unintentional no…
▽ More
Data-driven, neural network (NN) based anomaly detection and predictive maintenance are emerging research areas. NN-based analytics of time-series data offer valuable insights into past behaviors and estimates of critical parameters like remaining useful life (RUL) of equipment and state-of-charge (SOC) of batteries. However, input time series data can be exposed to intentional or unintentional noise when passing through sensors, necessitating robust validation and verification of these NNs. This paper presents a case study of the robustness verification approach for time series regression NNs (TSRegNN) using set-based formal methods. It focuses on utilizing variable-length input data to streamline input manipulation and enhance network architecture generalizability. The method is applied to two data sets in the Prognostics and Health Management (PHM) application areas: (1) SOC estimation of a Lithium-ion battery and (2) RUL estimation of a turbine engine. The NNs' robustness is checked using star-based reachability analysis, and several performance measures evaluate the effect of bounded perturbations in the input on network outputs, i.e., future outcomes. Overall, the paper offers a comprehensive case study for validating and verifying NN-based analytics of time-series data in real-world applications, emphasizing the importance of robustness testing for accurate and reliable predictions, especially considering the impact of noise on future outcomes.
△ Less
Submitted 25 July, 2023;
originally announced July 2023.
-
Optimal dividends and capital injection: A general Lévy model with extensions to regime-switching models
Authors:
Dante Mata López,
Kei Noba,
José-Luis Pérez,
Kazutoshi Yamazaki
Abstract:
This paper studies a general Lévy process model of the bail-out optimal dividend problem with an exponential time horizon, and further extends it to the regime-switching model. We first show the optimality of a double barrier strategy in the single-regime setting with a concave terminal payoff function. This is then applied to show the optimality of a Markov-modulated double barrier strategy in th…
▽ More
This paper studies a general Lévy process model of the bail-out optimal dividend problem with an exponential time horizon, and further extends it to the regime-switching model. We first show the optimality of a double barrier strategy in the single-regime setting with a concave terminal payoff function. This is then applied to show the optimality of a Markov-modulated double barrier strategy in the regime-switching model via contraction map** arguments. We solve these for a general Lévy model with both positive and negative jumps, greatly generalizing the existing results on spectrally one-sided models.
△ Less
Submitted 21 June, 2023;
originally announced June 2023.
-
Reachability Analysis of a General Class of Neural Ordinary Differential Equations
Authors:
Diego Manzanas Lopez,
Patrick Musau,
Nathaniel Hamilton,
Taylor T. Johnson
Abstract:
Continuous deep learning models, referred to as Neural Ordinary Differential Equations (Neural ODEs), have received considerable attention over the last several years. Despite their burgeoning impact, there is a lack of formal analysis techniques for these systems. In this paper, we consider a general class of neural ODEs with varying architectures and layers, and introduce a novel reachability fr…
▽ More
Continuous deep learning models, referred to as Neural Ordinary Differential Equations (Neural ODEs), have received considerable attention over the last several years. Despite their burgeoning impact, there is a lack of formal analysis techniques for these systems. In this paper, we consider a general class of neural ODEs with varying architectures and layers, and introduce a novel reachability framework that allows for the formal analysis of their behavior. The methods developed for the reachability analysis of neural ODEs are implemented in a new tool called NNVODE. Specifically, our work extends an existing neural network verification tool to support neural ODEs. We demonstrate the capabilities and efficacy of our methods through the analysis of a set of benchmarks that include neural ODEs used for classification, and in control and dynamical systems, including an evaluation of the efficacy and capabilities of our approach with respect to existing software tools within the continuous-time systems reachability literature, when it is possible to do so.
△ Less
Submitted 13 July, 2022;
originally announced July 2022.
-
An Empirical Analysis of the Use of Real-Time Reachability for the Safety Assurance of Autonomous Vehicles
Authors:
Patrick Musau,
Nathaniel Hamilton,
Diego Manzanas Lopez,
Preston Robinette,
Taylor T. Johnson
Abstract:
Recent advances in machine learning technologies and sensing have paved the way for the belief that safe, accessible, and convenient autonomous vehicles may be realized in the near future. Despite tremendous advances within this context, fundamental challenges around safety and reliability are limiting their arrival and comprehensive adoption. Autonomous vehicles are often tasked with operating in…
▽ More
Recent advances in machine learning technologies and sensing have paved the way for the belief that safe, accessible, and convenient autonomous vehicles may be realized in the near future. Despite tremendous advances within this context, fundamental challenges around safety and reliability are limiting their arrival and comprehensive adoption. Autonomous vehicles are often tasked with operating in dynamic and uncertain environments. As a result, they often make use of highly complex components, such as machine learning approaches, to handle the nuances of sensing, actuation, and control. While these methods are highly effective, they are notoriously difficult to assure. Moreover, within uncertain and dynamic environments, design time assurance analyses may not be sufficient to guarantee safety. Thus, it is critical to monitor the correctness of these systems at runtime. One approach for providing runtime assurance of systems with components that may not be amenable to formal analysis is the simplex architecture, where an unverified component is wrapped with a safety controller and a switching logic designed to prevent dangerous behavior. In this paper, we propose using a real-time reachability algorithm for the implementation of the simplex architecture to assure the safety of a 1/10 scale open source autonomous vehicle platform known as F1/10. The reachability algorithm that we leverage (a) provides provable guarantees of safety, and (b) is used to detect potentially unsafe scenarios. In our approach, the need to analyze an underlying controller is abstracted away, instead focusing on the effects of the controller's decisions on the system's future states. We demonstrate the efficacy of our architecture through a vast set of experiments conducted both in simulation and on an embedded hardware platform.
△ Less
Submitted 3 May, 2022;
originally announced May 2022.
-
Effects of positive jumps of assets on endogenous bankruptcy and optimal capital structure: Continuous- and periodic-observation models
Authors:
Dante Mata López,
José Luis Pérez,
Kazutoshi Yamazaki
Abstract:
In this paper, we study the optimal capital structure model with endogenous bankruptcy when the firm's asset value follows an exponential Lévy process with positive jumps. In the Leland-Toft framework \cite{LelandToft96}, we obtain the optimal bankruptcy barrier in the classical continuous-observation model and the periodic-observation model, recently studied by Palmowski et al.\ \cite{palmowski20…
▽ More
In this paper, we study the optimal capital structure model with endogenous bankruptcy when the firm's asset value follows an exponential Lévy process with positive jumps. In the Leland-Toft framework \cite{LelandToft96}, we obtain the optimal bankruptcy barrier in the classical continuous-observation model and the periodic-observation model, recently studied by Palmowski et al.\ \cite{palmowski2019leland}. We further consider the two-stage optimization problem of obtaining the optimal capital structure. Detailed numerical experiments are conducted to study the sensitivity of the firm's decision-making with respect to the observation frequency and positive jumps of the asset value.
△ Less
Submitted 24 August, 2020;
originally announced August 2020.
-
Logarithmic correction to resistance
Authors:
Antal A. Járai,
Dante Mata López
Abstract:
We study the trace of the incipient infinite oriented branching random walk in $\mathbb{Z}^d \times \mathbb{Z}_+$ when the dimension is $d = 6$. Under suitable moment assumptions, we show that the electrical resistance between the root and level $n$ is $O(n \log^{-ξ}n )$ for a $ξ> 0$ that does not depend on details of the model.
We study the trace of the incipient infinite oriented branching random walk in $\mathbb{Z}^d \times \mathbb{Z}_+$ when the dimension is $d = 6$. Under suitable moment assumptions, we show that the electrical resistance between the root and level $n$ is $O(n \log^{-ξ}n )$ for a $ξ> 0$ that does not depend on details of the model.
△ Less
Submitted 7 August, 2021; v1 submitted 6 June, 2020;
originally announced June 2020.
-
NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
Authors:
Hoang-Dung Tran,
Xiaodong Yang,
Diego Manzanas Lopez,
Patrick Musau,
Luan Viet Nguyen,
Weiming Xiang,
Stanley Bak,
Taylor T. Johnson
Abstract:
This paper presents the Neural Network Verification (NNV) software tool, a set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS). The crux of NNV is a collection of reachability algorithms that make use of a variety of set representations, such as polyhedra, star sets, zonotopes, and abstract-domain representations. NNV supports both exa…
▽ More
This paper presents the Neural Network Verification (NNV) software tool, a set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS). The crux of NNV is a collection of reachability algorithms that make use of a variety of set representations, such as polyhedra, star sets, zonotopes, and abstract-domain representations. NNV supports both exact (sound and complete) and over-approximate (sound) reachability algorithms for verifying safety and robustness properties of feed-forward neural networks (FFNNs) with various activation functions. For learning-enabled CPS, such as closed-loop control systems incorporating neural networks, NNV provides exact and over-approximate reachability analysis schemes for linear plant models and FFNN controllers with piecewise-linear activation functions, such as ReLUs. For similar neural network control systems (NNCS) that instead have nonlinear plant models, NNV supports over-approximate analysis by combining the star set analysis used for FFNN controllers with zonotope-based analysis for nonlinear plant dynamics building on CORA. We evaluate NNV using two real-world case studies: the first is safety verification of ACAS Xu networks and the second deals with the safety verification of a deep learning-based adaptive cruise control system.
△ Less
Submitted 11 April, 2020;
originally announced April 2020.
-
Verification for Machine Learning, Autonomy, and Neural Networks Survey
Authors:
Weiming Xiang,
Patrick Musau,
Ayana A. Wild,
Diego Manzanas Lopez,
Nathaniel Hamilton,
Xiaodong Yang,
Joel Rosenfeld,
Taylor T. Johnson
Abstract:
This survey presents an overview of verification techniques for autonomous systems, with a focus on safety-critical autonomous cyber-physical systems (CPS) and subcomponents thereof. Autonomy in CPS is enabling by recent advances in artificial intelligence (AI) and machine learning (ML) through approaches such as deep neural networks (DNNs), embedded in so-called learning enabled components (LECs)…
▽ More
This survey presents an overview of verification techniques for autonomous systems, with a focus on safety-critical autonomous cyber-physical systems (CPS) and subcomponents thereof. Autonomy in CPS is enabling by recent advances in artificial intelligence (AI) and machine learning (ML) through approaches such as deep neural networks (DNNs), embedded in so-called learning enabled components (LECs) that accomplish tasks from classification to control. Recently, the formal methods and formal verification community has developed methods to characterize behaviors in these LECs with eventual goals of formally verifying specifications for LECs, and this article presents a survey of many of these recent approaches.
△ Less
Submitted 3 October, 2018;
originally announced October 2018.
-
Reachable Set Estimation and Verification for Neural Network Models of Nonlinear Dynamic Systems
Authors:
Weiming Xiang,
Diego Manzanas Lopez,
Patrick Musau,
Taylor T. Johnson
Abstract:
Neural networks have been widely used to solve complex real-world problems. Due to the complicate, nonlinear, non-convex nature of neural networks, formal safety guarantees for the behaviors of neural network systems will be crucial for their applications in safety-critical systems. In this paper, the reachable set estimation and verification problems for Nonlinear Autoregressive-Moving Average (N…
▽ More
Neural networks have been widely used to solve complex real-world problems. Due to the complicate, nonlinear, non-convex nature of neural networks, formal safety guarantees for the behaviors of neural network systems will be crucial for their applications in safety-critical systems. In this paper, the reachable set estimation and verification problems for Nonlinear Autoregressive-Moving Average (NARMA) models in the forms of neural networks are addressed. The neural network involved in the model is a class of feed-forward neural networks called Multi-Layer Perceptron (MLP). By partitioning the input set of an MLP into a finite number of cells, a layer-by-layer computation algorithm is developed for reachable set estimation for each individual cell. The union of estimated reachable sets of all cells forms an over-approximation of reachable set of the MLP. Furthermore, an iterative reachable set estimation algorithm based on reachable set estimation for MLPs is developed for NARMA models. The safety verification can be performed by checking the existence of intersections of unsafe regions and estimated reachable set. Several numerical examples are provided to illustrate our approach.
△ Less
Submitted 10 February, 2018;
originally announced February 2018.
