PaperlayerView exact revision on arXiv

Source-linked AI summary

Verisig: verifying safety properties of hybrid systems with neural network controllers

Radoslav Ivanov, James Weimer, Rajeev Alur, George J. Pappas, Insup Lee

arXiv:1811.01828v1eess.SY

TL;DR

Existing neural-network verification methods do not capture nonlinear plant dynamics in closed-loop systems, motivating Verisig. Verisig transforms sigmoid-based controllers into hybrid systems, enabling reachability verification with decidability results for restricted or conjecturally general networks.

  • Problem

    Existing DNN verification methods check network input/output properties but do not verify closed-loop safety properties involving nonlinear plant dynamics.

  • Method

    Verisig uses the sigmoid’s quadratic differential equation to transform a DNN into an equivalent hybrid system and verifies the composed controller-plant system using reachability tools.

  • Results

    Reachability is decidable for one-hidden-layer DNNs, decidable for general DNNs if Schanuel’s conjecture holds, and Verisig is evaluated in two case studies.

  • Takeaways & Limitations

    Verisig provides a hybrid-system route to safety verification for closed-loop systems with sigmoid-based neural-network controllers.

  • Takeaways & Limitations

    The approach is a proof of concept because existing reachability tools do not exploit sigmoid dynamics, limiting scalability and precision until specialized tools are developed.

Abstract

from arXiv · show

This paper presents Verisig, a hybrid system approach to verifying safety properties of closed-loop systems using neural networks as controllers. Although techniques exist for verifying input/output properties of the neural network itself, these methods cannot be used to verify properties of the closed-loop system (since they work with piecewise-linear constraints that do not capture non-linear plant dynamics). To overcome this challenge, we focus on sigmoid-based networks and exploit the fact that the sigmoid is the solution to a quadratic differential equation, which allows us to transform the neural network into an equivalent hybrid system. By composing the network's hybrid system with the plant's, we transform the problem into a hybrid system verification problem which can be solved using state-of-the-art reachability tools. We show that reachability is decidable for networks with one hidden layer and decidable for general networks if Schanuel's conjecture is true. We evaluate the applicability and scalability of Verisig in two case studies, one from reinforcement learning and one in which the neural network is used to approximate a model predictive controller.

1 INTRODUCTION

Verisig addresses the challenge of verifying safety properties for closed-loop systems that combine hybrid plants with neural-network controllers. It transforms sigmoid-based DNNs into equivalent hybrid systems, enabling reachability-based verification and yielding decidability results plus case-study evaluations.

  • DNNs are increasingly used in safety-critical CPS, while autonomous-driving incidents underscore the need to verify safety properties involving such networks.
  • Existing SMT- and MILP-based methods can verify properties of DNNs themselves but do not straightforwardly capture nonlinear dynamics of typical CPS plants.
  • Verisig exploits sigmoid dynamics to transform a DNN into an equivalent hybrid system and composes it with the plant for closed-loop reachability verification.
  • DNN reachability is decidable for one-hidden-layer networks and for general networks if Schanuel’s conjecture holds; general-network reachability is also δ-decidable through dReach.
  • Verisig is evaluated on Mountain Car reinforcement learning and DNN approximation of an MPC with safety guarantees.
  • The MILP approach is faster for small or shallow networks, but its runtimes grow exponentially with depth while Verisig+Flow* scales linearly with the number of layers.

2 PROBLEM FORMULATION

