A major gap in the effective employment of autonomous systems is the ability to measure and validate the performance of human-autonomy collaboration. Toward improved methods for evaluating human-AI collaboration, we present a Testbed for Human-Autonomy Teaming (Testbed4HAT). Testbed4HAT tests real-time decisions made in a stressing maritime defense command and control (C2) scenario, in which the number of threats and timing of the scenario motivates the use of AI recommendations for timely and effective decisions. In our system, recommendations are provided by a novel deep reinforcement learning (DRL) agent, trained to be a tactical decision aid for planning weapon-to-target assignments. Testbed4HAT affords study of the effects of novel conditions on the human-autonomy team, allowing the characterization of performance in non-ideal, realistic conditions using a conceptual model to benchmark the potential human-autonomy collaboration performance. We demonstrate the utility of Testbed4HAT for measuring the effectiveness and reliability of human-autonomy teams, comparing the performance of humans alone, AI alone, and human-AI teams. We provide preliminary observations of the impact of an AI teammate on human judgement and motivate future work leveraging the testbed.

Unmanned ground vehicles (UGVs) that autonomously maneuver over off-road terrain are susceptible to a loss of stability through untripped rollovers. Without human supervision and intervention, untripped rollovers can damage the UGV and render it unusable. We create a runtime monitor that can provide protection against rollovers that is independent of the type of high-level autonomy strategy (path planning, navigation, etc.) used to command the platform. In particular, we present an implementation of a predictive system monitor for untripped rollover protection in a skid-steer robotic platform. The system monitor sits between the UGV’s autonomy stack and the platform, and it ensures that the platform is not at risk of rollover by intercepting mobility commands sent by the autonomy stack, predicting platform stability, and adjusting the mobility commands to avoid potential rollovers. We demonstrate our implementation through experiments with skid-steer UGVs in Gazebo simulation and physical experiments. Citation: E. Dietrich, S. Pohland, D. Genin, A. Schmidt, G. Vallabha, A. Composto, M. Randolph, “A Runtime Monitor for Platform Protection Against Skid-steer Untripped Rollovers,” In Proceedings of the Ground Vehicle Systems Engineering and Technology Symposium (GVSETS), NDIA, Novi, MI, Aug. 15-17, 2023.

We present an implementation of a formally verified safety fallback controller for improved collision avoidance in an autonomous vehicle research platform. Our approach uses a primary trajectory planning system that aims for collision-free navigation in the presence of pedestrians and other vehicles, and a fallback controller that guards its behavior. The safety fallback controller excludes the possibility of collisions by accounting for nondeterministic uncertainty in the dynamics of the vehicle and moving obstacles, and takes over the primary controller as necessary. We demonstrate the system in an experimental set-up that includes simulations and real-world tests with a 1/5-scale vehicle. In stressing simulation scenarios, the safety fallback controller significantly reduces the number of collisions.

Artificial intelligence in the form of machine learning algorithms is driving the latest industrial revolution, leading to disruptive changes in the ways we communicate, interact, design, collect information, and express ourselves. While these changes offer new possibilities for our societies, they may also introduce biases that can lead to unfair decisions. This issue is particularly critical in the context of medical diagnosis, as bias can jeopardize patient treatment and health. To mitigate these biases, it is essential to such biases and involve all relevant stakeholders in the design of fair machine learning algorithms. In this context, the MACAIF project aims to develop user-centred interfaces that allow stakeholders, including doctors, to challenge the fairness of machine learning algorithms based on demographics, such as gender or race. Our project proposes a methodology to engage with stakeholders and incorporate their concerns during the design of a dashboard based on MLighter - an adversarial tool which is applied to identify fairness-related issues in machine learning models.

A scientific model's usefulness relies on its ability to explain phenomena, predict how such phenomena will be impacted by future interventions, and prescribe actions to achieve desired outcomes. We study methods for learning causal models that explain the behaviors of simulated "human" populations. Through the Ground Truth project, we solved a series of Challenges where our explanations, predictions and prescriptions were scored against ground truth information. We describe the processes that emerged for applying causal discovery, network analysis, agent-based modeling and other analytical methods to inform solutions to Challenge tasks. We present our team's overall performance results on these Challenges and discuss implications for future efforts to validate social scientific research using simulation-based challenges.

We present an approach to analyze the safety of asynchronous, independent, non-deterministic, turn-to-bearing horizontal maneuvers for two vehicles. Future turn rates, final bearings, and continuously varying ground speeds throughout the encounter are unknown but restricted to known ranges. We develop a library of formal proofs about turning kinematics and apply the library to create a formally verified timing computation. Additionally, we create a technique that evaluates future collision possibilities that is based on waves of position possibilities and relies on the timing computation. The result either determines that the encounter will be collision-free, or computes a safe overapproximation for when and where collisions may occur.

