Karen Leung

ASL Publications

K. Leung, N. Aréchiga, and M. Pavone, “Backpropagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods,” Int. Journal of Robotics Research, vol. 42, no. 6, pp. 356–370, 2023.
[BibTeX] [Abstract]

Abstract: This paper presents a technique, named STLCG, to compute the quantitative semantics of Signal Temporal Logic (STL) formulas using computation graphs. STLCG provides a platform which enables the incorporation of logical specifications into robotics problems that benefit from gradient-based solutions. Specifically, STL is a powerful and expressive formal language that can specify spatial and temporal properties of signals generated by both continuous and hybrid systems. The quantitative semantics of STL provide a robustness metric, that is, how much a signal satisfies or violates an STL specification. In this work, we devise a systematic methodology for translating STL robustness formulas into computation graphs. With this representation, and by leveraging off-the-shelf automatic differentiation tools, we are able to efficiently backpropagate through STL robustness formulas and hence enable a natural and easy-to-use integration of STL specifications with many gradient-based approaches used in robotics. Through a number of examples stemming from various robotics applications, we demonstrate that STLCG is versatile, computationally efficient, and capable of incorporating human-domain knowledge into the problem formulation.
```
@article{LeungArechigaEtAl2021,
  author = {Leung, K. and Ar\'{e}chiga, N. and Pavone, M.},
  title = {Backpropagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods},
  journal = {{Int. Journal of Robotics Research}},
  year = {2023},
  volume = {42},
  number = {6},
  pages = {356--370},
  doi = {10.1177/02783649221082115},
  owner = {jthluke},
  timestamp = {2024-09-20},
  url = {https://arxiv.org/abs/2008.00097}
}
```
K. Leung and M. Pavone, “Semi-Supervised Trajectory-Feedback Controller Synthesis with Signal Temporal Logic Specifications,” in American Control Conference, 2022.
[BibTeX] [Abstract]

Abstract: There are spatio-temporal rules that dictate how robots should operate in complex environments, e.g., road rules govern how (self-driving) vehicles should behave on the road. However, seamlessly incorporating such rules into a robot control policy remains challenging especially for real-time applications. In this work, given a desired spatio-temporal specification expressed in the Signal Temporal Logic (STL) language, we propose a semi-supervised controller synthesis technique that is attuned to human-like behaviors while satisfying desired STL specifications. Offline, we synthesize a trajectory-feedback neural network controller via an adversarial training scheme that summarizes past spatio-temporal behaviors when computing controls, and then online, we perform gradient steps to improve specification satisfaction. Central to the offline phase is an imitation-based regularization component that fosters better policy exploration and helps induce naturalistic human behaviors. Our experiments demonstrate that having imitation-based regularization leads to higher qualitative and quantitative performance compared to optimizing an STL objective only as done in prior work. We demonstrate the efficacy of our approach with an illustrative case study and show that our proposed controller outperforms a state-of-the-art shooting method in both performance and computation time.
```
@inproceedings{LeungPavone2022,
  author = {Leung, K. and Pavone, M.},
  title = {Semi-Supervised Trajectory-Feedback Controller Synthesis with Signal Temporal Logic Specifications},
  booktitle = {{American Control Conference}},
  year = {2022},
  keywords = {pub},
  owner = {karenl7},
  timestamp = {2021-10-14}
}
```
K. Leung, “On Using Formal Methods for Safe and Robust Robot Autonomy,” PhD thesis, Stanford University, Dept. of Aeronautics and Astronautics, Stanford, California, 2021.
[BibTeX] [Abstract]

