Search arXiv⌕ Search

arXiv · 2505.00622

Neural Network Verification for Gliding Drone Control: A Case Study

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.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Colin Kessler, Ekaterina Komendantskaya, Marco Casadio, Ignazio Maria Viola, Thomas Flinkow, Albaraa Ammar Othman, Alistair Malhotra, Robbie McPherson. 2025-05-01. Neural Network Verification for Gliding Drone Control: A Case Study. https://arxiv.org/abs/2505.00622

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

A Scalable Multi-Robot Framework for Decentralized and Asynchronous Perception-Action-Communication Loops

We develop a decentralized Perception-Action-Communication (PAC) system for multi-robot teams that enables them to collaborate in large scale, outdoor environments. Our system natively supports deployments at any scale by leveraging a graph neural network (GNN) to diffuse information hop-by-hop across the fleet's network. This achieves global collaboration from individual robots limited to local sensing and communication. Fully asynchronous, the core modules of PAC: perception, inter-robot communication, message aggregation and action are clocked at different frequencies with information flowing between them through buffers. We implement the PAC system as a series of highly extensible ROS2 nodes to serve as the foundational infrastructure for deployable swarm systems. PAC is validated in the real world with outdoor experiments with up to N=20 quadrotor robots and in simulations based on real-world data with up to N=100. These validations show that our system upholds crucial properties for field-deployable robot collectives: scalability, resiliency and repeatability.

cs.RO↗

DexWrist: A Robotic Wrist for Constrained and Dynamic Manipulation

Development of dexterous manipulation hardware has primarily focused on hands and grippers. However, these end-effectors are often paired with bulky and highly stiff wrists that limit performance in human environments. More recent designs have adopted backdrivable actuation, but are still difficult to model and control due to coupled kinematics or high mechanical inertia from heavy links. We present DexWrist, a compact robotic wrist combining quasi-direct-drive actuation with a decoupled parallel kinematic mechanism to advance manipulation in highly constrained environments and enable dynamic, contact-rich tasks. It delivers 3.75$\pm$0.05 Nm rated torque, 0.33$\pm$0.06 Nm backdrive torque, 10.15$\pm$1.34 Hz torque bandwidth, $\pm 40^\circ$ ROM in both DOFs, and a diagonal velocity-constraint Jacobian (one-to-one motor-to-DOF mapping) in a 0.97 kg package. In practice, these properties increase workspace in clutter and stabilize contact without finely tuned admittance control. We evaluate DexWrist as a drop-in upgrade in simulation and on three robot arms across constrained and contact-rich tasks. In learned policy evaluations on the AgileX PiPER and UR3e, DexWrist achieved 50-76% relative improvements in success rate and reduced autonomous task completion times by 3-5x; on a torque-controlled Franka FR3, where a strong joint-impedance baseline already succeeds, it still completed the task 1.4x faster. Project page and videos: https://martinpeticco.com/dexwrist

cs.RO↗

Imagine2Act: Leveraging Object-Action Motion Consistency from Imagined Goals for Robotic Manipulation

Relational object rearrangement (ROR) tasks (e.g., insert flower to vase) require a robot to manipulate objects with precise semantic and geometric reasoning. Existing approaches either rely on pre-collected demonstrations that struggle to capture complex geometric constraints or generate goal-state observations to capture semantic and geometric knowledge, but fail to explicitly couple object transformation with action prediction, resulting in errors due to generative noise. To address these limitations, we propose Imagine2Act, a 3D imitation-learning framework that incorporates semantic and geometric constraints of objects into policy learning to tackle high-precision manipulation tasks. We first generate imagined goal images conditioned on language instructions and reconstruct corresponding 3D point clouds to provide robust semantic and geometric priors. These imagined goal point clouds serve as additional inputs to the policy model, while an object-action consistency strategy with soft pose supervision explicitly aligns predicted end-effector motion with generated object transformation. This design enables Imagine2Act to reason about semantic and geometric relationships between objects and predict accurate actions across diverse tasks. Experiments in both simulation and the real world demonstrate that Imagine2Act outperforms previous state-of-the-art policies. More visualizations can be found at https://sites.google.com/view/imagine2act.

cs.RO↗