Artificial Intelligence and Formal Methods Join Forces for Reliable Autonomy

To perform autonomously tasks such as object rearrangement, manipulation, and navigation, robots must be able to plan their actions over long horizons. Such planning is usually computationally challenging, especially considering complex robots and task specifications, or large planning domains, with many irrelevant objects and distractions. Hence, to support long-lived, multi-purpose planning agents, it is important to allow them to continually improve their planning capabilities from successful planning experience. To this end, our recent work, which will be covered in this talk, introduced a novel computational framework for online, automatic encoding of individual planning experiences as generalizable “abstract strategies;” such a strategy can later be adapted for and reused in new contexts, to accelerate the solution of new planning problems. This domain-independent approach is categorically different from standard techniques for “skill learning” or “learning from demonstration”, which consider offline policy learning from numerous demonstrations. In contrast, our suggested technique allows us to perform strategy extraction in real time from only a single experience, without human intervention.

Partially observable Markov decision processes (POMDPs) capture sequential decision-making in uncertain, partially observable environments. Since state observations are not Markovian, high-quality policies require reasoning about the history of the system’s observations, i.e., they require memory. In this talk, we highlight recent advances in computing policies for robust and multi-agent extensions of POMDPs.

Firstly, we presented recent work on robust POMDPs. A policy for a robust POMDP is called robust when it accounts for the worst-case among an infinite set of POMDPs encapsulated by the so-called uncertainty set of the robust POMDP. We introduce the pessimistic iterative planning (PIP) framework to compute robust policies by iteratively selecting the worst-case POMDP for the current policy from the uncertainty set [2]. We implement PIP in rFSCNet, an algorithm that optimizes a recurrent neural network to compute such robust policies. Empirical results show that the approach is promising and can outperform various baselines and a state-of-the-art planner for robust POMDPs.

Finally, we summarized recent work on computing policies for centralized multi-agent POMDPs with many agents. Multi-agent POMDPs are typically large POMDPs with an agent-wise factorization in their action and observation spaces. We consider the case where the agents share their belief distribution over the state and value function, but interactions between the agents adhere to or can be approximated by a sparse graphical structure. We utilize the sparse interactions among agents in sampled-based online planning approaches, exploiting it in the Monte Carlo estimates of both the value function and the belief distributions maintained by the agents. Thereby, we extend existing sample-based planners to operate in settings where many agents are involved [1].

This talk addresses the challenges that arise in multi-agent systems that are faced both with uncertainty and constraints. We first discuss the problem of resource allocation in factored, multi-agent Markov Decision Processes by enumerating a few different risk-constrained optimization objectives. We then propose a solution to one such objective, chance-constrained optimization, via an auction mechanism that allocates both resources and uncertainty. Finally, we consider how humans in these systems might perceive the risk-taking carried out by AI agents. We present a user study that tests humans’ tolerance for risk in a collaborative block stacking task.

This tutorial provides an in-depth exploration of robot learning, focusing on how machine learning techniques enable robots to learn and adapt through interaction with their environments. It covers core methods in imitation learning (IL), such as behavior cloning and addressing distribution shifts, and extends to advanced topics like generative models and privileged teachers. Additionally, the tutorial delves into reinforcement learning (RL) strategies, highlighting approaches such as Deep Q-learning, Proximal Policy Optimization (PPO), and Soft Actor-Critic (SAC). The ultimate goal discussed is what are the techniques that we currently investigate in the field of robot learning for equipping robots with general-purpose embodied intelligence, empowering them to autonomously handle dynamic, real-world tasks through continuous learning.

Defining soft preferences for motion planning (MP) in Signal Temporal Logic works to some extent by using robustness. However, undesired paths may still be considered optimal in terms of robustness. To address this, we introduce a new family of temporal logics specifically designed for soft preferences. This logic naturally expresses path segments and handles degrees of satisfaction more flexibly. Built on fuzzy, time-varying signal constraints, it offers greater expressivity, making it (i) more intuitive for human-given specifications in MP, and (ii) more suitable for learning specifications from demonstrations compared to other logics.