Abstract: Advances in the fields of artificial intelligence and machine learning have unlocked a new generation of robotic systems—"learning-enabled" robots that are designed to operate in unstructured, uncertain, and unforgiving environments, especially settings where robots are required to interact in close proximity with humans. However, as learning-enabled methods, especially "deep" learning, continue to become more pervasive throughout the autonomy stack, it also becomes increasingly difficult to ascertain the performance and safety of these robotic systems and explain their behavior, necessary prerequisites for their deployment in safety-critical settings. This dissertation develops methods drawing upon techniques from the field of formal methods, namely Hamilton-Jacobi (HJ) reachability and Signal Temporal Logic (STL), to complement a learning-enabled robot autonomy stack, thereby leading to safer and more robust robot behavior. The first part of this dissertation investigates the problem of providing safety assurance for human-robot interactions, safety-critical settings wherein robots must reason about the uncertainty in human behavior to achieve seamless interactions with humans. Specifically, we develop a two-step approach where we first develop a learning-based human behavior prediction model tailored towards proactive robot planning and decision-making, which we then couple with a reachability-based safety controller that minimally intervenes whenever the robot is near safety violation. The approach is validated through human-in-the-loop simulation as well as on an experimental vehicle platform, demonstrating clear connections between theory and practice. The second part of this dissertation examines the use of STL as a formal language to incorporate logical reasoning into robot learning. In particular, we develop a technique, named STLCG, that casts STL into the same computational language as deep neural networks. Consequently, by using STLCG to express designers’ domain expertise into a form compatible with neural networks, we can embed domain knowledge into learned components within the autonomy stack to provide additional levels of robustness and interpretability.
```
@phdthesis{Leung2021,
  author = {Leung, K.},
  title = {On Using Formal Methods for Safe and Robust Robot Autonomy},
  school = {{Stanford University, Dept. of Aeronautics and Astronautics}},
  year = {2021},
  address = {Stanford, California},
  month = aug,
  url = {https://stacks.stanford.edu/file/druid:kk533yj7758/Leung_PhD-augmented.pdf},
  owner = {bylard},
  timestamp = {2021-12-06}
}
```
S. Schaefer, K. Leung, B. Ivanovic, and M. Pavone, “Leveraging Neural Network Gradients within Trajectory Optimization for Proactive Human-Robot Interactions,” in Proc. IEEE Conf. on Robotics and Automation, Xi’an, China, 2021.
[BibTeX] [Abstract]

Abstract: To achieve seamless human-robot interactions, robots need to intimately reason about complex interaction dynamics and future human behaviors within their motion planning process. However, there is a disconnect between state-of-the-art neural network-based human behavior models and robot motion planners—either the behavior models are limited in their consideration of downstream planning or a simplified behavior model is used to ensure tractability of the planning problem. In this work, we present a framework that fuses together the interpretability and flexibility of trajectory optimization (TO) with the predictive power of state-of-the-art human trajectory prediction models. In particular, we leverage gradient information from data-driven prediction models to explicitly reason about human-robot interaction dynamics within a gradient-based TO problem. We demonstrate the efficacy of our approach in a multi-agent scenario whereby a robot is required to safely and efficiently navigate through a crowd of up to ten pedestrians. We compare against a variety of planning methods, and show that by explicitly accounting for interaction dynamics within the planner, our method offers safer and more efficient behaviors, even yielding proactive and nuanced behaviors such as waiting for a pedestrian to pass before moving.
```
@inproceedings{SchaeferLeungEtAl2021,
  author = {Schaefer, S. and Leung, K. and Ivanovic, B. and Pavone, M.},
  title = {Leveraging Neural Network Gradients within Trajectory Optimization for Proactive Human-Robot Interactions},
  booktitle = {{Proc. IEEE Conf. on Robotics and Automation}},
  year = {2021},
  address = {Xi'an, China},
  month = may,
  url = {https://arxiv.org/abs/2012.01027},
  owner = {borisi},
  timestamp = {2020-11-01}
}
```
B. Ivanovic, K. Leung, E. Schmerling, and M. Pavone, “Multimodal Deep Generative Models for Trajectory Prediction: A Conditional Variational Autoencoder Approach,” IEEE Robotics and Automation Letters, vol. 6, no. 2, pp. 295–302, Apr. 2021.
[BibTeX] [Abstract]

