Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision

• URL: http://arxiv.org/abs/2507.22760v1
• Date: Wed, 30 Jul 2025 15:21:22 GMT
• Title: Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision
• Authors: Samuel Teuber, Debasmita Lohar, Bernhard Beckert,
• Abstract summary: This paper bridges the gap between theoretical guarantees and real-world implementations by incorporating robustness under finite-precision perturbations.<n>We employ state-of-the-art mixed-precision fixed-point tuners to synthesize sound and efficient implementations, thus providing a complete end-to-end solution.<n>We evaluate our approach on case studies from the automotive and aeronautics domains, producing efficient NN implementations with rigorous infinite-time horizon safety guarantees.
• Score: 0.716879432974126
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: As neural networks (NNs) become increasingly prevalent in safety-critical neural network-controlled cyber-physical systems (NNCSs), formally guaranteeing their safety becomes crucial. For these systems, safety must be ensured throughout their entire operation, necessitating infinite-time horizon verification. To verify the infinite-time horizon safety of NNCSs, recent approaches leverage Differential Dynamic Logic (dL). However, these dL-based guarantees rely on idealized, real-valued NN semantics and fail to account for roundoff errors introduced by finite-precision implementations. This paper bridges the gap between theoretical guarantees and real-world implementations by incorporating robustness under finite-precision perturbations -- in sensing, actuation, and computation -- into the safety verification. We model the problem as a hybrid game between a good Demon, responsible for control actions, and a bad Angel, introducing perturbations. This formulation enables formal proofs of robustness w.r.t. a given (bounded) perturbation. Leveraging this bound, we employ state-of-the-art mixed-precision fixed-point tuners to synthesize sound and efficient implementations, thus providing a complete end-to-end solution. We evaluate our approach on case studies from the automotive and aeronautics domains, producing efficient NN implementations with rigorous infinite-time horizon safety guarantees.

Related papers

• Reachability Barrier Networks: Learning Hamilton-Jacobi Solutions for Smooth and Flexible Control Barrier Functions [5.846607930201535]
  Control barrier functions (CBFs) are a popular method for appending safety guarantees to a general control framework.<n>We use physics-informed neural networks (PINNs) to generate smooth approximations of CBFs by computing Hamilton-Jacobi optimal control solutions.<n>We demonstrate that RBNs are highly accurate in low dimensions, and safer than the standard neural CBF approach in high dimensions.
  arXiv  Detail & Related papers  (2025-05-16T23:30:13Z)
• Provably Safe Neural Network Controllers via Differential Dynamic Logic [2.416907802598482]
  We present the first general approach that allows reusing control theory results for NNCS verification. Based on provably safe control envelopes in dL, we derive specifications for the NN which is proven via NN verification. We show that a proof of the NN adhering to the specification is mirrored by a dL proof on the infinite-time safety of the NNCS.
  arXiv  Detail & Related papers  (2024-02-16T16:15:25Z)
• Scaling #DNN-Verification Tools with Efficient Bound Propagation and Parallel Computing [57.49021927832259]
  Deep Neural Networks (DNNs) are powerful tools that have shown extraordinary results in many scenarios. However, their intricate designs and lack of transparency raise safety concerns when applied in real-world applications. Formal Verification (FV) of DNNs has emerged as a valuable solution to provide provable guarantees on the safety aspect.
  arXiv  Detail & Related papers  (2023-12-10T13:51:25Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification problem involves counting the number of input configurations of a DNN that result in a violation of a safety property. We propose a novel approach that returns the exact count of violations. We present experimental results on a set of safety-critical benchmarks.
  arXiv  Detail & Related papers  (2023-01-17T18:32:01Z)
• 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)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• Log Barriers for Safe Black-box Optimization with Application to Safe Reinforcement Learning [72.97229770329214]
  We introduce a general approach for seeking high dimensional non-linear optimization problems in which maintaining safety during learning is crucial. Our approach called LBSGD is based on applying a logarithmic barrier approximation with a carefully chosen step size. We demonstrate the effectiveness of our approach on minimizing violation in policy tasks in safe reinforcement learning.
  arXiv  Detail & Related papers  (2022-07-21T11:14:47Z)
• Automated Repair of Neural Networks [0.26651200086513094]
  We introduce a framework for repairing unsafe NNs w.r.t. safety specification. Our method is able to search for a new, safe NN representation, by modifying only a few of its weight values. We perform extensive experiments which demonstrate the capability of our proposed framework to yield safe NNs w.r.t.
  arXiv  Detail & Related papers  (2022-07-17T12:42:24Z)
• Pointwise Feasibility of Gaussian Process-based Safety-Critical Control under Model Uncertainty [77.18483084440182]
  Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs) are popular tools for enforcing safety and stability of a controlled system, respectively. We present a Gaussian Process (GP)-based approach to tackle the problem of model uncertainty in safety-critical controllers that use CBFs and CLFs.
  arXiv  Detail & Related papers  (2021-06-13T23:08:49Z)
• Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning [0.0]
  We propose an automated verification pipeline capable of synthesizing high-quality safety shields. Our key insight involves separating safety verification from neural controller, using pre-computed verified safety shields to constrain neural controller training. Experimental results over a range of realistic high-dimensional deep RL benchmarks demonstrate the effectiveness of our approach.
  arXiv  Detail & Related papers  (2021-04-20T19:30:29Z)

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.