Verification of Visual Controllers via Compositional Geometric Transformations

• URL: http://arxiv.org/abs/2507.04523v1
• Date: Sun, 06 Jul 2025 20:22:58 GMT
• Title: Verification of Visual Controllers via Compositional Geometric Transformations
• Authors: Alexander Estornell, Leonard Jung, Michael Everett,
• Abstract summary: We introduce a novel verification framework for perception-based controllers that can generate outer-approximations of reachable sets.<n>We provide theoretical guarantees on the soundness of our method and demonstrate its effectiveness across benchmark control environments.
• Score: 49.81690518952909
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Designing Robust Software Sensors for Nonlinear Systems via Neural Networks and Adaptive Sliding Mode Control [2.884893167166808]
  This paper presents a novel approach to designing software sensors for nonlinear dynamical systems.<n>Unlike traditional model-based observers that rely on explicit transformations or linearization, the proposed framework integrates neural networks with adaptive Sliding Mode Control (SMC)<n>The training methodology leverages the system's governing equations as a physics-based constraint, enabling observer synthesis without access to ground-truth state trajectories.
  arXiv  Detail & Related papers  (2025-07-09T13:06:58Z)
• Designing Control Barrier Function via Probabilistic Enumeration for Safe Reinforcement Learning Navigation [55.02966123945644]
  We propose a hierarchical control framework leveraging neural network verification techniques to design control barrier functions (CBFs) and policy correction mechanisms.<n>Our approach relies on probabilistic enumeration to identify unsafe regions of operation, which are then used to construct a safe CBF-based control layer.<n>These experiments demonstrate the ability of the proposed solution to correct unsafe actions while preserving efficient navigation behavior.
  arXiv  Detail & Related papers  (2025-04-30T13:47:25Z)
• Learning Vision-Based Neural Network Controllers with Semi-Probabilistic Safety Guarantees [24.650302053973142]
  We introduce a novel semi-probabilistic verification framework that integrates reachability analysis with conditional generative adversarial networks.<n>Next, we develop a gradient-based training approach that employs a novel safety loss function, safety-aware data-sampling strategy, and curriculum learning.<n> Empirical evaluations in X-Plane 11 airplane landing simulation, CARLA-simulated autonomous lane following, and F1Tenth lane following in a visually-rich miniature environment demonstrate the effectiveness of our method in achieving formal safety guarantees.
  arXiv  Detail & Related papers  (2025-02-28T21:16:42Z)
• Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles [3.2540854278211864]
  Image-based neural network controllers in autonomous vehicles often struggle with high-dimensional inputs, computational inefficiency, and a lack of explainability.<n>We propose SEVIN, a framework that leverages a Variational Autoencoders (VAE) to encode high-dimensional images into a lower-dimensional, explainable latent space.<n>We show that SEVIN achieves efficient and scalable verification while providing explainable insights into controller behavior.
  arXiv  Detail & Related papers  (2025-01-23T16:46:45Z)
• Code-as-Monitor: Constraint-aware Visual Programming for Reactive and Proactive Robotic Failure Detection [56.66677293607114]
  We propose Code-as-Monitor (CaM) for both open-set reactive and proactive failure detection.<n>To enhance the accuracy and efficiency of monitoring, we introduce constraint elements that abstract constraint-related entities.<n>Experiments show that CaM achieves a 28.7% higher success rate and reduces execution time by 31.8% under severe disturbances.
  arXiv  Detail & Related papers  (2024-12-05T18:58:27Z)
• OOSTraj: Out-of-Sight Trajectory Prediction With Vision-Positioning Denoising [49.86409475232849]
  Trajectory prediction is fundamental in computer vision and autonomous driving. Existing approaches in this field often assume precise and complete observational data. We present a novel method for out-of-sight trajectory prediction that leverages a vision-positioning technique.
  arXiv  Detail & Related papers  (2024-04-02T18:30:29Z)
• In-Distribution Barrier Functions: Self-Supervised Policy Filters that Avoid Out-of-Distribution States [84.24300005271185]
  We propose a control filter that wraps any reference policy and effectively encourages the system to stay in-distribution with respect to offline-collected safe demonstrations. Our method is effective for two different visuomotor control tasks in simulation environments, including both top-down and egocentric view settings.
  arXiv  Detail & Related papers  (2023-01-27T22:28:19Z)
• Assuring Safety of Vision-Based Swarm Formation Control [0.0]
  We propose a technique for safety assurance of vision-based formation control. We show how the convergence analysis of a standard quantized consensus algorithm can be adapted for the constructed quantizers.
  arXiv  Detail & Related papers  (2022-10-03T14:47:32Z)
• Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
  This paper addresses learning safe output feedback control laws from partial observations of expert demonstrations. We first propose robust output control barrier functions (ROCBFs) as a means to guarantee safety. We then formulate an optimization problem to learn ROCBFs from expert demonstrations that exhibit safe system behavior.
  arXiv  Detail & Related papers  (2021-11-18T23:21:00Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.