Abstract: Human behavior prediction models enable robots to anticipate how humans may react to their actions, and hence are instrumental to devising safe and proactive robot planning algorithms. However, modeling complex interaction dynamics and capturing the possibility of many possible outcomes in such interactive settings is very challenging, which has recently prompted the study of several different approaches. In this work, we provide a self-contained tutorial on a conditional variational autoencoder (CVAE) approach to human behavior prediction which, at its core, can produce a multimodal probability distribution over future human trajectories conditioned on past interactions and candidate robot future actions. Specifically, the goals of this tutorial paper are to review and build a taxonomy of state-of-the-art methods in human behavior prediction, from physics-based to purely data-driven methods, provide a rigorous yet easily accessible description of a data-driven, CVAE-based approach, highlight important design characteristics that make this an attractive model to use in the context of model-based planning for human-robot interactions, and provide important design considerations when using this class of models.
```
@article{IvanovicLeungEtAl2020,
  author = {Ivanovic, B. and Leung, K. and Schmerling, E. and Pavone, M.},
  title = {Multimodal Deep Generative Models for Trajectory Prediction: A Conditional Variational Autoencoder Approach},
  journal = {{IEEE Robotics and Automation Letters}},
  volume = {6},
  number = {2},
  pages = {295--302},
  year = {2021},
  month = apr,
  url = {https://arxiv.org/abs/2008.03880},
  owner = {borisi},
  timestamp = {2020-12-23}
}
```
X. Wang, K. Leung, and M. Pavone, “Infusing Reachability-Based Safety into Planning and Control for Multi-agent Interactions,” in IEEE/RSJ Int. Conf. on Intelligent Robots & Systems, Las Vegas, United States, 2020.
[BibTeX] [Abstract]

Abstract: Within a robot autonomy stack, the planner and controller are typically designed separately, and serve different purposes. As such, there is often a diffusion of responsibilities when it comes to ensuring safety for the robot. We propose that a planner and controller should share the same interpretation of safety but apply this knowledge in a different yet complementary way. To achieve this, we use Hamilton-Jacobi (HJ) reachability theory at the planning level to provide the robot planner with the foresight to avoid entering regions with possible inevitable collision. However, this alone does not guarantee safety. In conjunction with this HJ reachability-infused planner, we propose a minimally-interventional multi-agent safety-preserving controller also derived via HJ-reachability theory. The safety controller maintains safety for the robot without unduly impacting planner performance. We demonstrate the benefits of our proposed approach in a multi-agent highway scenario where a robot car is rewarded to navigate through traffic as fast as possible, and we show that our approach provides strong safety assurances yet achieves the highest performance compared to other safety controllers.
```
@inproceedings{WangLeungEtAl2020,
  author = {Wang, X. and Leung, K. and Pavone, M.},
  title = {Infusing Reachability-Based Safety into Planning and Control for Multi-agent Interactions},
  booktitle = {{IEEE/RSJ Int. Conf. on Intelligent Robots \& Systems}},
  year = {2020},
  url = {https://arxiv.org/pdf/2008.00067.pdf},
  address = {Las Vegas, United States},
  owner = {karenl7},
  timestamp = {2020-10-19}
}
```
K. Leung, E. Schmerling, M. Zhang, M. Chen, J. Talbot, J. C. Gerdes, and M. Pavone, “On Infusing Reachability-Based Safety Assurance within Planning Frameworks for Human-Robot Vehicle Interactions,” Int. Journal of Robotics Research, vol. 39, no. 10–11, pp. 1326–1345, 2020.
[BibTeX] [Abstract]