The paper models a closed-loop system as a hybrid plant controlled by a trained DNN and formulates both DNN-output and closed-loop reachable-state verification problems. Its approach transforms the DNN into an equivalent hybrid system that can be composed with the plant.

  • 2.1 Plant Model: The plant is modeled as a hybrid system with discrete modes, continuous variables, differential dynamics, invariants, guarded transitions, resets, and an observation model.
  • 2.1 Plant Model: A hybrid system is represented as H = (X,X0,F,E,I,G,R,д), including state space, initial states, vector fields, transitions, invariants, guards, resets, and observations.
  • 2.2 DNN Controller Model: The controller is a feedforward DNN mapping measurements y to control inputs u, with layered affine transformations and element-wise nonlinear hidden-layer activations.
  • 2.2 DNN Controller Model: The paper considers sigmoid and tanh activations, while the final layer is conventionally linear and each layer is parameterized by weights and offsets.
  • 2.2 DNN Controller Model: The DNN parameters are learned during training and are assumed fixed once the trained controller is verified.
  • 2.3 Problem Statement: The DNN verification problem checks an output property ψdnn under input constraints ξdnn, while the closed-loop problem checks a property ψ over plant states reachable from initial states satisfying ξ.
  • 2.3 Problem Statement: The closed-loop system is the composition S = h || HP of the DNN controller and hybrid plant, and the final layer may also use a nonlinear activation in the Mountain Car case study.
  • 2.3 Problem Statement: Verisig addresses both problems by transforming h into an equivalent hybrid system Hh and verifying the composed system Hh || HP.

3 ON THE DECIDABILITY OF SIGMOID-BASED DNN REACHABILITY

The paper characterizes sigmoid-based DNN reachability using real-arithmetic formulas with exponentiation, establishing decidability under different architectural and input assumptions.

  • Multiple hidden layers: DNN reachability becomes an Rexp-formula when input and output properties are R-formulas.The sigmoid’s exponentiation introduces transcendental functions into the verification property.
  • Multiple hidden layers: If Schanuel’s conjecture holds, reachability for general sigmoid-based DNNs is decidable.This follows because Schanuel’s conjecture would imply decidability of the relevant Rexp-formulas.
  • Multiple hidden layers: Reachability is δ-decidable for general DNNs after transforming them into equivalent hybrid systems.The result uses dReach and the fact that sigmoid is Type 2 computable.
  • Single hidden layer: For one-hidden-layer DNNs with interval-bounded inputs, reachability is decidable without assuming Schanuel’s conjecture.The property can be transformed into an R-formula by exploiting interval bounds and sigmoid monotonicity.
  • Single hidden layer: The single-hidden-layer result assumes rational network parameters and additional rationality conditions on exponentials of biases and interval endpoints.These conditions are part of the theorem’s scope.

4 DNN REACHABILITY USING HYBRID SYSTEMS

Verisig transforms sigmoid-based DNNs into equivalent hybrid systems so existing reachability tools can analyze their reachable outputs and closed-loop compositions.

  • 4.1 Sigmoids as solutions to differential equations: The transformation exploits the sigmoid’s quadratic differential equation to represent each neural layer through continuous dynamics.Tracing the proxy dynamics to t = 1 recovers the exact sigmoid value.
  • 4.2 Deep Neural Networks as Hybrid Systems: Proposition 4.1 states that the DNN’s image of an input set equals the reachable output set in the final hybrid-system mode.The proof follows layer-by-layer composition and applies the final linear output map.
  • 4.2 Deep Neural Networks as Hybrid Systems: The hybrid system uses sequential modes, guards at t = 1, and resets that initialize the next layer from the preceding layer’s neuron values.A reset mode initializes proxy states at 0.5 before integrating each sigmoid layer.
  • 4.3 Illustrative example: In the illustrative two-layer example, the DNN is transformed into an equivalent three-mode hybrid system.Positive weights and monotone sigmoids allow output extrema to be obtained at corresponding input extrema.
  • 4.4 Hybrid System Verification Tools: Flow* is selected for scalability and handles systems with a few hundred states, while existing tools do not exploit sigmoid-specific monotonicity and polynomial structure.The paper identifies a specialized sigmoid reachability tool as future work because it could improve scalability and precision.

5 CASE STUDY APPLICATIONS

