PaperlayerView exact revision on arXiv

Source-linked AI summary

Formal Verification of Neural Network Controlled Autonomous Systems

Xiaowu Sun, Haitham Khedr, Yasser Shoukry

arXiv:1810.13072v1cs.AIcs.ROeess.SY

TL;DR

The paper seeks formal guarantees that a LiDAR-equipped, neural-network-controlled robot avoids polytopic obstacles from specified initial states. It constructs imaging-adapted workspace partitions and an SMC-based finite-state abstraction, then applies reachability analysis; the framework is correct, and preprocessing reduces execution time by 2-3 orders of magnitude.

  • Problem

    Formal verification must establish system-level safety for autonomous robots whose neural-network controllers process LiDAR images, beyond simpler neural-network input-output properties.

  • Method

    The framework partitions the workspace into imaging-adapted sets with affine LiDAR maps, constructs a finite-state abstraction using SMC-based ReLU analysis, and applies reachability analysis.

  • Results

    2-3 orders of magnitude execution time reduction was achieved by preprocessing that generates counterexamples for SMC analysis.

  • Takeaways & Limitations

    The computed safe initial set is guaranteed to contain only states whose trajectories are safe, providing an under-approximation of the safe robot states.

  • Takeaways & Limitations

    Neural-network analysis is NP-hard, the verification algorithm may require exponentially many analyses in the number of partition regions, and the computed safe set is not guaranteed maximal.

Abstract

from arXiv · show

In this paper, we consider the problem of formally verifying the safety of an autonomous robot equipped with a Neural Network (NN) controller that processes LiDAR images to produce control actions. Given a workspace that is characterized by a set of polytopic obstacles, our objective is to compute the set of safe initial conditions such that a robot trajectory starting from these initial conditions is guaranteed to avoid the obstacles. Our approach is to construct a finite state abstraction of the system and use standard reachability analysis over the finite state abstraction to compute the set of the safe initial states. The first technical problem in computing the finite state abstraction is to mathematically model the imaging function that maps the robot position to the LiDAR image. To that end, we introduce the notion of imaging-adapted sets as partitions of the workspace in which the imaging function is guaranteed to be affine. We develop a polynomial-time algorithm to partition the workspace into imaging-adapted sets along with computing the corresponding affine imaging functions. Given this workspace partitioning, a discrete-time linear dynamics of the robot, and a pre-trained NN controller with Rectified Linear Unit (ReLU) nonlinearity, the second technical challenge is to analyze the behavior of the neural network. To that end, we utilize a Satisfiability Modulo Convex (SMC) encoding to enumerate all the possible segments of different ReLUs. SMC solvers then use a Boolean satisfiability solver and a convex programming solver and decompose the problem into smaller subproblems. To accelerate this process, we develop a pre-processing algorithm that could rapidly prune the space feasible ReLU segments. Finally, we demonstrate the efficiency of the proposed algorithms using numerical simulations with increasing complexity of the neural network controller.

1 INTRODUCTION

The paper addresses the lack of system-level safety guarantees for neural-network-controlled cyber-physical systems. It develops a formal verification framework for LiDAR-based autonomous robots using workspace partitioning, finite-state abstraction, and reachability analysis.

  • AI-enabled cyber-physical systems increasingly control physical systems, but their safety and reliability remain understudied despite safety-critical failures.
  • Existing robustness methods focus on neural-network behavior under data outliers rather than guarantees for system-level safety and reliability.
  • Testing and falsification can find defects or specification violations but do not provide formal guarantees for the complete neural-network-controlled system.
  • The paper formulates formal verification for robots that process LiDAR images with neural-network controllers to produce control inputs.
  • Imaging-adapted sets partition the workspace so the robot-pose-to-LiDAR map is affine, with a polynomial-time algorithm computing the partitions and maps.
  • The framework combines finite-state abstraction, SMC-based ReLU analysis, preprocessing to reduce feasible assignments, and reachability analysis to compute safe initial states.

2 PROBLEM FORMULATION

