WeB03 – Bridging Learning-Enabled Control with Modern Neural Network Verifier: A Unified Framework with α,β-CROWN

Deep learning–based controllers have gained substantial popularity due to their strong empirical performance. However, their deployment in safety-critical scenarios remains a major concern. In this tutorial, we bridge learning-based control with the modern neural network verifier α,β-CROWN, a state of-the-art method that scales via GPU-parallel symbolic linear bound propagation and branch-and-bound refinement. As many control guarantees can be rewritten as inequality constraints over a computation graph, α,β-CROWN enables faster, more generic, and more scalable certification beyond what classical SMT/MILP/SDP pipelines can typically handle.

This tutorial aims to systematically introduce α,β-CROWN to the control community as a fresh perspective for tackling the verification of nonlinear and learned controllers. Participants will learn the basics of the α,β-CROWN toolbox, and how to reformulate and verify core control properties, such as Lyapunov stability, safety via barrier functions, contraction-metric analysis, and related robustness conditions, using α,β-CROWN. We will also discuss emerging training frameworks that jointly synthesize controllers and verifier-friendly certificates, and we will provide hands-on, runnable demos so attendees can apply α,β-CROWN to their own tasks right away.

Schedule of Talks