More Like this

1. Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers

   Jafarpour, Saber; Harapanahalli, Akash; Coogan, Samuel (June 2023, 5th Annual Learning for Dynamics & Control Conference)

   N. Matni, M. Morari (Ed.)

   This paper proposes a computationally efficient framework, based on interval analysis, for rigorous verification of nonlinear continuous-time dynamical systems with neural network controllers. Given a neural network, we use an existing verification algorithm to construct inclusion functions for its input-output behavior. Inspired by mixed monotone theory, we embed the closed-loop dynamics into a larger system using an inclusion function of the neural network and a decomposition function of the open-loop system. This embedding provides a scalable approach for safety analysis of the neural control loop while preserving the nonlinear structure of the system. We show that one can efficiently compute hyper-rectangular over-approximations of the reachable sets using a single trajectory of the embedding system. We design an algorithm to leverage this computational advantage through partitioning strategies, improving our reachable set estimates while balancing its runtime with tunable parameters. We demonstrate the performance of this algorithm through two case studies. First, we demonstrate this method’s strength in complex nonlinear environments. Then, we show that our approach matches the performance of the state-of-the art verification algorithm for linear discretized systems. 

   more » « less
2. Scalable Zonotopic Under-approximation of Backward Reachable Sets for Uncertain Linear Systems

   https://doi.org/10.1109/LCSYS.2021.3123228  

   Yang, Liren; Ozay, Necmiye (January 2022, IEEE control systems letters)

   Zonotopes are widely used for over-approximating forward reachable sets of uncertain linear systems for verification purposes. In this paper, we use zonotopes to achieve more scalable algorithms that under-approximate backward reachable sets of uncertain linear systems for control design. The main difference is that the backward reachability analysis is a twoplayer game and involves Minkowski difference operations, but zonotopes are not closed under such operations. We underapproximate this Minkowski difference with a zonotope, which can be obtained by solving a linear optimization problem. We further develop an efficient zonotope order reduction technique to bound the complexity of the obtained zonotopic underapproximations. The proposed approach is evaluated against existing approaches using randomly generated instances and illustrated with several examples. 

   more » « less
3. Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming

   https://doi.org/10.1109/CDC42340.2020.9304296  

   Hu, Haimin; Fazlyab, Mahyar; Morari, Manfred; Pappas, George J. (December 2020, IEEE Conference on Decision and Control)

   There has been an increasing interest in using neural networks in closed-loop control systems to improve performance and reduce computational costs for on-line implementation. However, providing safety and stability guarantees for these systems is challenging due to the nonlinear and compositional structure of neural networks. In this paper, we propose a novel forward reachability analysis method for the safety verification of linear time-varying systems with neural networks in feedback interconnection. Our technical approach relies on abstracting the nonlinear activation functions by quadratic constraints, which leads to an outer-approximation of forward reachable sets of the closed-loop system. We show that we can compute these approximate reachable sets using semidefinite programming. We illustrate our method in a quadrotor example, in which we first approximate a nonlinear model predictive controller via a deep neural network and then apply our analysis tool to certify finite-time reachability and constraint satisfaction of the closed-loop system. 

   more » « less
4. PIVA: Privacy-Preserving Identity Verification Methods for Accountless Users via Private List Intersection and Variants

   https://doi.org/10.1007/978-3-031-70896-1_18  

   Hwang, Seoyeon; Jarecki, Stanislaw; Karl, Zane; van_Kempen, Elina; Tsudik, Gene (September 2024, Springer Nature Switzerland)

   Garcia-Alfaro, J; Kozik, R; Choraś, M; Katsikas, S (Ed.)

   Several prominent privacy regulation (e.g., CCPA and GDPR) require service providers to let consumers request access to, correct, or delete, their personal data. Compliance necessitates verification of consumer identity. This is not a problem for consumers who already have an account with a service provider since they can authenticate themselves via a successful account log-in. However, there are no such methods for accountless consumers, even though service providers routinely collect data about casual consumers, i.e., those without accounts. Currently, in order to access their collected data, accountless consumers are asked to provide Personally Identifiable Information (PII) to service providers, which is privacy-invasive. To address this problem, we propose PIVA: Privacy-Preserving Identity Verification for Accountless Users, a technique based on Private List Intersection (PLI) and its variants. First, we introduce PLI, a close relative of private set intersection (PSI), a well-known cryptographic primitive that allows two or more mutually suspicious parties to compute the intersection of their private input sets. PLI takes advantage of the (ordered and fixed) list structure of each party’s private set. As a result, PLI is more efficient than PSI. We also explore PLI variants: PLI-cardinality (PLI-CA), threshold-PLI (t-PLI), and threshold-PLI-cardinality (t-PLI-CA), all of which yield less information than PLI. These variants are progressively better suited for addressing the accountless consumer authentication problem. We prototype and compare its performance against techniques based on regular PSI and garbled circuits (GCs). Results show that proposed PLI and PLI-CA constructions are more efficient than GC-based techniques, in terms of both computation and communication overheads. While GC-based t-PLI and t-PLI-CA execute faster, proposed constructs greatly outperform the former in terms of bandwidth, e.g., our t-PLI protocol consumes less bandwidth. We also show that proposed protocols can be made secure against malicious adversaries, with only moderate increases in overhead. These variants outperform their GC-based counterparts by at least one order of magnitude. 

   more » « less
5. Transfer Learning with Uncertainty Quantification: Random Effect Calibration of Source to Target (RECaST)

   Hickey, Jimmy; Williams, Jonathan P; Hector, Emily C (November 2024, Journal of machine learning research)

   Transfer learning uses a data model, trained to make predictions or inferences on data from one population, to make reliable predictions or inferences on data from another population. Most existing transfer learning approaches are based on fine-tuning pre-trained neural network models, and fail to provide crucial uncertainty quantification. We develop a statistical framework for model predictions based on transfer learning, called RECaST. The primary mechanism is a Cauchy random effect that recalibrates a source model to a target population; we mathematically and empirically demonstrate the validity of our RECaST approach for transfer learning between linear models, in the sense that prediction sets will achieve their nominal stated coverage, and we numerically illustrate the method's robustness to asymptotic approximations for nonlinear models. Whereas many existing techniques are built on particular source models, RECaST is agnostic to the choice of source model, and does not require access to source data. For example, our RECaST transfer learning approach can be applied to a continuous or discrete data model with linear or logistic regression, deep neural network architectures, etc. Furthermore, RECaST provides uncertainty quantification for predictions, which is mostly absent in the literature. We examine our method's performance in a simulation study and in an application to real hospital data. 

   more » « less