The problem formulation models a robot with discrete-time dynamics moving through a polytopic workspace while sensing obstacles with LiDAR and acting through a ReLU neural-network controller. Safety means avoiding obstacles over the entire trajectory, and the verification goal is to compute all initial conditions whose trajectories are safe.

  • 2.1 Notation: The notation defines natural, real, positive-real, and Boolean number sets, vector concatenation and indexing, elementwise maxima, set interiors and boundaries, and set-valued maps.
  • 2.1 Notation: Figure 1 presents the problem setup and introduces atan2 for a vector z = (x,y) as atan2(y,x).
  • 2.2 Dynamics and Workspace: The robot moves in a compact, convex, two-dimensional polytopic workspace and must avoid both workspace boundaries and polytopic obstacles.
  • 2.2 Dynamics and Workspace: The robot state evolves under a discrete-time linear system, with A and B representing the dynamics and ζ projecting the state to the robot's workspace position.
  • 2.3 LiDAR Imaging: A LiDAR scanner emits N evenly distributed laser beams; each observation is the distance to the nearest obstacle in the corresponding beam direction, and these observations form the processed LiDAR image.
  • 2.3 LiDAR Imaging: The formulation assumes a fixed LiDAR heading, a condition applicable when the robot maintains a fixed pose such as constant yaw.
  • 2.4 Neural Network Controller: A pre-trained fully connected neural-network controller maps the 2N-dimensional LiDAR image to control actions using ReLU hidden layers and learned weights and biases.
  • 2.5 Robot Trajectories and Safety Specifications: A trajectory is safe when the robot avoids every obstacle at all times, and the verification problem is to compute initial conditions whose trajectories satisfy that property.

3 FRAMEWORK

The framework builds a finite-state abstraction of the neural-network-controlled robot, establishes a simulation relation, and applies reachability analysis to conservatively compute safe initial states.

  • Finite-state abstraction: The abstraction SF represents the robot system SNN and is connected to it by a simulation relation Q for safety verification.The finite abstraction may be nondeterministic and is defined over abstract states and transitions.
  • Finite-state abstraction: Workspace and state-space partitioning produces finite abstract states and relates concrete robot states to corresponding abstract states.Aggregate partitions can group multiple fine partitions to reduce computational effort.
  • Transition computation: A preprocessing step prunes feasible ReLU indicator assignments before transition analysis, reducing the execution time by an order of magnitude.The preprocessing is applied to the original SMC encoding.
  • Safety computation: Fixed-point reachability marks obstacle- and boundary-related abstract states as unsafe, then classifies remaining states as safe and maps them back to concrete safe states.The resulting safe set is computed as the complement of the fixed-point unsafe set.
  • Transition computation: Transition feasibility combines linear robot dynamics, affine LiDAR imaging, and ReLU-network reasoning encoded as a satisfiability problem.The neural network is the main technical difficulty in checking transitions.

4 IMAGING-ADAPTED WORKSPACE PARTITIONING

The paper partitions a polytopic workspace into imaging-adapted regions so each LiDAR ray has consistent obstacle-edge intersections and the imaging function is affine within every region.

  • Imaging-adapted partitions: An imaging-adapted partition ensures that each LiDAR ray intersects the same obstacle edge for every robot position in a region.This property is expressed by requiring each possible intersection set L_k(R) to be a line segment.
  • Imaging-adapted partitions: Within an imaging-adapted region, the LiDAR imaging function is affine in the robot state.The affine representation uses region- and laser-angle-dependent matrices and vectors.
  • Workspace partitioning: Figure 3 contrasts a non-adapted region, where a ray hits different obstacle edges, with adapted regions, where the intersected edge remains constant.The comparison illustrates why the partition must follow imaging geometry.
  • Workspace partitioning: The workspace-partitioning algorithm constructs line segments from obstacle and workspace vertices, computes their intersections with obstacle edges, and extracts planar regions.A plane-sweep procedure avoids testing all segment combinations directly.
  • Workspace partitioning: The algorithm computes imaging-adapted regions whose LiDAR maps are affine, with time complexity O(M log M+I log M).Here M is the cardinality of the constructed segment and edge set, while I counts their intersection points.

5 COMPUTING THE FINITE STATE ABSTRACTION

The paper constructs a finite-state abstraction by partitioning the workspace into regions with affine LiDAR imaging, discretizing the remaining state dimensions, and encoding transition feasibility with SMC constraints. Reachability over this abstraction yields a sound, though not necessarily maximal, safe-state set.

  • Finite-state abstraction: The finite state space indexes an imaging-adapted region and ε-sized hypercubes covering the remaining state dimensions.The relation Q associates concrete states with their corresponding abstract region and hypercube.
  • Imaging-adapted workspace partitioning: The workspace is partitioned into imaging-adapted regions where the LiDAR imaging map is affine.The construction uses obstacle and workspace geometry, ray-polygon intersections, plane-sweep intersection computation, and planar-graph cycles.
  • Transition feasibility: Transition feasibility searches for robot states and LiDAR images whose neural-network control input moves the robot between two abstract states while respecting its dynamics.The encoding includes state partitions, robot dynamics, affine imaging, and ReLU controller constraints.
  • SMC encoding: SMC combines Boolean assignments for ReLU phases with convex feasibility checks, using infeasibility explanations to prune subsequent assignments.This avoids MILP big-M encoding heuristics and iteratively narrows the ReLU search space.
  • SMC encoding: Pre-processing removes infeasible ReLU assignments before the original SMC encoding, producing an order of magnitude reduction in execution time.The reduction exploits constraints imposed by each workspace region and its LiDAR imaging function.
  • Correctness and scope: The abstraction simulates the neural-network-controlled system, and reachability computes an under-approximation of safe states whose initial trajectories are guaranteed safe.The framework is correct, but the computed safe set is not guaranteed to be maximal; analysis can be exponential in the number of partition regions.