Abstract: Action anticipation, intent prediction, and proactive behavior are all desirable characteristics for autonomous driving policies in interactive scenarios. Paramount, however, is ensuring safety on the road—a key challenge in doing so is accounting for uncertainty in human driver actions without unduly impacting planner performance. This paper introduces a minimally-interventional safety controller operating within an autonomous vehicle control stack with the role of ensuring collision-free interaction with an externally controlled (e.g., human-driven) counterpart while respecting static obstacles such as a road boundary wall. We leverage reachability analysis to construct a real-time (100Hz) controller that serves the dual role of (1) tracking an input trajectory from a higher-level planning algorithm using model predictive control, and (2) assuring safety through maintaining the availability of a collision-free escape maneuver as a persistent constraint regardless of whatever future actions the other car takes. A full-scale steer-by-wire platform is used to conduct traffic weaving experiments wherein two cars, initially side-by-side, must swap lanes in a limited amount of time and distance, emulating cars merging onto/off of a highway. We demonstrate that, with our control stack, the autonomous vehicle is able to avoid collision even when the other car defies the planner’s expectations and takes dangerous actions, either carelessly or with the intent to collide, and otherwise deviates minimally from the planned trajectory to the extent required to maintain safety.
```
@article{LeungSchmerlingEtAl2019,
  author = {Leung, K. and Schmerling, E. and Zhang, M. and Chen, M. and Talbot, J. and Gerdes, J. C. and Pavone, M.},
  title = {On Infusing Reachability-Based Safety Assurance within Planning Frameworks for Human-Robot Vehicle Interactions},
  journal = {{Int. Journal of Robotics Research}},
  year = {2020},
  volume = {39},
  number = {10--11},
  pages = {1326--1345},
  url = {https://arxiv.org/abs/2012.03390},
  timestamp = {2020-10-13}
}
```
K. Leung, N. Aréchiga, and M. Pavone, “Back-propagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods,” in Workshop on Algorithmic Foundations of Robotics, Oulu, Finland, 2020.
[BibTeX] [Abstract]

Abstract: This paper presents a technique, named stlcg, to compute the quantitative semantics of Signal Temporal Logic (STL) formulas using computation graphs. This provides a platform which enables the incorporation of logic-based specifications into robotics problems that benefit from gradient-based solutions. Specifically, STL is a powerful and expressive formal language that can specify spatial and temporal properties of signals generated by both continuous and hybrid systems. The quantitative semantics of STL provide a robustness metric, i.e., how much a signal satisfies or violates an STL specification. In this work we devise a systematic methodology for translating STL robustness formulas into computation graphs. With this representation, and by leveraging off-the-shelf auto-differentiation tools, we are able to back-propagate through STL robustness formulas and hence enable a natural and easy-to-use integration with many gradient-based approaches used in robotics. We demonstrate, through examples stemming from various robotics applications, that the technique is versatile, computationally efficient, and capable of injecting human-domain knowledge into the problem formulation.
```
@inproceedings{LeungArechigaEtAl2020,
  author = {Leung, K. and Ar\'{e}chiga, N. and Pavone, M.},
  title = {Back-propagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods},
  booktitle = {{Workshop on Algorithmic Foundations of Robotics}},
  year = {2020},
  address = {Oulu, Finland},
  url = {https://arxiv.org/abs/2008.00097v2},
  owner = {karenl7},
  timestamp = {2020-04-09}
}
```
J. DeCastro, K. Leung, N. Aréchiga, and M. Pavone, “Interpretable Policies from Formally-Specified Temporal Properties,” in Proc. IEEE Int. Conf. on Intelligent Transportation Systems, Rhodes, Greece, 2020.
[BibTeX] [Abstract]

Abstract: We present an approach for interpreting parameterized policies based on a formally-specified abstract description of the importance of certain behaviors or observed outcomes of a policy. The standard way to deploy data-driven policies usually involves sampling from the set of outcomes produced by the policy. Our approach leverages parametric signal temporal logic (pSTL) formulas to construct an interpretable view on the modeling parameters via a sequence of variational inference problems; one to solve for the pSTL parameters and another to construct a new parameterization satisfying the specification. We perform clustering using a finite set of examples, either real or simulated, and combine computational graph learning and normalizing flows to form a relationship between these parameters and pSTL formulas either derived by hand or inferred from data. We illustrate the utility of our approach to model selection for validation of the safety properties of an autonomous driving system, using a learned generative model of the surrounding agents.
```
@inproceedings{DeCastroLeungEtAl2020,
  author = {DeCastro, J. and Leung, K. and Ar\'{e}chiga, N. and Pavone, M.},
  title = {Interpretable Policies from Formally-Specified Temporal Properties},
  booktitle = {{Proc. IEEE Int. Conf. on Intelligent Transportation Systems}},
  year = {2020},
  url = {/wp-content/papercite-data/pdf/DeCastro.Leung.ea.ITSC20.pdf},
  address = {Rhodes, Greece},
  timestamp = {2020-10-19}
}
```
K. Leung, N. Aréchiga, and M. Pavone, “Backpropagation for Parametric STL,” in IEEE Intelligent Vehicles Symposium: Workshop on Unsupervised Learning for Automated Driving, Paris, France, 2019.
[BibTeX] [Abstract]

