Talk Title: Formal Verification of Visual Autonomy: Perception Contracts and Abstract Rendering
Abstract: Generative AI and 3D vision are accelerating the development of autonomous systems that see, decide, and act in the physical world. Formal verification has built trust in circuits, programs, and control software by proving properties of their models. Can the same be done for autonomous systems whose decisions depend on learned vision? This talk describes our progress on that question along two lines. The first is perception contracts: bounds on the error of a vision pipeline over an operating design domain that are strong enough to prove closed-loop safety and can be established from data. Lyapunov perception contracts extend this idea to prove convergence under imperfect perception and make explicit the conditions on the environment under which the guarantee holds. The second is abstract rendering, which computes sound over-approximations of all the images a camera can produce as the scene and pose vary over a set. This lets us propagate uncertainty through the renderer and the neural network together and certify the downstream decision. I will discuss both with application in vision-based automated landing and formation flight, and close with what these results suggest about assurance for AI agents that act in the physical world.
Bio: Sayan Mitra is a Professor of Electrical and Computer Engineering and John Bardeen Faculty Scholar at the University of Illinois Urbana-Champaign, where he directs the Center for Autonomy. His research develops formal verification methods and tools for autonomous systems. He is the author of the textbook Verifying Cyber-Physical Systems (MIT Press, 2021) and co-founder of Rational CyPhy, a startup building certified autonomous platforms. He received his Ph.D. from MIT.