Verisig is evaluated on Mountain Car and quadrotor control tasks, verifying closed-loop liveness and safety properties for nonlinear hybrid plants. The case studies demonstrate applicability while exposing counterexamples and computational costs.

  • Case studies: Verisig evaluates closed-loop DNN controllers in Mountain Car reinforcement learning and quadrotor MPC-approximation case studies.The plants include discrete- and continuous-time nonlinear hybrid dynamics.
  • 5.1 Mountain Car: A Reinforcement Learning Case Study: Mountain Car verification confirms reward of at least 90 within at most 100 dynamics steps for most initial-condition subsets.Most properties require 10–15 minutes; endpoint subsets take longer because of hybrid-system branching.
  • 5.1 Mountain Car: A Reinforcement Learning Case Study: The subset [-0.6, -0.59] exposes a counterexample at p0 = −0.6, where the final reward is 88.Verisig therefore identifies initial regions where the desired property does not hold.
  • 5.2 Using DNNs to Approximate MPCs with Safety Guarantees: The quadrotor case study verifies that trajectories from the shown initial-condition set stay within 0.32m of the planner and avoid obstacles.The quadrotor follows a piecewise-linear plan toward the goal.
  • 5.1 Mountain Car: A Reinforcement Learning Case Study: Flow* approximation uncertainty grows during the car’s rapid downhill motion but remains within the tolerance needed to verify the desired Mountain Car property.The approximation sets are shown over time for p0 ∈ [−0.5, −0.48].
  • 5.2 Using DNNs to Approximate MPCs with Safety Guarantees: Most quadrotor verification cases take less than 30 minutes, while discrete DNN outputs require enumerating paths whose number can grow exponentially with scenario length.All properties in the quadrotor case study were verified.

6 COMPARISON WITH OTHER DNN VERIFICATION TECHNIQUES

The scalability study compares Verisig+Flow* with MILP-based sigmoid approximations on increasingly deep DNNs. MILP is faster for smaller or shallow networks, whereas Verisig+Flow* scales linearly and predictably with depth.

  • Experimental setup: Both methods use roughly 100 linear pieces to achieve similar sigmoid approximation error.The MILP baseline encodes piecewise-linear sigmoid bounds with binary variables.
  • Experimental setup: The study compares DNN reachability verification times while varying layers from two to ten and neurons per layer from 16 to 128.The comparison concerns DNN properties alone, not closed-loop properties.
  • Results: MILP-based verification is faster for small networks and large networks with few layers.This advantage changes as network depth increases.
  • Results: As layers increase, MILP runtimes grow exponentially with the number of binary variables, while Verisig+Flow* scales linearly because it repeats the same computation per layer.The comparison supports using Verisig+Flow* for fairly deep networks.
  • Results: A nine-layer MILP instance runs much faster than an eight-layer instance, likely because Gurobi exploits a corner case.The authors caution that such fast MILP runtimes may not represent worst-case behavior.

7 CONCLUSION AND FUTURE WORK

Verisig transforms sigmoid-based neural-network controllers into hybrid systems, enabling closed-loop safety verification with reachability tools. The paper establishes decidability results and evaluates applicability and scalability, while identifying broader activation-function support and specialized verification as future directions.

  • 7 CONCLUSION AND FUTURE WORK: Verisig transforms sigmoid-based DNN controllers into equivalent hybrid systems and verifies the composed closed-loop system with reachability tools such as Flow*.A network with L layers and N neurons per layer becomes a hybrid system with L + 1 modes and 2N states.
  • 7 CONCLUSION AND FUTURE WORK: Reachability is decidable for one-hidden-layer DNNs and for general DNNs if Schanuel’s conjecture is true.
  • 7 CONCLUSION AND FUTURE WORK: Two case studies evaluate Verisig+Flow*: reinforcement learning and neural-network approximation of an MPC with safety guarantees.
  • 7 CONCLUSION AND FUTURE WORK: Approximating DNNs with other activation functions using sigmoid-based networks could extend verification to arbitrary DNNs and broaden Verisig’s application domain.
  • 7 CONCLUSION AND FUTURE WORK: A specialized sigmoid verification tool could improve scalability and precision by exploiting monotone and quadratic sigmoid dynamics instead of relying on general-purpose Flow*.
  • 7 CONCLUSION AND FUTURE WORK: Flow*’s coarse approximation is a potential limitation, although experiments showed no large approximation errors; bounding this error remains future work.
Loading 1811.01828v1…