Skip to main content
eScholarship
Open Access Publications from the University of California

Scholarly Works (13 results)

  • Article
  • Peer Reviewed
UC Berkeley Previously Published Works (2020)
In many settings, such as robotics, demonstrations provide a natural way to specify tasks. However, most methods for learning from demonstrations either do not provide guarantees that the learned artifacts can be safely composed or do not explicitly capture temporal properties. Motivated by this deficit, recent works have proposed learning Boolean task specifications, a class of Boolean non-Markovian rewards which admit well-defined composition and explicitly handle historical dependencies. This work continues this line of research by adapting maximum causal entropy inverse reinforcement learning to estimate the posteriori probability of a specification given a multi-set of demonstrations. The key algorithmic insight is to leverage the extensive literature and tooling on reduced ordered binary decision diagrams to efficiently encode a time unrolled Markov Decision Process. This enables transforming a naïve algorithm with running time exponential in the episode length, into a polynomial time algorithm.
    Cover page: Maximum Causal Entropy Specification Inference from Demonstrations
    • Thesis
    • Peer Reviewed
    UC Berkeley Electronic Theses and Dissertations (2022)

    This dissertation considers the problem of learning and teaching Boolean task specifications, such as automata, using demonstrations. The resulting framework bridges grammatical inference and maximum-entropy inverse reinforcement learning with applications in human-robot interaction, formal synthesis, and multi-task reinforcement learning.

    In the context of inverse reinforcement learning, Boolean task specifications are a class of sparse memory augmented rewards with explicit support for temporal and Boolean composition. These properties make task specifications immune to certain classes of reward hacking bugs that emerge from ad-hoc composition or perturbations to the dynamics. Unfortunately, the discrete nature of task specifications combined with an a-priori ignorance of what historical features are needed to encode the demonstrated task make existing approaches to learning rewards from demonstrations inapplicable.

    In the context of specification mining and grammatical inference, demonstrations provide an ergonomic and sample efficient means to communicate formal languages and specifications. For example, this dissertation enables a user to partially specify the desired behavior of a system as example demonstrations and then find an automata or program that explains the user's behavior. Conversely, by synthesizing pedagogic demonstrations, this dissertation enables communicating the nuances of a specification that may be hard to intuit from a formal description.

    In either case, this thesis contributes a collection of algorithms and theoretical machinery for systematically mitigating combinatorial explosions inherent in (1) finding specifications that explain an agent's behavior (2) finding pedagogic demonstrations that help humans infer the specification and (3) robustly predicting the behavior of an agent adhering to a specification.

      Cover page: Specifications from Demonstrations: Learning, Teaching, and Control
      • Article
      • Peer Reviewed
      UC Berkeley Previously Published Works (2021)
      High level declarative constraints provide a powerful (and popular) way to define and construct control policies; however, most synthesis algorithms do not support specifying the degree of randomness (unpredictability) of the resulting controller. In many contexts, e.g., patrolling, testing, behavior prediction, and planning on idealized models, predictable or biased controllers are undesirable. To address these concerns, we introduce the Entropic Reactive Control Improvisation (ERCI) framework and algorithm which supports synthesizing control policies for stochastic games that are declaratively specified by (i) a hard constraint specifying what must occur, (ii) a soft constraint specifying what typically occurs, and (iii) a randomization constraint specifying the unpredictability and variety of the controller, as quantified using causal entropy. This framework, which extends the state of the art by supporting arbitrary combinations of adversarial and probabilistic uncertainty in the environment. ERCI enables a flexible modeling formalism which we argue, theoretically and empirically, remains tractable.
        Cover page: Entropy-Guided Control Improvisation
        • Article
        • Peer Reviewed
        UC Berkeley Previously Published Works (2018)
        Cyber-physical systems of today are generating large volumes of time-series data. As manual inspection of such data is not tractable, the need for learning methods to help discover logical structure in the data has increased. We propose a logic-based framework that allows domain-specific knowledge to be embedded into formulas in a parametric logical specification over time-series data. The key idea is to then map a time series to a surface in the parameter space of the formula. Given this mapping, we identify the Hausdorff distance between surfaces as a natural distance metric between two time-series data under the lens of the parametric specification. This enables embedding nontrivial domain-specific knowledge into the distance metric and then using off-the-shelf machine learning tools to label the data. After labeling the data, we demonstrate how to extract a logical specification for each label. Finally, we showcase our technique on real world traffic data to learn clas-sifiers/monitors for slow-downs and traffic jams.
          Cover page: Time-Series Learning Using Monotonic Logical Properties
          • Article
          • Peer Reviewed
          UC Berkeley Previously Published Works (2019)
          We present VerifAI, a software toolkit for the formal design and analysis of systems that include artificial intelligence (AI) and machine learning (ML) components. VerifAI particularly addresses challenges with applying formal methods to ML components such as perception systems based on deep neural networks, as well as systems containing them, and to model and analyze system behavior in the presence of environment uncertainty. We describe the initial version of VerifAI, which centers on simulation-based verification and synthesis, guided by formal models and specifications. We give examples of several use cases, including temporal-logic falsification, model-based systematic fuzz testing, parameter synthesis, counterexample analysis, and data set augmentation.
            Cover page: VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
            • Article
            • Peer Reviewed
            UC Berkeley Previously Published Works (2018)
            Real-world applications often naturally decompose into several sub-tasks. In many settings (e.g., robotics) demonstrations provide a natural way to specify the sub-tasks. However, most methods for learning from demonstrations either do not provide guarantees that the artifacts learned for the sub-tasks can be safely recombined or limit the types of composition available. Motivated by this deficit, we consider the problem of inferring Boolean non-Markovian rewards (also known as logical trace properties or specifications) from demonstrations provided by an agent operating in an uncertain, stochastic environment. Crucially, specifications admit well-defined composition rules that are typically easy to interpret. In this paper, we formulate the specification inference task as a maximum a posteriori (MAP) probability inference problem, apply the principle of maximum entropy to derive an analytic demonstration likelihood model and give an efficient approach to search for the most likely specification in a large candidate pool of specifications. In our experiments, we demonstrate how learning specifications can help avoid common problems that often arise due to ad-hoc reward composition.
              Cover page: Learning Task Specifications from Demonstrations
              • Article
              • Peer Reviewed
              UC Berkeley Previously Published Works (2019)
              We present VerifAI, a software toolkit for the formal design and analysis of systems that include artificial intelligence (AI) and machine learning (ML) components. VerifAI particularly addresses challenges with applying formal methods to ML components such as perception systems based on deep neural networks, as well as systems containing them, and to model and analyze system behavior in the presence of environment uncertainty. We describe the initial version of VerifAI, which centers on simulation-based verification and synthesis, guided by formal models and specifications. We give examples of several use cases, including temporal-logic falsification, model-based systematic fuzz testing, parameter synthesis, counterexample analysis, and data set augmentation.
                Cover page: VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
                • Article
                • Peer Reviewed
                UC Berkeley Previously Published Works (2018)
                  Cover page: Time-Series Learning Using Monotonic Logical Properties.
                  • Article
                  • Peer Reviewed
                  UC Berkeley Previously Published Works (2018)
                  Motivated by the synthesis of controllers from high-level temporal specifications, we present two algorithms to compute dominant strategies for continuous two-player zero-sum games based on the Counter-Example Guided Inductive Synthesis (CEGIS) paradigm. In CEGIS, we iteratively propose candidate dominant strategies and find counterexamples. For scalability, past work has constrained the number of counterexamples used to generate new candidates, which leads to oscillations and incompleteness, even in very simple examples. The first algorithm combines Satisfiability Modulo Theory (SMT) solving with optimization to efficiently implement CEGIS. The second abstracts previously refuted strategies, while maintaining a finite counterexample set. We characterize sufficient conditions for soundness and termination, and show that both algorithms are sound and terminate. Additionally, the second approach can be made complete to within an arbitrary factor. We conclude by comparing across different variants of CEGIS.
                    Cover page: Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games
                    • Article
                    • Peer Reviewed
                    UC Berkeley Previously Published Works (2022)
                      Cover page: Modeling and Influencing Human Attentiveness in Autonomy-to-Human Perception Hand-offs
                      Top