Verification of Visual Controllers via Compositional Geometric Transformations

TL;DR

This paper introduces a new verification framework for perception-based neural network controllers that models visual uncertainties with geometric transformations, enabling safety guarantees under realistic visual perturbations.

Contribution

It presents a novel method that explicitly models geometric visual uncertainties for verification, bridging the gap between pixel perturbations and real-world effects.

Findings

Effective in benchmark control environments

Provides theoretical guarantees of soundness

Enables safety certification under visual uncertainties

Abstract

Perception-based neural network controllers are increasingly used in autonomous systems that rely on visual inputs to operate in the real world. Ensuring the safety of such systems under uncertainty is challenging. Existing verification techniques typically focus on Lp-bounded perturbations in the pixel space, which fails to capture the low-dimensional structure of many real-world effects. In this work, we introduce a novel verification framework for perception-based controllers that can generate outer-approximations of reachable sets through explicitly modeling uncertain observations with geometric perturbations. Our approach constructs a boundable mapping from states to images, enabling the use of state-based verification tools while accounting for uncertainty in perception. We provide theoretical guarantees on the soundness of our method and demonstrate its effectiveness across benchmark control environments. This work provides a principled framework for certifying the safety of perception-driven control systems under realistic visual perturbations.