Mission planning for long-term robot deployments is an extremely challenging problem that requires close integration between machine learning and model-based reasoning techniques. We propose explicitly considering the long-term learning and the mission-level behaviour planning and execution as two tightly coupled components. Each of these components has specific roles in enabling intelligent and adaptive robots. We describe a framework where the long-term autonomy component uses gathered data to learn possible models of the environment dynamics, and the mission-planning component synthesises plans that explicitly consider that the learnt models are underspecified and uncertain. These plans should be able to use online observations to refine their estimates over the underlying true model, thus adapting to deployment-time conditions. We describe recent research related to each of these components, and discuss how frameworks that encompass both in an integrated fashion can be developed.

In this tutorial talk, we consider probabilistic verification of Markov decision processes (MDPs). In short, this means that consider approaches that take an MDP in a suitable format and a temporal specification on that MDP and ask whether the specification holds on the MDP. In this talk, we cover three areas.

(1) Probabilistic model checking (PMC). PMC has emerged as a toolbox with algorithmic support for a wide variety of specifications. Under the hood, PMC relies on solving undiscounted Bellman equations. The PMC community provides a variety of mutually compatible tools, most prominently Storm and PRISM. (2) Novel methods in probabilistic verification. We discuss more recent ideas whose methods have different performance characteristics. In particular, we consider (a) inductive synthesis for inductive invariants in probabilistic models that search for a proof that a property holds, (b) methods from probabilistic inference, in particular using BDD-based model counting, and (c) compositional reasoning in MDPs. (3) Uncertainty on top of probabilistic models, such as parametric MDPs and their application in Bayesian reasoning as well as sensitivity analysis as well as the simultaneous verification of many MDPs with the tool PAYNT.

This talk introduces an offline and an online preference learning method that ensures adherence to given specifications, with an application to autonomous vehicles. Our approach incorporates the priority ordering of Signal Temporal Logic (STL) formulas describing traffic rules into a learning framework. By leveraging Weighted Signal Temporal Logic (WSTL), we formulate the problem of safety-guaranteed preference learning based on pairwise comparisons and propose two approaches to solve this learning problem. The learned valuations lead to a WSTL formula that can be used in correct-and-custom-by-construction controller synthesis. We demonstrate the performance of our method with two pilot human subject studies in different simulated driving scenarios.

This talk outlines the content of a new textbook called Algorithms for Validation. This book provides a broad introduction to algorithms for validating safety-critical systems. We cover a wide variety of topics related to validation, introducing the underlying mathematical problem formulations and the algorithms for solving them.

The first part of this talk is an experience report on how Bosch brings formal methods to autonomous systems engineering. We strive at making formal methods efficiently applicable in industry, especially in autonomous driving and robotics. We report on our experiences and findings gained in industrial research projects in which we developed and analyzed formal methods tooling for the application in industrial case studies. These works provided insights how formal methods can be made attractive for industry. At the same time, they raised challenging research questions to overcome recurring problems which often still prevent practical applicability of formal methods in industry. In more detail, we report on how we applied search-based testing in automated driving control applications in several use cases, how we developed a formally verifiable DSL, called vTSL, for the specification of robot tasks by end-users, and how we automatically generate a formal model from the system code of a behavior planner of an autonomous car to apply model checking during development.

The second part of the talk is about the EU Horizon project CONVINCE, where we show that formal methods are also of great help to achieve robust deliberation capabilities of autonomous robots. We discuss the challenges we are currently facing, ideas on how to even better integrate formal verification, learning, and robotics, and potential topics for collaborations.

This talk presents some of the main challenges in making POMDPs practical for robotics and a brief overview of our work in alleviating those challenges. I hope this talk elucidates what we can now do with POMDPs.

Autonomous systems require reliable controllers that address complex specification and complex system dynamics. Optimization-based control methods, such as model predictive control, provide a systematic method that can ensure safe operation for such challenging environments. In this talk, I show how machine learning methods can address the following challenges: uncertain environments; uncertain dynamics; and efficient implementation. All methods leverage non-parametric function regression, corresponding error bounds, and guarantee safe operation (with high probability) for the resulting closed-loop system. In a second part, I discuss large open questions, such as fragility of online learning in control.

