Events Calendar

Speaker: Kevin Leahy

Title: Composition and Decomposition for Verified Autonomy

Abstract: Machine learning failures increasingly compromise autonomous systems, yet the black-box nature of learned components makes traditional verification approaches inadequate. This challenge is particularly acute in safety-critical applications like autonomous vehicles and robotic systems, where unverified ML components can lead to catastrophic failures despite high average-case performance. We address this verification gap through compositional system design, treating learned components as modules within larger, formally analyzable architectures. Unlike end-to-end learning approaches that are opaque and difficult to verify, compositional design enables modular reasoning: each component can be verified independently with guaranteed properties that compose into system-level safety assurances. This modularity makes verification tractable while preserving the flexibility of machine learning. This talk presents two complementary approaches for verifiable autonomous systems. First, I demonstrate bottom-up composition in reinforcement learning, where we synthesize complex behaviors by formally composing verified sub-policies with provable guarantees on the resulting system behavior. Second, I present top-down decomposition for perception-based control, separating vision systems from control modules to enable independent verification of each component while maintaining end-to-end performance guarantees.

About the Speaker: Kevin Leahy is an Assistant Professor in Robotics Engineering at Worcester Polytechnic Institute, focusing involves AI for autonomous systems, with an emphasis on formal methods and multi-agent systems. He received his Ph.D. degree in Mechanical Engineering in 2017 from Boston University. From 2017 to 2023, he was a member of the Technical Staff at MIT Lincoln Laboratory, working on learning decentralized control strategies for multi-agent systems, researching collision avoidance in aviation, and planning for heterogeneous teams from high-level specifications. He currently serves as Associate Co-chair on the IEEE RAS Technical Committee for Verification of Autonomous Systems. He is a recipient of the 2025 ONR YIP award.