Abstract: Signal Temporal Logic (STL) is an expressive language used to describe logical and temporal properties of signals, both continuous and discrete. Inferring STL formulas from behavior traces can provide powerful insights into complex systems. These insights can help system designers better understand and improve the systems they develop (e.g., long-term behaviors of time series data), yet this is a very challenging and often intractable problem. This work presents a method for evaluating STL formulas using computation graphs, hence bridging a connection between STL and many modern machine learning frameworks that depend on computation graphs, such as deep learning. We show that this approach is particularly effective for solving parameteric STL (pSTL) problems, the problem of parameter fitting for a given signal. We provide a relaxation technique that makes this method more tractable when solving general pSTL formulas. By using computation graphs, we can leverage the benefits and the computational prowess of modern day machine learning tools. Motivated by the problem of learning explanatory factors and safety assurance for complex cyber-physical systems, we demonstrate our proposed method on an autonomous driving case study.
```
@inproceedings{LeungArechigaEtAl2019,
  author = {Leung, K. and Ar\'{e}chiga, N. and Pavone, M.},
  title = {Backpropagation for Parametric {STL}},
  booktitle = {{IEEE Intelligent Vehicles Symposium: Workshop on Unsupervised Learning for Automated Driving}},
  year = {2019},
  address = {Paris, France},
  month = jun,
  url = {/wp-content/papercite-data/pdf/Leung.Arechiga.ea.ULAD19.pdf},
  owner = {karenl7},
  timestamp = {2021-07-12}
}
```

K. Leung, N. Aréchiga, and M. Pavone, “Backpropagation for Parametric STL.” U.S. Patent 62 746 700, Oct-2018.

Abstract:

