-
Language-Enhanced Latent Representations for Out-of-Distribution Detection in Autonomous Driving
Authors:
Zhenjiang Mao,
Dong-You Jhong,
Ao Wang,
Ivan Ruchkin
Abstract:
Out-of-distribution (OOD) detection is essential in autonomous driving, to determine when learning-based components encounter unexpected inputs. Traditional detectors typically use encoder models with fixed settings, thus lacking effective human interaction capabilities. With the rise of large foundation models, multimodal inputs offer the possibility of taking human language as a latent represent…
▽ More
Out-of-distribution (OOD) detection is essential in autonomous driving, to determine when learning-based components encounter unexpected inputs. Traditional detectors typically use encoder models with fixed settings, thus lacking effective human interaction capabilities. With the rise of large foundation models, multimodal inputs offer the possibility of taking human language as a latent representation, thus enabling language-defined OOD detection. In this paper, we use the cosine similarity of image and text representations encoded by the multimodal model CLIP as a new representation to improve the transparency and controllability of latent encodings used for visual anomaly detection. We compare our approach with existing pre-trained encoders that can only produce latent representations that are meaningless from the user's standpoint. Our experiments on realistic driving data show that the language-based latent representation performs better than the traditional representation of the vision encoder and helps improve the detection performance when combined with standard representations.
△ Less
Submitted 2 May, 2024;
originally announced May 2024.
-
Zero-shot Safety Prediction for Autonomous Robots with Foundation World Models
Authors:
Zhenjiang Mao,
Siqi Dai,
Yuang Geng,
Ivan Ruchkin
Abstract:
A world model creates a surrogate world to train a controller and predict safety violations by learning the internal dynamic model of systems. However, the existing world models rely solely on statistical learning of how observations change in response to actions, lacking precise quantification of how accurate the surrogate dynamics are, which poses a significant challenge in safety-critical syste…
▽ More
A world model creates a surrogate world to train a controller and predict safety violations by learning the internal dynamic model of systems. However, the existing world models rely solely on statistical learning of how observations change in response to actions, lacking precise quantification of how accurate the surrogate dynamics are, which poses a significant challenge in safety-critical systems. To address this challenge, we propose foundation world models that embed observations into meaningful and causally latent representations. This enables the surrogate dynamics to directly predict causal future states by leveraging a training-free large language model. In two common benchmarks, this novel model outperforms standard world models in the safety prediction task and has a performance comparable to supervised learning despite not using any data. We evaluate its performance with a more specialized and system-relevant metric by comparing estimated states instead of aggregating observation-wide error.
△ Less
Submitted 2 May, 2024; v1 submitted 30 March, 2024;
originally announced April 2024.
-
Bridging Dimensions: Confident Reachability for High-Dimensional Controllers
Authors:
Yuang Geng,
Jake Brandon Baldauf,
Souradeep Dutta,
Chao Huang,
Ivan Ruchkin
Abstract:
Autonomous systems are increasingly implemented using end-to-end learning-based controllers. Such controllers make decisions that are executed on the real system, with images as one of the primary sensing modalities. Deep neural networks form a fundamental building block of such controllers. Unfortunately, the existing neural-network verification tools do not scale to inputs with thousands of dime…
▽ More
Autonomous systems are increasingly implemented using end-to-end learning-based controllers. Such controllers make decisions that are executed on the real system, with images as one of the primary sensing modalities. Deep neural networks form a fundamental building block of such controllers. Unfortunately, the existing neural-network verification tools do not scale to inputs with thousands of dimensions -- especially when the individual inputs (such as pixels) are devoid of clear physical meaning. This paper takes a step towards connecting exhaustive closed-loop verification with high-dimensional controllers. Our key insight is that the behavior of a high-dimensional controller can be approximated with several low-dimensional controllers. To balance the approximation accuracy and verifiability of our low-dimensional controllers, we leverage the latest verification-aware knowledge distillation. Then, we inflate low-dimensional reachability results with statistical approximation errors, yielding a high-confidence reachability guarantee for the high-dimensional controller. We investigate two inflation techniques -- based on trajectories and control actions -- both of which show convincing performance in three OpenAI gym benchmarks.
△ Less
Submitted 2 May, 2024; v1 submitted 8 November, 2023;
originally announced November 2023.
-
Repairing Learning-Enabled Controllers While Preserving What Works
Authors:
Pengyuan Lu,
Matthew Cleaveland,
Oleg Sokolsky,
Insup Lee,
Ivan Ruchkin
Abstract:
Learning-enabled controllers have been adopted in various cyber-physical systems (CPS). When a learning-enabled controller fails to accomplish its task from a set of initial states, researchers leverage repair algorithms to fine-tune the controller's parameters. However, existing repair techniques do not preserve previously correct behaviors. Specifically, when modifying the parameters to repair t…
▽ More
Learning-enabled controllers have been adopted in various cyber-physical systems (CPS). When a learning-enabled controller fails to accomplish its task from a set of initial states, researchers leverage repair algorithms to fine-tune the controller's parameters. However, existing repair techniques do not preserve previously correct behaviors. Specifically, when modifying the parameters to repair trajectories from a subset of initial states, another subset may be compromised. Therefore, the repair may break previously correct scenarios, introducing new risks that may not be accounted for. Due to this issue, repairing the entire initial state space may be hard or even infeasible. As a response, we formulate the Repair with Preservation (RwP) problem, which calls for preserving the already-correct scenarios during repair. To tackle this problem, we design the Incremental Simulated Annealing Repair (ISAR) algorithm, which leverages simulated annealing on a barriered energy function to safeguard the already-correct initial states while repairing as many additional ones as possible. Moreover, formal verification is utilized to guarantee the repair results. Case studies on an Unmanned Underwater Vehicle (UUV) and OpenAI Gym Mountain Car (MC) show that ISAR not only preserves correct behaviors from previously verified initial state regions, but also repairs 81.4% and 23.5% of broken state spaces in the two benchmarks. Moreover, the average signal temporal logic (STL) robustnesses of the ISAR repaired controllers are larger than those of the controllers repaired using baseline methods.
△ Less
Submitted 13 March, 2024; v1 submitted 6 November, 2023;
originally announced November 2023.
-
Curating Naturally Adversarial Datasets for Learning-Enabled Medical Cyber-Physical Systems
Authors:
Sydney Pugh,
Ivan Ruchkin,
Insup Lee,
James Weimer
Abstract:
Deep learning models have shown promising predictive accuracy for time-series healthcare applications. However, ensuring the robustness of these models is vital for building trustworthy AI systems. Existing research predominantly focuses on robustness to synthetic adversarial examples, crafted by adding imperceptible perturbations to clean input data. However, these synthetic adversarial examples…
▽ More
Deep learning models have shown promising predictive accuracy for time-series healthcare applications. However, ensuring the robustness of these models is vital for building trustworthy AI systems. Existing research predominantly focuses on robustness to synthetic adversarial examples, crafted by adding imperceptible perturbations to clean input data. However, these synthetic adversarial examples do not accurately reflect the most challenging real-world scenarios, especially in the context of healthcare data. Consequently, robustness to synthetic adversarial examples may not necessarily translate to robustness against naturally occurring adversarial examples, which is highly desirable for trustworthy AI. We propose a method to curate datasets comprised of natural adversarial examples to evaluate model robustness. The method relies on probabilistic labels obtained from automated weakly-supervised labeling that combines noisy and cheap-to-obtain labeling heuristics. Based on these labels, our method adversarially orders the input data and uses this ordering to construct a sequence of increasingly adversarial datasets. Our evaluation on six medical case studies and three non-medical case studies demonstrates the efficacy and statistical validity of our approach to generating naturally adversarial datasets
△ Less
Submitted 7 November, 2023; v1 submitted 1 September, 2023;
originally announced September 2023.
-
Distributionally Robust Statistical Verification with Imprecise Neural Networks
Authors:
Souradeep Dutta,
Michele Caprio,
Vivian Lin,
Matthew Cleaveland,
Kuk ** Jang,
Ivan Ruchkin,
Oleg Sokolsky,
Insup Lee
Abstract:
A particularly challenging problem in AI safety is providing guarantees on the behavior of high-dimensional autonomous systems. Verification approaches centered around reachability analysis fail to scale, and purely statistical approaches are constrained by the distributional assumptions about the sampling process. Instead, we pose a distributionally robust version of the statistical verification…
▽ More
A particularly challenging problem in AI safety is providing guarantees on the behavior of high-dimensional autonomous systems. Verification approaches centered around reachability analysis fail to scale, and purely statistical approaches are constrained by the distributional assumptions about the sampling process. Instead, we pose a distributionally robust version of the statistical verification problem for black-box systems, where our performance guarantees hold over a large family of distributions. This paper proposes a novel approach based on a combination of active learning, uncertainty quantification, and neural network verification. A central piece of our approach is an ensemble technique called Imprecise Neural Networks, which provides the uncertainty to guide active learning. The active learning uses an exhaustive neural-network verification tool Sherlock to collect samples. An evaluation on multiple physical simulators in the openAI gym Mujoco environments with reinforcement-learned controllers demonstrates that our approach can provide useful and scalable guarantees for high-dimensional systems.
△ Less
Submitted 11 December, 2023; v1 submitted 28 August, 2023;
originally announced August 2023.
-
How Safe Am I Given What I See? Calibrated Prediction of Safety Chances for Image-Controlled Autonomy
Authors:
Zhenjiang Mao,
Carson Sobolewski,
Ivan Ruchkin
Abstract:
End-to-end learning has emerged as a major paradigm for develo** autonomous systems. Unfortunately, with its performance and convenience comes an even greater challenge of safety assurance. A key factor of this challenge is the absence of the notion of a low-dimensional and interpretable dynamical state, around which traditional assurance methods revolve. Focusing on the online safety prediction…
▽ More
End-to-end learning has emerged as a major paradigm for develo** autonomous systems. Unfortunately, with its performance and convenience comes an even greater challenge of safety assurance. A key factor of this challenge is the absence of the notion of a low-dimensional and interpretable dynamical state, around which traditional assurance methods revolve. Focusing on the online safety prediction problem, this paper proposes a configurable family of learning pipelines based on generative world models, which do not require low-dimensional states. To implement these pipelines, we overcome the challenges of learning safety-informed latent representations and missing safety labels under prediction-induced distribution shift. These pipelines come with statistical calibration guarantees on their safety chance predictions based on conformal prediction. We perform an extensive evaluation of the proposed learning pipelines on two case studies of image-controlled systems: a racing car and a cartpole.
△ Less
Submitted 18 June, 2024; v1 submitted 23 August, 2023;
originally announced August 2023.
-
Causal Repair of Learning-enabled Cyber-physical Systems
Authors:
Pengyuan Lu,
Ivan Ruchkin,
Matthew Cleaveland,
Oleg Sokolsky,
Insup Lee
Abstract:
Models of actual causality leverage domain knowledge to generate convincing diagnoses of events that caused an outcome. It is promising to apply these models to diagnose and repair run-time property violations in cyber-physical systems (CPS) with learning-enabled components (LEC). However, given the high diversity and complexity of LECs, it is challenging to encode domain knowledge (e.g., the CPS…
▽ More
Models of actual causality leverage domain knowledge to generate convincing diagnoses of events that caused an outcome. It is promising to apply these models to diagnose and repair run-time property violations in cyber-physical systems (CPS) with learning-enabled components (LEC). However, given the high diversity and complexity of LECs, it is challenging to encode domain knowledge (e.g., the CPS dynamics) in a scalable actual causality model that could generate useful repair suggestions. In this paper, we focus causal diagnosis on the input/output behaviors of LECs. Specifically, we aim to identify which subset of I/O behaviors of the LEC is an actual cause for a property violation. An important by-product is a counterfactual version of the LEC that repairs the run-time property by fixing the identified problematic behaviors. Based on this insights, we design a two-step diagnostic pipeline: (1) construct and Halpern-Pearl causality model that reflects the dependency of property outcome on the component's I/O behaviors, and (2) perform a search for an actual cause and corresponding repair on the model. We prove that our pipeline has the following guarantee: if an actual cause is found, the system is guaranteed to be repaired; otherwise, we have high probabilistic confidence that the LEC under analysis did not cause the property violation. We demonstrate that our approach successfully repairs learned controllers on a standard OpenAI Gym benchmark.
△ Less
Submitted 26 April, 2023; v1 submitted 5 April, 2023;
originally announced April 2023.
-
Conservative Safety Monitors of Stochastic Dynamical Systems
Authors:
Matthew Cleaveland,
Oleg Sokolsky,
Insup Lee,
Ivan Ruchkin
Abstract:
Generating accurate runtime safety estimates for autonomous systems is vital to ensuring their continued proliferation. However, exhaustive reasoning about future behaviors is generally too complex to do at runtime. To provide scalable and formal safety estimates, we propose a method for leveraging design-time model checking results at runtime. Specifically, we model the system as a probabilistic…
▽ More
Generating accurate runtime safety estimates for autonomous systems is vital to ensuring their continued proliferation. However, exhaustive reasoning about future behaviors is generally too complex to do at runtime. To provide scalable and formal safety estimates, we propose a method for leveraging design-time model checking results at runtime. Specifically, we model the system as a probabilistic automaton (PA) and compute bounded-time reachability probabilities over the states of the PA at design time. At runtime, we combine distributions of state estimates with the model checking results to produce a bounded time safety estimate. We argue that our approach produces well-calibrated safety probabilities, assuming the estimated state distributions are well-calibrated. We evaluate our approach on simulated water tanks.
△ Less
Submitted 29 March, 2023; v1 submitted 26 January, 2023;
originally announced January 2023.
-
Confidence Composition for Monitors of Verification Assumptions
Authors:
Ivan Ruchkin,
Matthew Cleaveland,
Radoslav Ivanov,
Pengyuan Lu,
Taylor Carpenter,
Oleg Sokolsky,
Insup Lee
Abstract:
Closed-loop verification of cyber-physical systems with neural network controllers offers strong safety guarantees under certain assumptions. It is, however, difficult to determine whether these guarantees apply at run time because verification assumptions may be violated. To predict safety violations in a verified system, we propose a three-step confidence composition (CoCo) framework for monitor…
▽ More
Closed-loop verification of cyber-physical systems with neural network controllers offers strong safety guarantees under certain assumptions. It is, however, difficult to determine whether these guarantees apply at run time because verification assumptions may be violated. To predict safety violations in a verified system, we propose a three-step confidence composition (CoCo) framework for monitoring verification assumptions. First, we represent the sufficient condition for verified safety with a propositional logical formula over assumptions. Second, we build calibrated confidence monitors that evaluate the probability that each assumption holds. Third, we obtain the confidence in the verification guarantees by composing the assumption monitors using a composition function suitable for the logical formula. Our CoCo framework provides theoretical bounds on the calibration and conservatism of compositional monitors. Two case studies show that compositional monitors are calibrated better than their constituents and successfully predict safety violations.
△ Less
Submitted 5 May, 2022; v1 submitted 3 November, 2021;
originally announced November 2021.
-
Monotonic Safety for Scalable and Data-Efficient Probabilistic Safety Analysis
Authors:
Matthew Cleaveland,
Ivan Ruchkin,
Oleg Sokolsky,
Insup Lee
Abstract:
Autonomous systems with machine learning-based perception can exhibit unpredictable behaviors that are difficult to quantify, let alone verify. Such behaviors are convenient to capture in probabilistic models, but probabilistic model checking of such models is difficult to scale -- largely due to the non-determinism added to models as a prerequisite for provable conservatism. Statistical model che…
▽ More
Autonomous systems with machine learning-based perception can exhibit unpredictable behaviors that are difficult to quantify, let alone verify. Such behaviors are convenient to capture in probabilistic models, but probabilistic model checking of such models is difficult to scale -- largely due to the non-determinism added to models as a prerequisite for provable conservatism. Statistical model checking (SMC) has been proposed to address the scalability issue. However it requires large amounts of data to account for the aforementioned non-determinism, which in turn limits its scalability. This work introduces a general technique for reduction of non-determinism based on assumptions of "monotonic safety'", which define a partial order between system states in terms of their probabilities of being safe. We exploit these assumptions to remove non-determinism from controller/plant models to drastically speed up probabilistic model checking and statistical model checking while providing provably conservative estimates as long as the safety is indeed monotonic. Our experiments demonstrate model-checking speed-ups of an order of magnitude while maintaining acceptable accuracy and require much less data for accurate estimates when running SMC -- even when monotonic safety does not perfectly hold and provable conservatism is not achieved.
△ Less
Submitted 16 March, 2022; v1 submitted 4 November, 2021;
originally announced November 2021.
-
Foundations and Tools for End-User Architecting
Authors:
David Garlan,
Vishal Dwivedi,
Ivan Ruchkin,
Bradley Schmerl
Abstract:
Within an increasing number of domains an important emerging need is the ability for technically naive users to compose computational elements into novel configurations. Examples include astronomers who create new analysis pipelines to process telescopic data, intelligence analysts who must process diverse sources of unstructured text to discover socio-technical trends, and medical researchers who…
▽ More
Within an increasing number of domains an important emerging need is the ability for technically naive users to compose computational elements into novel configurations. Examples include astronomers who create new analysis pipelines to process telescopic data, intelligence analysts who must process diverse sources of unstructured text to discover socio-technical trends, and medical researchers who have to process brain image data in new ways to understand disease pathways. Creating such compositions today typically requires low-level technical expertise, limiting the use of computational methods and increasing the cost of using them. In this paper we describe an approach - which we term end-user architecting - that exploits the similarity between such compositional activities and those of software architects. Drawing on the rich heritage of software architecture languages, methods, and tools, we show how those techniques can be adapted to support end users in composing rich computational systems through domain-specific compositional paradigms and component repositories, without requiring that they have knowledge of the low-level implementation details of the components or the compositional infrastructure. Further, we outline a set of open research challenges that the area of end-user architecting raises.
△ Less
Submitted 17 October, 2012;
originally announced October 2012.
-
Single-window Integrated Development Environment
Authors:
Ivan Ruchkin,
Vladimir Prus
Abstract:
This paper addresses the problem of IDE interface complexity by introducing single-window graphical user interface. This approach lies in removing additional child windows from IDE, thus allowing a user to keep only text editor window open. We describe an abstract model of IDE GUI that is based on most popular modern integrated environments and has generalized user interface parts. Then this abstr…
▽ More
This paper addresses the problem of IDE interface complexity by introducing single-window graphical user interface. This approach lies in removing additional child windows from IDE, thus allowing a user to keep only text editor window open. We describe an abstract model of IDE GUI that is based on most popular modern integrated environments and has generalized user interface parts. Then this abstract model is reorganized into single windowed interface model: access to common IDE functions is provided from the code editing window while utility windows are removed without loss of IDE functionality. After that the implementation of single-window GUI on KDevelop 4 is described. And finally tool views and usability of several well- known IDEs are surveyed.
△ Less
Submitted 5 July, 2012;
originally announced July 2012.