For AI-controlled mobile platforms, avoiding collisions with walls and boundaries is an important safety requirement. This is a problem especially for fast-moving aerial vehicles, such as fixed-wing aircraft, that cannot be brought to a stop in an emergency. To enable geographic confinement of such AI-controlled vehicles, we present a formally verified algorithm for predicting geofence violations and selecting a safe maneuver that will keep the vehicle within the designated operations area. The algorithm is based on a higher-order dynamics model that generalizes circular turns using linearly changing centripetal acceleration and allows handling of uncertainty in model parameters. The proposed algorithm was implemented along with extensions to handle non-determinism, and flight-tested on an autonomous aircraft.

We investigate a method for formally verifying the absence of adversarial examples in a neural network controller. Our approach applies to networks with piecewise affine activation units, which may be encoded symbolically as a piecewise affine mapping from inputs to outputs. The approach rests on characterizing and bounding a critical subset of the state space where controller action is required, partitioning this critical subset, and using satisfiability modulo theories (SMT) to prove nonexistence of safety counterexamples on each of the resulting partition elements. We demonstrate this approach on a simple collision avoidance neural network controller, trained with reinforcement learning to avoid collisions in a simplified simulated environment. After encoding the network weights in SMT, we formally verify safety of the neural network controller on a subset of the critical partition elements, and determine that the rest of the critical set partition elements are potentially unsafe. We further experimentally confirm the existence of actual adversarial collision scenarios in 90% of the identified potentially unsafe critical partition elements, indicating that our approach is reasonably tight.

For complex artificially intelligent systems to be incorporated into applications where safety is critical, the systems must be safe and reliable. This article describes work a Johns Hopkins University Applied Physics Laboratory (APL) team is doing toward verifying safety in artificial intelligence and reinforcement learning systems.

For AI-controlled mobile platforms, avoiding collisions with walls and boundaries is an important safety requirement. This is a problem especially for fast-moving aerial vehicles, such as fixed-wing aircraft, that cannot be brought to a stop in an emergency. To enable geographic confinement of such AI-controlled vehicles, we present a formally verified algorithm for predicting geofence violations and selecting a safe maneuver that will keep the vehicle within the designated operations area. The algorithm is based on a higher-order dynamics model that generalizes circular turns using linearly changing centripetal acceleration and allows handling of uncertainty in model parameters. The proposed algorithm was implemented along with extensions to handle non-determinism, and flight-tested on an autonomous aircraft.

We describe and validate a system for monitoring social contagions on Twitter: social movements, rumors, and emotional outbursts that spread from person to person in a viral manner. We use Twitter streams to monitor the spread of these phenomena through human social and information networks. This system, the contagion monitor, parses Twitter posts to identify emerging phenomena, as captured in hashtags, URLs, words and phrases, or account-handles, and then determines the extent to which a particular phenomenon spreads via the social network (in contrast to its spread via news broadcasts or independent adoption) and locates the contagion within Twitter communities. The monitor approximates the adoption threshold of a social contagion by measuring the fraction of Twitter users who were "infected" by the contagion (e.g., joined a particular social movement) after more than one of their friends had done so. Finally, the monitor makes a judgment about whether the phenomenon has reached critical mass, which is defined as the point where a social contagion begins spreading rapidly and breaches the social boundaries of its early adopter group. We test our prototype monitor on two data sources --- an ongoing stream of tweets grouped by user-added hashtags and a collection of posts by a monitored set of Nigerian Twitter users --- before productionalizing. We use the Amazon Mechanical Turk platform to evaluate the performance on both data sources. In both cases, we find that our approach successfully distinguishes between high-threshold and low-threshold social contagions.

There is great interest in using formal methods to guarantee the reliability of deep neural networks. However, these techniques may also be used to implant carefully selected input-output pairs. We present initial results on a novel technique for using SMT solvers to fine tune the weights of a ReLU neural network to guarantee outcomes on a finite set of particular examples. This procedure can be used to ensure performance on key examples, but it could also be used to insert difficult-to-find incorrect examples that trigger unexpected performance. We demonstrate this approach by fine tuning an MNIST network to incorrectly classify a particular image and discuss the potential for the approach to compromise reliability of freely-shared machine learning models.

We describe an approach to developing a verified controller using hybrid system safety predicates. It selects from a dictionary of sequences of control actions, interleaving them and under model assumptions guaranteeing their continuing safety in unbounded time. The controller can adapt to changing priorities and objectives during operation. It can confer safety guarantees on a primary controller, identifying, intervening, and remediating actions that might lead to unsafe conditions in the future. Remediation is delayed until the latest time at which a safety-preserving intervention is available. When the assumptions of the safety proofs are violated, the controller provides altered but quantifiable safety guarantees. We apply this approach to synthesize a controller for aircraft collision avoidance, and report on the performance of this controller as a stand-alone collision avoidance system, and as a safety controller for the FAA's next-generation aircraft collision avoidance system ACAS X.

