Article Author
June 27, 2023
Link to Original Article
Designing Safe and Reliable Autonomous Systems
Our evolving vision of an autonomous future is informed by the tools we develop to enhance the safety of the systems that will replace man with machine. Chuchu Fan and the team of researchers she leads at her creatively acronymed Reliable Autonomous systems Lab at MIT (REALM) use rigorous mathematics to provide autonomous systems with proof of their safety, efficiency, and performance. Her research lies at the intersection of control theory, machine learning, and formal methods; it aims to provide verification for safety-and-mission critical systems, including drones, satellites, self-driving cars, and medical devices.
Before she arrived at the Institute, Fan earned a PhD in computer engineering from the University of Illinois at Urbana-Champagne and completed her postdoctoral research in computing and mathematical science at the California Institute of Technology. She is a recipient of the 2020 ACM Doctoral Dissertation Award, which is widely regarded as the most prestigious annual prize for dissertations in the field of computer science. The Association for Computing Machinery lauded her for, among other things, making foundational contributions to the verification of embedded and cyber-physical systems while demonstrating the applicability of her groundbreaking verification technologies to industrial-scale systems.
She titled her dissertation "Formal Methods for Safe Autonomy: Data-Driven Verification, Synthesis, and Applications." For the uninitiated, formal methods are specific, rigorous mathematical techniques that can be used to ensure computer systems behave as intended by proving correctness mathematically (as opposed to empirically, with field tests and simulations). “I was honored to receive the ACM award,” says Fan. “It served as recognition from the computer science domain that using formal methods to provide strong guarantees for systems, especially safety-critical systems, is essential.”
For context, in 1994, a mathematician discovered a flaw in Intel’s Pentium processor, sparking a public relations debacle for the company. What became known as the Pentium FDIV bug was no more and no less than an error in the precision of the division algorithm impacting Pentium's math coprocessor. The mistake cost Intel US$ 475 million in the form of a write-off related to chip recall and replacement. Moving forward, Intel invested heavily to incorporate formal methods into the testing phase of their chips.
Outside of the hardware domain, these techniques tend to be championed by designers of safety-critical systems for their ability to provide rigorous system analysis. You can find formal methods used in aircraft control systems, automotive subsystems, and spacecraft. As Fan explains it, with the prospect of safety-critical autonomous systems becoming commonplace in our everyday lives, formal methods have an important role to play.
Advances in machine learning have created extraordinary opportunities for achieving full autonomy by turning raw data into actionable information. However, learning-based methods for autonomous systems can and do fail, which Fan attributes to their limited ability to react to new data (generalization) and a lack of formal guarantees. Furthermore, once a model has been trained with learning-based methods, it’s difficult to explain its behavior (i.e., how it has arrived at the decision it has made). Without explainability there is no causality. How can we trust autonomous machines if we don’t understand the decisions they are making on our behalf?
Since coming to the Institute, Fan has been working to combine formal verification methods with machine learning to address these issues of safety, reliability, and trust. “At REALM, we give every machine learning algorithm a proof,” she explains. “We explore why and how a system makes its decisions, proving mathematically that a system driven by machine learning satisfies required safety specifications.” Think of it as prying open the machine learning black box.
In 2021 she partnered with Ford Motor Company to design a state-of-the-art method for predicting the probability of future collisions. She’s also collaborating with, among others, Boeing Research and Technology and General Electric Aviation on a NASA-sponsored research project to define a roadmap for the verification, validation, and assurance of autonomy through the year 2045. It will be broadly applicable to autonomy-related research investment decisions for stakeholders at the national level.
Her research with REALM demonstrates a commitment to solving the tough challenges associated with autonomous systems. In a paper accepted for the 5th Annual Conference on Robot Learning, she tackled what is commonly referred to as the spacecraft docking and rendezvous issue, effectively guaranteeing the reliability of autonomous satellite docking in space. She’s also designed a novel method for controlling aerial vehicles with verifiable collision-avoidance and goal-reaching behaviors.
More recently, Fan has developed a groundbreaking method to address the challenge of large-scale deployment of multi-agent autonomous systems in the real world. It provides control policies and safety guarantees for more than 1,000 aerial vehicles (think delivery drones). While traditional methods for multi-agent systems rely on route planning for each agent, Fan proposes a decentralized approach that she believes is the key to success. “Imagine a future with tens of thousands of drones, satellites, and driverless cars," she says. "Our decentralized approach allows for scalability and progress without sacrificing safety—it is unprecedented.”
Research & Markets predicts that 20.8 million autonomous vehicles will be operating on America’s roads by 2030. As for delivery drones, in 2019, McKinsey&Co published a debate about the likelihood of delivery UAVs scaling by 2030. Fan and her team of researchers are helping shape the conversation about autonomous systems through research that has real-world impact. “In the Reliable Autonomous systems Lab at MIT, we're not just sitting at our computers coming up with algorithms," Fan says. “Everything we do has real-world applications, and we’re designing tools that work for actual industry systems.”