Robert Reed

About

Hello! I’m Robert, a Ph.D. candidate in the Aerospace Engineering Department at CU Boulder. I’m currently part of the ARIA Systems group advised by Dr. Morteza Lahijanian. Check out our github repo to see what we’ve been up to. Prior to joining ARIA Systems, I spent two years working as a Controls Engineer at Johns Hopkins University Applied Physics Lab. My work there expanded my interests in control theory and encouraged me to delve into research for autonomous systems.

My current research focuses on how to use machine learning techniques to improve the scalability of formal methods. In particular, I consider cases where the dynamics of the system are not well defined due to unmodeled/black-box components and reason about how to learn and verify a model from data. My regression model of choice is the Gaussian Process, which has the rigorous uncertainty quantification we need to reason in a formal manner; check out my papers to see how they can be used even without Gaussian noise and how to incorporate a deep architecture to increase their expressivity! Outside of regression, my research interests include Formal Methods, Verification of Autonomous Systems, Control Theory, Reinforcement Learning, and Neural Network Verificaiton.

---

Publications

1. R. Reed, L. Laurenti, and M. Lahijanian, “Scalable Formal Verification via Autoencoder Latent Space Abstraction,” 2026. Under Review
   
   pdf

   Abstract

   Finite Abstraction methods provide a powerful formal framework for proving that systems satisfy their specifications. However, these techniques face scalability challenges for high-dimensional systems, as they rely on state-space discretization which grows exponentially with dimension. Learning-based approaches to dimensionality reduction, utilizing neural networks and autoencoders, have shown great potential to alleviate this problem. However, ensuring the correctness of the resulting verification results remains an open question. In this work, we provide a formal approach to reduce the dimensionality of systems via convex autoencoders and learn the dynamics in the latent space through a kernel-based method. We then construct a finite abstraction from the learned model in the latent space and guarantee that the abstraction contains the true behaviors of the original system. We show that the verification results in the latent space can be mapped back to the original system. Finally, we demonstrate the effectiveness of our approach on multiple systems, including a 26D system controlled by a neural network, showing significant scalability improvements without loss of rigor.

   BibTeX

   @inproceedings{Reed:HSCC:2026,
     title = {Scalable Formal Verification via Autoencoder Latent Space Abstraction},
     author = {Reed, Robert and Laurenti, Luca and Lahijanian, Morteza},
     note = {Under Review},
     year = {2026},
     url = {https://arxiv.org/abs/2512.13593}
   }
   

2. R. Reed and M. Lahijanian, “Learning-Based Shielding for Safe Autonomy under Unknown Dynamics,” in American Control Conference (ACC), Denver, CO, USA, 2025.
   
   pdf publisher

   Abstract

   Shielding is a common method used to guarantee the safety of a system under a black-box controller, such as a neural network controller from deep reinforcement learning (DRL), with simpler, verified controllers. Existing shielding methods rely on formal verification through Markov Decision Processes (MDPs), assuming either known or finite-state models, which limits their applicability to DRL settings with unknown, continuous-state systems. This paper addresses these limitations by proposing a data-driven shielding methodology that guarantees safety for unknown systems under black-box controllers. The approach leverages Deep Kernel Learning to model the systems’ one-step evolution with uncertainty quantification and constructs a finite-state abstraction as an Interval MDP (IMDP). By focusing on safety properties expressed in safe linear temporal logic (safe LTL), we develop an algorithm that computes the maximally permissive set of safe policies on the IMDP, ensuring avoidance of unsafe states. The algorithms soundness and computational complexity are demonstrated through theoretical proofs and experiments on nonlinear systems, including a high-dimensional autonomous spacecraft scenario.

   BibTeX

   @inproceedings{Reed:ACC:2025,
     title = {Learning-Based Shielding for Safe Autonomy under Unknown Dynamics},
     author = {Reed, Robert and Lahijanian, Morteza},
     booktitle = {American Control Conference (ACC)},
     month = jul,
     year = {2025},
     organization = {IEEE},
     address = {Denver, CO, USA},
     note = {},
     doi = {10.23919/ACC63710.2025.11108000},
     url = {https://arxiv.org/abs/2410.07359}
   }
   

3. R. Reed, L. Laurenti, and M. Lahijanian, “Error Bounds For Gaussian Process Regression Under Bounded Support Noise With Applications To Safety Certification,” in The Thirty-Ninth AAAI Conference on Artificial Intelligence (AAAI), Philadelphia, Pennsylvania, USA, 2025, vol. 39, no. 19, pp. 20157–20164.
   
   pdf publisher video

   Abstract

   Gaussian Process Regression (GPR) is a powerful and elegant method for learning complex functions from noisy data with a wide range of applications, including in safety-critical domains. Such applications have two key features: (i) they require rigorous error quantification, and (ii) the noise is often bounded and non-Gaussian due to, e.g., physical constraints. While error bounds for applying GPR in the presence of non-Gaussian noise exist, they tend to be overly restrictive and conservative in practice. In this paper, we provide novel error bounds for GPR under bounded support noise. Specifically, by relying on concentration inequalities and assuming that the latent function has low complexity in the reproducing kernel Hilbert space (RKHS) corresponding to the GP kernel, we derive both probabilistic and deterministic bounds on the error of the GPR. We show that these errors are substantially tighter than existing state-of-the-art bounds and are particularly well-suited for GPR with neural network kernels, i.e., Deep Kernel Learning (DKL). Furthermore, motivated by applications in safety-critical domains, we illustrate how these bounds can be combined with stochastic barrier functions to successfully quantify the safety probability of an unknown dynamical system from finite data. We validate the efficacy of our approach through several benchmarks and comparisons against existing bounds. The results show that our bounds are consistently smaller, and that DKLs can produce error bounds tighter than sample noise, significantly improving the safety probability of control systems.

   BibTeX

   @inproceedings{Reed:AAAI:2025,
     title = {Error Bounds For Gaussian Process Regression Under Bounded Support Noise With Applications To Safety Certification},
     author = {Reed, Robert and Laurenti, Luca and Lahijanian, Morteza},
     booktitle = {The Thirty-Ninth AAAI Conference on Artificial Intelligence (AAAI)},
     year = {2025},
     volume = {39},
     number = {19},
     pages = {20157--20164},
     month = feb,
     address = {Philadelphia, Pennsylvania, USA},
     publisher = {{AAAI} Press},
     url = {https://arxiv.org/abs/2408.09033},
     note = {},
     doi = {https://doi.org/10.1609/aaai.v39i19.34220},
     videourl = {https://youtu.be/7TsMPE3tyBM},
     bibkey = {synth-ml}
   }
   

4. R. Reed, H. Schaub, and M. Lahijanian, “Shielded Deep Reinforcement Learning for Complex Spacecraft Specifications,” in American Control Conference (ACC), Toronto, Canada, 2024, pp. 2331–2337.
   
   pdf publisher

   Abstract

   Autonomous spacecraft control via Shielded Deep Reinforcement Learning (SDRL) has become a rapidly growing research area. However, the construction of shields and the definition of tasking remains informal, resulting in policies with no guarantees on safety and ambiguous goals for the RL agent. In this paper, we first explore the use of formal languages, namely Linear Temporal Logic (LTL), to formalize spacecraft tasks and safety requirements. We then define a manner in which to construct a reward function from a co-safe LTL specification automatically for effective training in SDRL framework. We also investigate methods for constructing a shield from a safe LTL specification for spacecraft applications and propose three designs that provide probabilistic guarantees. We show how these shields interact with different policies and the flexibility of the reward structure through experimentation.

   BibTeX

   @inproceedings{Reed:ACC:2024,
     title = {Shielded Deep Reinforcement Learning for Complex Spacecraft Specifications},
     author = {Reed, Robert and Schaub, Hanspeter and Lahijanian, Morteza},
     booktitle = {American Control Conference (ACC)},
     month = jul,
     year = {2024},
     pages = {2331-2337},
     organization = {IEEE},
     address = {Toronto, Canada},
     doi = {10.23919/ACC60939.2024.10644855},
     note = {},
     url = {https://arxiv.org/abs/2403.05693}
   }
   

5. R. Reed, L. Laurenti, and M. Lahijanian, “Promises of Deep Kernel Learning for Control Synthesis,” IEEE Control Systems Letters, vol. 7, pp. 3986–3990, Dec. 2023.
   
   pdf publisher

   Abstract

   Deep Kernel Learning (DKL) combines the representational power of neural networks with the uncertainty quantification of Gaussian Processes. Hence, it is potentially a promising tool to learn and control complex dynamical systems. In this letter, we develop a scalable abstraction-based framework that enables the use of DKL for control synthesis of stochastic dynamical systems against complex specifications. Specifically, we consider temporal logic specifications and create an end-to-end framework that uses DKL to learn an unknown system from data and formally abstracts the DKL model into an interval Markov decision process to perform control synthesis with correctness guarantees. Furthermore, we identify a deep architecture that enables accurate learning and efficient abstraction computation. The effectiveness of our approach is illustrated on various benchmarks, including a 5-D nonlinear stochastic system, showing how control synthesis with DKL can substantially outperform state-of-the-art competitive methods.

   BibTeX

   @article{Reed:LCSS:2023,
     author = {Reed, Robert and Laurenti, Luca and Lahijanian, Morteza},
     journal = {IEEE Control Systems Letters},
     title = {Promises of Deep Kernel Learning for Control Synthesis},
     year = {2023},
     month = dec,
     volume = {7},
     number = {},
     pages = {3986-3990},
     doi = {10.1109/LCSYS.2023.3340995},
     url = {https://arxiv.org/abs/2309.06569}
   }
   

---

CV

You can find a copy of my CV here.

---

Contact

Email (Work) Robert.Reed-1@colorado.edu

Mailing Address Ann & H.J. Smead Department of Aerospace Engineering Sciences
University of Colorado Boulder
Boulder, CO 80303
USA

---