We investigate the use of spectral clustering of hashtag adoptions in Nigerian Twitter users between October 2013 and November 2014. This period is of interest due to the online campaign centered around the #BringBackOurGirls (BBOG) hashtag, which relates to the kidnapping of 276 Nigerian schoolgirls. We examine the adoption of hashtags during the six months before, the month after, and the six months following the kidnapping to test the informational value of behavior-based clusters discovered with unsupervised methods for predicting future hashtag usage behaviors. We demonstrate an efficient spectral clustering approach, that leverages power iteration on symmetric adjacency matrices, to group users based on hashtag adoptions prior to the kidnapping. Unlike follow network-based clusters, these adoption-based clusters reveal groups of users with similar interests and prove to be more predictive of interest in future topics. We compare this unsupervised spectral clustering to spectral clustering based on symmetrized follow network relations as well as clusters induced by latent Dirichlet allocation (LDA) topics. We find that hashtag adoption-based clusters perform similarly to the more computationally expensive LDA approach at identifying interest groups that are more likely to adopt future topical tags. We also benchmark the spectral clustering approach against the popular Louvain clustering approach on a synthetic dataset, finding the faster spectral clustering algorithm produces more balanced clusters with a higher similarity to the true interest groupings used to synthesize adoption data.

We address zero-shot (ZS) learning, building upon prior work in hierarchical classification by combining it with approaches based on semantic attribute estimation. For both non-novel and novel image classes we compare multiple formulations of the problem, starting with deep universal features in each case. We investigate the effect of using different posterior probabilities as inputs to the hierarchical classifier, comparing the performances of posteriors derived from distances to SVM classifier boundaries with those of posteriors based on semantic attribute estimation. Using a dataset consisting of 150 object classes from the ImageNet ILSVRC2012 data set, we find that the hierarchical classification method that maximizes expected reward for non-novel classes differs from the method that maximizes expected reward for novel classes. We also show that using input posteriors based on semantic attributes improves the expected reward for novel classes.

We examine hierarchical approaches to image classification problems that include categories for which we have no training examples. Building on prior work in hierarchical classification that optimizes the trade-off between depth in a tree and accuracy of placement, we compare the performance of multiple formulations of the problem on both previously seen (non-novel) and previously unseen (novel) classes. We use a subset of 150 object classes from the ImageNet ILSVRC2012 data set, for which we have 218 human-annotated semantic attribute labels and for which we compute deep convolutional features using the OVERFEAT network. We quantitatively evaluate several approaches, using input posteriors derived from distances to SVM classifier boundaries as well as input posteriors based on semantic attribute estimation. We find that the relative performances of the methods differ in non-novel and novel applications and achieve information gains in novel applications through the incorporation of attribute-based posteriors.

The Next-Generation Airborne Collision Avoidance System (ACAS X) is intended to be installed on all large aircraft to give advice to pilots and prevent mid-air collisions with other aircraft. It is currently being developed by the Federal Aviation Administration (FAA). In this paper, we determine the geometric configurations under which the advice given by ACAS X is safe under a precise set of assumptions and formally verify these configurations using hybrid systems theorem proving techniques. We consider subsequent advisories and show how to adapt our formal verification to take them into account. We examine the current version of the real ACAS X system and discuss some cases where our safety theorem conflicts with the actual advisory given by that version, demonstrating how formal hybrid systems proving approaches are helping to ensure the safety of ACAS X. Our approach is general and could also be used to identify unsafe advice issued by other collision avoidance systems or confirm their safety.

We present the formally verified predicate and strategy used to independently evaluate the safety of the final version (Run 15) of the FAAs next-generation air-traffic collision avoidance system, ACAS X. This approach is a general one that can analyze simultaneous vertical and horizontal maneuvers issued by aircraft collision avoidance systems. The predicate is specialized to analyze sequences of vertical maneuvers, and in the horizontal dimension is modular, allowing it to be safely composed with separately analyzed horizontal dynamics. Unlike previous efforts, this approach enables analysis of aircraft that are turning, and accelerating non-deterministically. It can also analyze the safety of coordinated advisories, and encounters with more than two aircraft. We provide results on the safety evaluation of ACAS X coordinated collision avoidance on a subset of the system state space. This approach can also be used to establish the safety of vertical collision avoidance maneuvers for other systems with complex dynamics.

We present a probabilistic model checking approach for evaluating the safety and operational suitability of the Airborne Collision Avoidance System X (ACAS X). This system issues advisories to pilots when the risk of mid-air collision is imminent, and is expected to be equipped on all large, piloted aircraft in the future. We developed an approach to efficiently compute the probabilities of generically specified events and the most likely sequences of states leading to those events within a discrete-time Markov chain model of aircraft flight and ACAS X. The probabilities and sequences are computed for all states in the model. Events of interest include near mid-air collisions (NMACs) and undesirable sequences of advisories that affect operational suitability. We have validated numerous observations of the model with higher-fidelity simulations of the full system. This analysis has revealed several characteristics of ACAS X's behavior.