# Neural Network Verification for Gliding Drone Control: A Case Study

arXiv: https://arxiv.org/abs/2505.00622 · HTML: https://mlsanity.com/paper/2505.00622/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 36 references that are in the map.
- First posted on arXiv 1 May 2025.

## Builds on (most cited first, 9 of 9)

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Neural Network Robustness as a Verification Property: A Principled Case Study](https://mlsanity.com/paper/2104.01396/) (2021)
- [POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/2304.01218/) (2023)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Comparing differentiable logics for learning with logical constraints](https://mlsanity.com/paper/2407.03847/) (2024)
- [Deep Convolutional Neural Network-Based Autonomous Drone Navigation](https://mlsanity.com/paper/1905.01657/) (2019)
- [Autonomous Drone Swarm Navigation and Multi-target Tracking in 3D Environments with Dynamic Obstacles](https://mlsanity.com/paper/2202.06253/) (2022)
- [Solar-powered shape-changing origami microfliers](https://mlsanity.com/paper/2309.06725/) (2023)

## Abstract (arXiv)

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.