Neural Network Verification for Gliding Drone Control: A Case Study

TL;DR

This work tackles verification of neural network controllers for Alsomitra-inspired gliding microdrones, addressing continuous-time dynamics and regression control. It proposes a two-pronged verification strategy using Vehicle for property-based checks and CORA for reachability, complemented by adversarial robustness training and Property-Driven Training (PDT). The study demonstrates that Lipschitz-based adversarial training can improve certain verification properties, while also highlighting substantial tool and modeling limitations that hinder full coverage of infinite-horizon and relational specifications. The results illuminate practical challenges in cross-tool integration, normalisation, and set-explosion issues, and argue for focused tool development to enable safe, robust, real-world deployment of energy-efficient wind-dispersed sensors. Overall, the work lays out a concrete path toward integrating verification into engineering workflows for bio-inspired autonomous microdrones, with broader implications for safe environmental sensing in complex dynamic environments.$

Abstract

As machine learning is increasingly deployed in autonomous systems, verification of neural network controllers is becoming an active research domain. Existing tools and annual verification competitions suggest that soon this technology will become effective for real-world applications. Our application comes from the emerging field of microflyers that are passively transported by the wind, which may have various uses in weather or pollution monitoring. Specifically, we investigate centimetre-scale bio-inspired gliding drones that resemble Alsomitra macrocarpa diaspores. In this paper, we propose a new case study on verifying Alsomitra-inspired drones with neural network controllers, with the aim of adhering closely to a target trajectory. We show that our system differs substantially from existing VNN and ARCH competition benchmarks, and show that a combination of tools holds promise for verifying such systems in the future, if certain shortcomings can be overcome. We propose a novel method for robust training of regression networks, and investigate formalisations of this case study in Vehicle and CORA. Our verification results suggest that the investigated training methods do improve performance and robustness of neural network controllers in this application, but are limited in scope and usefulness. This is due to systematic limitations of both Vehicle and CORA, and the complexity of our system reducing the scale of reachability, which we investigate in detail. If these limitations can be overcome, it will enable engineers to develop safe and robust technologies that improve people's lives and reduce our impact on the environment.

Figures (11)

• Figure 1: An artist's impression of a swarm of gliding drones inspired by Alsomitra seeds certini2023alsomitra.
• Figure 2: Overview of a negative feedback control system. For each control iteration, an error signal is calculated by subtracting the current system state (feedback) from the desired system state (input). A controller computes an actuation based on this error, which is applied to a simulated or real system (plant), resulting in some new output state.
• Figure 3: General form of reachability specifications - dots represent the system at successive control time steps, and arrows represent the continuous trajectory of the system. Any trajectory starting in the initial set should never intersect an unsafe set, and always finish in the goal set.
• Figure 4: (a) An Alsomitra seed certini2023alsomitra. (b) A two-dimensional approximation of an Alsomitra seed, with centre of mass (CoM) displaced by $\ell_{\mathrm{CM}}$ (nondimensional form $e_x = \ell_{\mathrm{CM}}/\ell$). (c) Effect of various $e_x$ on gliding trajectories; according to a quasi-steady aerodynamic model ( Li2022model, Sect. \ref{['equations']}). As the CoM is displaced the trajectory behaviour is affected significantly.
• Figure 5: As a control problem, we consider an Alsomitra-inspired microdrone and attempt to follow a linear trajectory in two dimensions.