Stochastic world models improve verifying vision-based neural systems
Stochastic World Models for Verifying Vision-Based Neural Feedback Systems
Artificial Intelligence
Summary
Verifying systems that use camera images with neural networks is hard because the models of what the cameras see are often too big or inaccurate. This paper shows a new way to model the camera observations using stochastic world models that simulate sensor variations more realistically but remain easier to analyze. The authors also introduce a method combining different verification strategies that can check much more of the system’s possible states than before. Their method works better than previous approaches on a safety test involving emergency braking in driving scenarios.
What this means in practice
- •For autonomous vehicle developers: Verify vision-based braking controllers more comprehensively to improve safety validation before deployment.
- •For robotics software engineers: Use stochastic world models as perceptual surrogates to test neural feedback loops under varied sensor conditions.
Authors
I. Samuel Akinwande, Mykel J. Kochenderfer, Clark Barrett
Abstract
Verifying a vision-based neural feedback system requires a model of the observations its controller acts upon. Such a model must capture the variation the sensor produces, while remaining tractable for closed-loop analysis. Generative adversarial networks (GANs) have served as perception surrogates, but they are large, reproduce complex scenes poorly, and are hard to verify. We explore stochastic world models as a richer class of perception surrogates. We train a world model with physically grounded latents, built from operations that standard verifiers bound. It reproduces held-out frames more faithfully than GAN surrogates with up to 130 times as many parameters. To verify these surrogates, we develop a procedure that combines falsification, adaptive refinement, symbolic, and backward analyses. On an emergency braking benchmark with a GAN surrogate, our procedure resolves the entire state space, 38% of which the state-of-the-art verifier left unresolved. On the RGB version of the benchmark, where no verification results have previously been reported, our procedure resolves over 80% of the state space with a world model surrogate.