Formal verification of Physics Informed Neural Network Controlled Systems.

Ensuring safe and efficient navigation of autonomous robots in complex real-world environments is a critical challenge. This work presents a novel approach that combines Physics-Informed Neural Networks (PINNs) with Model Predictive Control (MPC) and formal verification techniques to enable provably safe navigation of the TurtleBot Burger mobile robot. The proposed PINN-MPC framework learns the robot’s dynamics from data while respecting physical constraints and integrates formal verification to provide safety guarantees on the generated control actions.

PINN-MPC

We introduce an iterative verification procedure that leverages reachability analysis and the Reluplex neural network verification tool to ensure that the PINN-MPC system generates control actions that satisfy safety requirements, such as collision avoidance and adherence to velocity limits, over a finite time horizon. The approach is evaluated through extensive experiments in both sparse and cluttered environments, demonstrating significant improvements in navigation safety, efficiency, and smoothness compared to baseline methods.

We demonstrate the performance of our approach on hardware robot showing that the formally verified PINN-MPC achieves a 100% success rate in the sparse environment and a 96% success rate in the cluttered environment, with no collisions.

Find the full report here: report