CPS-IoT Week 2025 Keynotes

Date: May 7, 2025, 9 am - 10 am

Trusted AI on Mars

Speaker: Dr. Steve Chien, Jet Propulsion Laboratory, California Institute of Technology

Abstract: In October 2023, the Onboard Planner (OBP) took control of the Perseverance rover on Mars, over 200 million miles from Earth. As of 29th January 2025, OBP has operated for 429 Martian days (sols) and has: executed over 7800 activities requested by scientists and engineers, driven over 12 kilometers, acquired over 70,000 images, and collected 4 rock core samples. In contrast to the traditional form of operations, where operators provide a rigid set of instructions for the rover, with OBP Perseverance revises its schedule an average of 16 times each day to stay responsive in a dynamic Martian environment where things don’t always go as expected. This flexibility allows the mission to manage resources such as energy more efficiently and therefore accomplish more science.

In this talk, we discuss the approach to ensuring that a search-based AI system, specifically the Onboard Planner, would (1) achieve mission objectives; and critically (2) protect the rover, a multi-billion dollar one of a kind asset. We describe the “whole lifecycle” approach to developing trusted autonomy software for M2020, spanning: conception, design, analysis, prototyping, and testing. We then describe the incremental rollout and training to smooth the transition to operations with increased onboard autonomy. Next we discuss how the OBP software has performed. Finally we describe the even greater challenges of autonomy in future missions to hunt for life beyond Earth.

Bio: Steve Chien is a Technical Fellow in Artificial Intelligence and Co-head of the Artificial Intelligence Group at the Jet Propulsion Laboratory, California Institute of Technology. He has spent decades deploying AI/Autonomy to numerous space missions including: Earth Observing One, Sensorweb, ESA’s Rosetta Orbiter, and M2020. He has been awarded four NASA Medals in 1997, 2000, 2007, and 2015 for development and deployment of AI technologies for space missions. He has supported numerous government bodies including the Defense Science Board and the Air Force Scientific Advisory Board. He was appointed by Congress to the National Security Commission on Artificial Intelligence (2018-2021). He currently serves on the Army Science Board and as an Advisor to the Senate Defense Modernization Caucus.

---

Date: May 9, 2025, 9 am - 10 am

Towards a Design Flow for Verified AI-Based Autonomy

Speaker: Professor Sanjit A. Seshia, University of California, Berkeley, USA

Abstract: Verified artificial intelligence (AI) is the goal of designing AI systems that have strong, ideally provable, assurances of correctness with respect to formally-specified requirements. This talk will review the main challenges to achieving Verified AI, and the progress the research community has made towards this goal. A particular focus will be on AI-based autonomous and semi-autonomous cyber-physical systems (CPS), and on the role of environment/world modeling throughout the design cycle. We argue for developing a new generation of design automation techniques, rooted in formal methods, to enable and support the routine development of high assurance AI-based autonomy. I will describe our work on formal methods for Verified AI-based autonomy, implemented in the open-source Scenic and VerifAI toolkits. The use of these tools will be demonstrated in industrial case studies involving deep learning-based autonomy in ground and air vehicles. We conclude with an outlook to the future of the Verified AI agenda.

Bio: Sanjit A. Seshia is the Cadence Founders Chair Professor in the Department of Electrical Engineering and Computer Sciences (EECS) at the University of California, Berkeley. His research interests are in formal methods for dependable and secure computing, spanning the areas of cyber-physical systems (CPS), computer security, distributed systems, artificial intelligence (AI), machine learning, and robotics. He is co-author of a widely-used textbook on embedded, cyber-physical systems and has led the development of technologies for cyber-physical systems education based on formal methods. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, the Frederick Emmons Terman Award for contributions to EECS education, the IEEE TCCPS Mid-Career Award, a Distinguished Alumnus Award from IIT Bombay, and the Computer-Aided Verification (CAV) Award for contributions to the foundations of SMT solving. He is a Fellow of the ACM and the IEEE.