Sample-Free Safety Assessment of Neural Network Controllers via Taylor Methods

TL;DR

The work presents a Taylor-polynomial based framework for safety verification of neural-network feedback controllers in spaceflight. By embedding a trained NN into the system dynamics, it constructs high-order Taylor expansions to obtain transfer maps and event maps, which are then bounded via interval arithmetic and adaptive domain splitting to produce exhaustive safety guarantees over large state spaces. The approach is demonstrated on two flight-critical scenarios—the Clohessy–Wiltshire planar rendezvous and an Earth–Mars transfer—showing substantial portions of the state space can be classified as safe with quantified bounds, while identifying unsafe regions that guide controller retraining. This methodology provides a formal, scalable tool for validating neural network controllers in safety-critical missions and supports informed decision-making in real-world operations.

Abstract

In recent years, artificial neural networks have been increasingly studied as feedback controllers for guidance problems. While effective in complex scenarios, they lack the verification guarantees found in classical guidance policies. Their black-box nature creates significant concerns regarding trustworthiness, limiting their adoption in safety-critical spaceflight applications. This work addresses this gap by developing a method to assess the safety of a trained neural network feedback controller via automatic domain splitting and polynomial bounding. The methodology involves embedding the trained neural network into the system's dynamical equations, rendering the closed-loop system autonomous. The system flow is then approximated by high-order Taylor polynomials, which are subsequently manipulated to construct polynomial maps that project state uncertainties onto an event manifold. Automatic domain splitting ensures the polynomials are accurate over their relevant subdomains, whilst also allowing an extensive state-space to be analysed efficiently. Utilising polynomial bounding techniques, the resulting event values may be rigorously constrained and analysed within individual subdomains, thereby establishing bounds on the range of possible closed-loop outcomes from using such neural network controllers and supporting safety assessment and informed operational decision-making in real-world missions.

Figures (6)

• Figure 1: Illustration of the distinction between the transfer map and the event map.
• Figure 2: Illustration of how remedies the wrapping effect for a scalar event map $x_{\textrm{e}}(x_0)$. Solid horizontal lines represent the interval bounds, for increasing number of subdomains from left to right. Red and green shading represents intervals that are deemed unsafe and safe, respectively.
• Figure 3: Neural network to replicate the optimal control direction for the Clohessy--Wiltshire scenario, (left) network architecture and (right) losses during training.
• Figure 4: Plot of the event map bounding for the Clohessy--Wiltshire scenario using the trained controller. A colour bar is applied to indicate safe and unsafe subdomains, based on the bounds of the squared length.
• Figure 5: Neural network to replicate the optimal control direction for the Earth--Mars transfer, (left) network architecture and (right) losses during training.