Learning-enabled autonomous systems promise to enable many future technologies such as autonomous driving, intelligent transportation, and robotics. Accelerated by algorithmic and computational advances in machine learning and AI, there has been tremendous success in the design of learning-enabled autonomous systems. However, these exciting developments are accompanied by new fundamental challenges that arise regarding the safety and reliability of these increasingly complex control systems in which sophisticated algorithms interact with unknown dynamic environments. Imperfect learning and unknowns in the environment require control techniques to rigorously account for such uncertainties. I advocate for the use of conformal prediction (CP) – a statistical tool for uncertainty quantification – due to its simplicity, generality, and efficiency as opposed to existing optimization techniques that are either conservative or subject to scalability issues. I first provide an accessible introduction to CP for the non-expert. My goal is then to show how we can use CP to design probabilistically safe motion planning algorithms in dynamic environments. Specifically, we will design a model predictive controller in conjunction with (i) learning-enabled trajectory predictors to obtain predictions of the environment, and (ii) conformal prediction regions quantifying uncertainty of these predictions. We will also discuss how to deal with distribution shifts that arise when the deployed learning-enabled system changes. While existing approaches quantify uncertainty heuristically, we quantify uncertainty in a distribution-free manner with probabilistic safety guarantees. Finally, we provide an extension that enables the consideration of high-level formal system specifications via mixed integer linear programing.

In this talk, I will present a blue-sky idea that builds towards learning provably correct concepts from raw data based on causal representation learning. In many settings, we might have datasets that have spurious correlations between the concept we are interested in learning and other irrelevant features, which might result in a machine learning method showing perfect performance on the dataset, despite learning the wrong concept, which is often referred to as shortcut learning. Marconato et al. [1] show that this issue can be even worse in neurosymbolic predictors, when we do not have access to the labels of the concepts, but we only have access to a label of a constraint on the concepts, e.g. a safety constraint. In safety-critical settings learning these concepts wrongly could potentially lead to misplaced confidence in the safety of neurosymbolic systems. As one of the mitigation strategies in this case Marconato et al. [1] propose the use of disentangled representation learning methods, which are based on the assumptions that the underlying concepts are independent in the underlying data.

Inspired by this work, in this talk I will describe a few similar ideas, focusing first on the simpler case of learning concepts when we have labels for the individual concepts, but allowing for concepts that might have (spurious) correlations in the data. In particular, I will describe a potential pipeline that builds on the recent advances in causal representation learning in interactive temporal settings. Causal representation learning (CRL) aims at identifying high level causal variables (e.g. concepts) from high-dimensional raw data, e.g. images, up to a class of transformations. BISCUIT [2] is a promising CRL approach that leverages actions in an environment to learn a disentangled representation of the causal variables, even when they are correlated with each other. In this representation, each set of latent variables that is assigned to an individual causal variable or concept is guaranteed to have no information about any other causal variable, allowing us to manipulate the reconstructed causal variables as independent factors of variation.

Assuming that the concepts we want to learn are represented by the causal variables in this disentangled representation, we can now split the problem in two phases: a first phase with unlabelled data in which we learn a causal representation with disentanglement guarantees, and a second phase in which we use a small number of labeled data to learn simple alignment functions for each individual concept. This allows us to avoid learning shortcuts in which we wrongly use an irrelevant concept instead of the correct one. Additionally, since for each concept we are learning simpler functions in low-dimensional spaces, instead of learning a potentially complex function directly from the high-dimensional data, this requires less labeled data and it might ideally simplify verifying the correctness of each of these functions or reliably characterize the uncertainty in the prediction.

Further interesting directions include devising active learning strategies to select the most informative actions in the environment to learn these alignment functions, as well as selecting actions that maximally improve the joint learning of causal representations and the alignment functions, progressively learning more and more disentangled representations. Finally, in this active learning setting, we also consider the challenging case in which we do not have (all) concept labels, but only labels on a downstream task involving the concepts, e.g. a constraint.