@misc{LeungArechigaEtAl2018,
  author = {Leung, K. and Ar\'{e}chiga, N. and Pavone, M.},
  title = {Backpropagation for Parametric {STL}},
  howpublished = {{U.S. Patent 62 746 700}},
  month = oct,
  year = {2018},
  timestamp = {2019-08-05}
}

B. Ivanovic, E. Schmerling, K. Leung, and M. Pavone, “Generative Modeling of Multimodal Multi-Human Behavior,” in IEEE/RSJ Int. Conf. on Intelligent Robots & Systems, Madrid, Spain, 2018.
[BibTeX] [Abstract]

Abstract: This work presents a methodology for modeling and predicting human behavior in settings with N humans interacting in highly multimodal scenarios (i.e. where there are many possible highly-distinct futures). A motivating example includes robots interacting with humans in crowded environments, such as self-driving cars operating alongside human-driven vehicles or human-robot collaborative bin packing in a warehouse. Our approach to model human behavior in such uncertain environments is to model humans in the scene as nodes in a graphical model, with edges encoding relationships between them. For each human, we learn a multimodal probability distribution over future actions from a dataset of multi-human interactions. Learning such distributions is made possible by recent advances in the theory of conditional variational autoencoders and deep learning approximations of probabilistic graphical models. Specifically, we learn action distributions conditioned on interaction history, neighboring human behavior, and candidate future agent behavior in order to take into account response dynamics. We demonstrate the performance of such a modeling approach in modeling basketball player trajectories, a highly multimodal, multi-human scenario which serves as a proxy for many robotic applications.
```
@inproceedings{IvanovicSchmerlingEtAl2018,
  author = {Ivanovic, B. and Schmerling, E. and Leung, K. and Pavone, M.},
  title = {Generative Modeling of Multimodal Multi-Human Behavior},
  booktitle = {{IEEE/RSJ Int. Conf. on Intelligent Robots \& Systems}},
  year = {2018},
  address = {Madrid, Spain},
  month = oct,
  url = {https://arxiv.org/pdf/1803.02015.pdf},
  owner = {borisi},
  timestamp = {2018-10-14}
}
```
E. Schmerling, K. Leung, W. Vollprecht, and M. Pavone, “Multimodal Probabilistic Model-Based Planning for Human-Robot Interaction,” in Proc. IEEE Conf. on Robotics and Automation, Brisbane, Australia, 2018.
[BibTeX] [Abstract]

Abstract: This paper presents a method for constructing human-robot interaction policies in settings where multimodality, i.e., the possibility of multiple highly distinct futures, plays a critical role in decision making. We are motivated in this work by the example of traffic weaving, e.g., at highway onramps/offramps, where entering and exiting cars must swap lanes in a short distance — a challenging negotiation even for experienced drivers due to the inherent multimodal uncertainty of who will pass whom. Our approach is to learn multimodal probability distributions over future human actions from a dataset of human-human exemplars and perform real-time robot policy construction in the resulting environment model through massively parallel sampling of human responses to candidate robot action sequences. Direct learning of these distributions is made possible by recent advances in the theory of conditional variational autoencoders (CVAEs), whereby we learn action distributions simultaneously conditioned on the present interaction history, as well as candidate future robot actions in order to take into account response dynamics. We demonstrate the efficacy of this approach with a human-in-the-loop simulation of a traffic weaving scenario.
```
@inproceedings{SchmerlingLeungEtAl2018,
  author = {Schmerling, E. and Leung, K. and Vollprecht, W. and Pavone, M.},
  title = {Multimodal Probabilistic Model-Based Planning for Human-Robot Interaction},
  booktitle = {{Proc. IEEE Conf. on Robotics and Automation}},
  year = {2018},
  address = {Brisbane, Australia},
  month = may,
  url = {/wp-content/papercite-data/pdf/Schmerling.Leung.Vollprecht.Pavone.ICRA18.pdf},
  owner = {schmrlng},
  timestamp = {2017-09-18}
}
```

K. Leung, E. Schmerling, M. Chen, J. Talbot, J. C. Gerdes, and M. Pavone, “On Infusing Reachability-Based Safety Assurance within Probabilistic Planning Frameworks for Human-Robot Vehicle Interactions,” in Int. Symp. on Experimental Robotics, Buenos Aires, Argentina, 2018.

[BibTeX] [Abstract]

Abstract:

@inproceedings{LeungSchmerlingEtAl2018,
  author = {Leung, K. and Schmerling, E. and Chen, M. and Talbot, J. and Gerdes, J. C. and Pavone, M.},
  title = {On Infusing Reachability-Based Safety Assurance within Probabilistic Planning Frameworks for Human-Robot Vehicle Interactions},
  booktitle = {{Int. Symp. on Experimental Robotics}},
  year = {2018},
  address = {Buenos Aires, Argentina},
  url = {/wp-content/papercite-data/pdf/Leung.Schmerling.Chen.ea.ISER18.pdf},
  owner = {mochen72},
  timestamp = {2018-10-13}
}

K. Leung, E. Schmerling, and M. Pavone, “Distributional Prediction of Human Driving Behaviours using Mixture Density Networks,” Stanford University, 2016.
[BibTeX] [Abstract]

Abstract: Confident predictions of human driving behaviours are necessary in designing safe and efficient control policies for autonomous vehicles. A better understanding of how human drivers react to their surrounding may avoid the design of overly-conservative control policies which require greater cost (e.g., time, traffic flow disruption) to achieve their objective. In this paper, we explore ways to learn distributions over human driver actions that are typical of a highway setting. We use actions filtered from Next Generation SIMulation (NGSIM) vehicle trajectory data gathered on the US 101 highway as training data for a Recurrent Neural Network. In particular, we use a Mixture Density Network (MDN) model to represent predicted driver actions as a Gaussian Mixture Model. We present and discuss exploratory results on the filtering of the raw NGSIM data and design of the MDN model.
```
@techreport{LeungSchmerlingEtAl2016,
  author = {Leung, K. and Schmerling, E. and Pavone, M.},
  title = {Distributional Prediction of Human Driving Behaviours using Mixture Density Networks},
  institution = {{Stanford University}},
  year = {2016},
  owner = {bylard},
  timestamp = {2017-01-28},
  url = {/wp-content/papercite-data/pdf/Leung.Schmerling.Pavone.2016.pdf}
}
```

Contacts:

Karen Leung

Awards:

ASL Publications