A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems

• URL: http://arxiv.org/abs/2601.08065v1
• Date: Mon, 12 Jan 2026 23:20:58 GMT
• Title: A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems
• Abstract summary: We introduce new algorithms that compute both over- and under-approximations of backward reachable sets for such systems.<n>We further integrate these backward algorithms with established forward analysis techniques to yield a unified verification framework for neural feedback systems.
• Score: 21.549912728385518
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Forward reachability analysis is the predominant approach for verifying reach-avoid properties in neural feedback systems (dynamical systems controlled by neural networks). This dominance stems from the limited scalability of existing backward reachability methods. In this work, we introduce new algorithms that compute both over- and under-approximations of backward reachable sets for such systems. We further integrate these backward algorithms with established forward analysis techniques to yield a unified verification framework for neural feedback systems.

Related papers

• The FABRIC Strategy for Verifying Neural Feedback Systems [21.549912728385518]
  We introduce new algorithms for computing both over- and underapproximations of backward reachable sets for nonlinear neural feedback systems.<n>We call the resulting algorithm Forward and Backward Reachability Integration for Certification (FaBRIC)
  arXiv  Detail & Related papers  (2026-03-09T21:54:07Z)
• Certified Neural Approximations of Nonlinear Dynamics [51.01318247729693]
  In safety-critical contexts, the use of neural approximations requires formal bounds on their closeness to the underlying system.<n>We propose a novel, adaptive, and parallelizable verification method based on certified first-order models.
  arXiv  Detail & Related papers  (2025-05-21T13:22:20Z)
• Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems [59.57462129637796]
  This paper presents a backward reachability approach for safety verification of closed-loop systems with neural networks (NNs) The presence of NNs in the feedback loop presents a unique set of problems due to the nonlinearities in their activation functions and because NN models are generally not invertible. We present frameworks for calculating BP over-approximations for both linear and nonlinear systems with control policies represented by feedforward NNs.
  arXiv  Detail & Related papers  (2022-09-28T13:17:28Z)
• Large-Scale Sequential Learning for Recommender and Engineering Systems [91.3755431537592]
  In this thesis, we focus on the design of an automatic algorithms that provide personalized ranking by adapting to the current conditions. For the former, we propose novel algorithm called SAROS that take into account both kinds of feedback for learning over the sequence of interactions. The proposed idea of taking into account the neighbour lines shows statistically significant results in comparison with the initial approach for faults detection in power grid.
  arXiv  Detail & Related papers  (2022-05-13T21:09:41Z)
• Backward Reachability Analysis for Neural Feedback Loops [40.989393438716476]
  This paper presents a backward reachability approach for safety verification of closed-loop systems with neural networks (NNs) The presence of NNs in the feedback loop presents a unique set of problems due to the nonlinearities in their activation functions and because NN models are generally not invertible. We present an algorithm to iteratively find BP set estimates over a given time horizon and demonstrate the ability to reduce conservativeness by up to 88% with low additional computational cost.
  arXiv  Detail & Related papers  (2022-04-14T01:13:14Z)
• Imbedding Deep Neural Networks [0.0]
  Continuous depth neural networks, such as Neural ODEs, have refashioned the understanding of residual neural networks in terms of non-linear vector-valued optimal control problems. We propose a new approach which explicates the network's depth' as a fundamental variable, thus reducing the problem to a system of forward-facing initial value problems.
  arXiv  Detail & Related papers  (2022-01-31T22:00:41Z)
• Neural Network Verification in Control [3.3123634393237706]
  This tutorial first introduces and unifies recent techniques for verifying robustness properties of NNs. The techniques are then extended to provide formal guarantees of neural feedback loops. The provided tools are shown to enable closed-loop reachability analysis and robust deep reinforcement learning.
  arXiv  Detail & Related papers  (2021-09-30T22:28:44Z)
• Supervised DKRC with Images for Offline System Identification [77.34726150561087]
  Modern dynamical systems are becoming increasingly non-linear and complex. There is a need for a framework to model these systems in a compact and comprehensive representation for prediction and control. Our approach learns these basis functions using a supervised learning approach.
  arXiv  Detail & Related papers  (2021-09-06T04:39:06Z)
• Reinforcement Learning as Iterative and Amortised Inference [62.997667081978825]
  We use the control as inference framework to outline a novel classification scheme based on amortised and iterative inference. We show that taking this perspective allows us to identify parts of the algorithmic design space which have been relatively unexplored.
  arXiv  Detail & Related papers  (2020-06-13T16:10:03Z)
• Parallelization Techniques for Verifying Neural Networks [52.917845265248744]
  We introduce an algorithm based on the verification problem in an iterative manner and explore two partitioning strategies. We also introduce a highly parallelizable pre-processing algorithm that uses the neuron activation phases to simplify the neural network verification problems.
  arXiv  Detail & Related papers  (2020-04-17T20:21:47Z)
• Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming [19.51345816555571]
  We propose a novel forward reachability analysis method for the safety verification of linear time-varying systems with neural networks in feedback. We show that we can compute these approximate reachable sets using semidefinite programming. We illustrate our method in a quadrotor example, in which we first approximate a nonlinear model predictive controller via a deep neural network and then apply our analysis tool to certify finite-time reachability and constraint satisfaction of the closed-loop system.
  arXiv  Detail & Related papers  (2020-04-16T18:48:25Z)

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.