Autonomous robots should efficiently and reliably learn new skills while reusing experiences. What is limiting the advancement of robotic autonomy? Autonomy has rapidly increased with the development of Interpretable and Explainable methods. Interpretable methods focus on understanding how the learned model reaches decisions by examining its structure and relationships. Explainable methods reveal why a model made specific decisions without requiring an understanding of the model itself. Combining these methods in robotic systems enhances the transparency of decision-making processes. While challenging, Interpretable and Explainable capabilities are crucial for deploying Robots in real and dynamic environments. In this talk, I will first introduce our interpretable AI methods that generate compact and general semantic models to infer human activities, enabling robots to gain a high-level understanding of human movements. Next, I will present our causal-based approach, which empowers robots to rapidly predict and prevent both immediate and future failures. This method helps robots understand why failures occurred, allowing them to learn from their mistakes, thus improving their future performances. Finally, I will discuss strategies for combining these methods into a single framework by integrating symbolic planning with hierarchical Reinforcement Learning. This integration allows us to learn flexible and reusable robot policies for manipulation tasks, creating holistic sequences of actions that can be executed independently. Interpretable and Explainable AI are key to developing general-purpose robots. These approaches enable robots to make complex decisions in dynamic and unpredictable environments by learning “how” and “why”, ultimately improving robotic autonomy.

Developments in AI methods continuously motivate to advance existing approaches in robotics towards increased versatility. This talk looks into different concrete examples at Bosch from recent years, ranging from learning-based task allocation in multi-agent systems over motion skill optimization and sequencing in robotic assembly, model-free grasping and life-long learning in robotic bin picking, up to language-based planning agents with active perception.

We confront the limitations inherent in specifying the behavior expected from a reinforcement learning agent solely via a reward function. We introduce a model that mitigates this issue using constraints, and we discuss two novel ways to learn an optimal policy while minimizing the safety constraint violation. The first is a transfer approach that can efficiently and safely explore the environment [1]. The second is a safe curriculum generation framework, which reduces the safety violations of a constrained agent by gradually increasing the difficulty of the underlying tasks.

In risk-aware motion planning for autonomous systems, it is common to pose an optimization problem that captures both system performance and safety/risk. A typical formulation is to maximize system performance subject to safety constraints. However, typically, one cannot guarantee absolute safety, and thus the constraints contain user-specified thresholds or parameters. In this talk, we will discuss whether this is the “right” way to solve risk-aware planning, or if tools from multi-objective optimization might offer alternatives that allow us better explore the trade-off between performance and risk.

In recent years, there has been an increase in autonomous systems operating in complex environments and relying on machine learning (ML) components to perform challenging decision-making tasks. However, ML models are brittle and susceptible to failures that can compromise the safety of autonomous systems. There is a pressing need for a systematic methodology that can identify the conditions in which components in the autonomy pipeline can fail at design time and detect such failures at runtime.

This talk introduces safety assurance approach for autonomous systems based on runtime verification. Runtime verification is an analysis technique based on extracting information from a system at runtime and evaluating this information to determine whether an execution of the system satisfies or violates a given property. Specifically, we will report on recent results, presenting runtime verification methods for capturing the operational design domains, i.e., the conditions under which the system or a component thereof is designed to operate safely, and for evaluating the safety of a system in noisy and unpredictable environments.

Specifications in linear temporal logic (LTL) offer a simplified way of specifying tasks for policy optimization that may otherwise be difficult to describe with scalar reward functions. However, the standard RL frameworks can be too myopic to find maximally satisfying policies. In this talk we will discuss eventual discounting, a value-function based proxy under which one can find policies that satisfy a specification with highest achievable probability. To improve the efficiency of learning from specifications we combine eventual discounting with LTL-guided Counterfactual Experience Replay, a method for generating off-policy data from on-policy rollouts via counterfactual reasoning. Finally, we will discuss a mechanism for exploiting the compositionality of a specification to provide formal guarantees on the behavior of learnt policies for reach-avoid tasks.

With the increased use of autonomy in safety-critical applications, it is crucial to develop safe and adaptable systems. This talk first introduces an assured runtime safety monitoring technique that draws ideas from machine learning, reachability analysis, and verification techniques to assess the safety of an autonomous robot under disturbance. It then continues with a neural network controller verification approach that uses backward reachability to verify the closed-loop system safety of the system. The talk then touches on adaptability and introduces a technique to relate an unseen condition for an autonomous vehicle to previous experiences to generate policies for novel conditions. Finally, it concludes with a discussion of future research directions and challenges.