6 RESULTS

Experiments evaluate workspace partitioning, ReLU pre-processing, and transition-feasibility checking as neural-network and workspace complexity increase. The results show substantial reductions in feasible ReLU assignments and transition-checking time when pre-processing counterexamples are used.

  • Workspace partitioning: Workspace partitioning remains below 1.5 minutes for a LiDAR scanner with 298 lasers.The number of regions and execution time increase with the number of LiDAR lasers and obstacle vertices.
  • ReLU pre-processing: For a 32-neuron network, only 11 ReLU assignments are feasible among 4.3E9 possible assignments in the tested region.The IIS counterexample strategy enumerates feasible assignments during pre-processing.
  • ReLU pre-processing: The counterexample strategy finds feasible ReLU assignments for networks with a couple of hundred neurons in less than 4 minutes for one-hidden-layer networks.The experiment varies the neural-network architecture while fixing one workspace region.
  • Workspace-region dependence: The number of feasible ReLU assignments increases with workspace-region size for a two-hidden-layer network with 40 neurons per layer.Execution time, counterexamples, and feasible assignments are compared across regions.
  • Transition feasibility: Pre-processing counterexamples reduce transition-feasibility execution time by 2-3 orders of magnitude compared with SMC without pre-processing.The counterexample-enhanced encoding is also less sensitive to neural-network architecture changes.

7 CONCLUSIONS

The framework verifies safety for LiDAR-equipped autonomous robots controlled by neural networks by combining imaging-adapted workspace partitioning with SMC-based finite-state abstraction. Pre-processing counterexamples reduce execution time by 2–3 orders of magnitude.

  • The framework verifies the safety of autonomous robots equipped with LiDAR scanners and neural network controllers.
  • Imaging-adapted sets partition the workspace, while SMC encodings compute a finite-state abstraction for under-approximating safe robot states.
  • 2–3 orders of magnitude execution time reduction resulted from pre-processing counterexamples.

A PROOF OF LEMMA 4.2

The proof shows that each LiDAR component is affine over an imaging-adapted region. It derives this by representing the ray–segment intersection through an interpolation parameter and substituting the resulting expression into the distance formula.

  • For an arbitrary laser angle and robot position in a region, the LiDAR intersection point lies on the region’s corresponding line segment.
  • The intersection point is also constrained to the laser ray, yielding an equation involving the interpolation parameter ν_k.
  • Solving for ν_k produces a piecewise expression determined by the laser angle and segment geometry.
  • Because the resulting coefficients are constant within the region, each LiDAR component d_k(ζ(x)) is affine, and therefore the full LiDAR image is affine.

B PROOF OF PROPOSITION 4.3

The proof establishes the geometric property needed for the workspace partition by showing that distinct obstacle edges cannot generate four distinct parallel boundary segments within one region. This contradiction implies the required partition structure.

  • Assuming two distinct obstacle edges generate four ray-derived segments inside the region leads to a contradiction.
  • The constructed segments belong to the region boundary because segments in G do not intersect the region interior.
  • All four segments are parallel because they lie on rays sharing the same angle.
  • A polygon can have at most two parallel edges, so the four segments force corresponding segments, and hence the original obstacle edges, to coincide.

C PROOF OF THEOREM 4.4

The theorem’s complexity claim follows directly from the plane-sweep algorithm used for the workspace partitioning, whose complexity is established by the cited computational-geometry theorem.

  • The partitioning complexity follows from the plane-sweep algorithm and its established computational-geometry complexity bound.

D PROOF OF PROPOSITION 5.1

The proof establishes correctness by combining affine LiDAR imaging, convex workspace partitions, and the correctness of the monotone SMC decision procedure used to compute δF.

  • Theorem 4.4 establishes that the LiDAR imaging is affine.
  • The partitions R are convex, making the encoding in (15)-(23) monotone SMC.
  • Correctness of the SMC decision procedure entails correct computation of δF.
Loading 1810.13072v1…