Differentiable Reachability for Scalable Verification and Safe Training of Neural Network Controllers

This NSF project aims to make it possible to mathematically guarantee the safe operation of modern automated systems that use learning and artificial intelligence to make control decisions. Robots, aircraft, and self-driving vehicles increasingly rely on machine-learning components, such as neural networks, to interpret their surroundings and decide how to act. But they also make it hard to prove that a system will behave safely, especially in unfamiliar or rapidly changing conditions. The project will bring transformative change by making safety verification fast enough to be woven directly into the design of these systems, rather than performed only as a separate check afterward. This will be achieved by developing new mathematical theory together with algorithmic tools that run efficiently on modern computational platforms so that safety guarantees can be computed, and even improved, automatically during design. The intellectual merit of the project includes new foundational theory and scalable algorithms for analyzing, verifying, and designing feedback control systems that contain neural networks, unifying advances across control theory and high-performance computation. The broader impacts of the project include training students at all levels, engaging undergraduates through a team-based research program, developing interdisciplinary courses that bridge control, machine learning, and computer vision, and releasing open-source software; the underlying methods also apply broadly to autonomous driving, assistive robotics, power grids, and transportation networks. The technical goal of this project is a scalable, differentiable framework for verifiable learning-based feedback control. Its central tool is reachability analysis, which computes the set of all possible future states a system may enter, giving a rigorous basis for certifying safety properties such as obstacle avoidance and staying within operating limits. Traditional reachability methods are slow, do not scale to high dimensions, and cannot be differentiated, making them impractical during design. The project addresses these challenges by building on monotone systems theory and contraction theory—mathematical tools describing how nearby trajectories evolve—together with interval analysis, which rigorously encloses quantities within upper and lower bounds. These ideas yield efficient, reliable overapproximations of reachable sets that scale to large systems and neural controllers. By implementing them in JAX, a Python framework offering automatic differentiation and graphics-processing-unit (GPU) acceleration, reachability is made differentiable, allowing controllers to be trained with built-in safety and tracking guarantees. The framework is extended to motion planning and to perception-based control from camera images, and validated on robotic testbeds such as bimanual manipulation. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.