(350f) Verification of Neural-Network-Based Explicit Control Systems Using Mixed-Integer Programming

While recent decades have seen the development and widespread adoption of optimization-based control systems, notably model predictive control (MPC) [1], solution of the involved optimization problems in real time can be intractable, owing to model size, nonlinearity, etc [2]. Therefore, the MPC controller is often approximated using surrogate models; neural networks using rectified linear (ReLU) activation functions have gained particular attention, as they can accurately represent complex piecewise-affine functions [3-4]. In general, neural networks can serve as a form of explicit MPC by training them on MPC controllers offline, then using the trained model as a feedback controller online.

Although neural networks can accurately approximate complex functions and be evaluated quickly, they may also be prone to overfitting, limiting their adoption in risk-critical applications. To this end, several works have sought to analyze properties of neural network controllers, such as constraint satisfaction and stability [4-6] or Lyapunov stability [7].

In this work, we show how embedding ReLU neural network controllers in mixed-integer optimization formulations, e.g., see [8-9], enables analyzing extreme behavior of closed-loop system dynamics prior to deployment. We propose two optimization formulations to verify the “trustworthiness” of a neural network controller: (i) identifying the maximum deviation from the original control system and (ii) computing extreme values of system states. The proposed formulations are computationally demonstrated using practically motivated cases studies.

References:

[1] Simkoff, J. M., Lejarza, F., Kelley, M. T., Tsay, C., & Baldea, M. (2020). Process control and energy efficiency. Annual Review of Chemical and Biomolecular Engineering, 11, 423-445.

[2] Vaupel, Y., Hamacher, N. C., Caspari, A., Mhamdi, A., Kevrekidis, I. G., & Mitsos, A. (2020). Accelerating nonlinear model predictive control through machine learning. Journal of Process Control, 92, 261-270.

[3] Kumar, P., Rawlings, J. B., & Wright, S. J. (2021). Industrial, large-scale model predictive control with structured neural networks. Computers & Chemical Engineering, 150, 107291.

[4] Paulson, J. A., & Mesbah, A. (2020). Approximate closed-loop robust model predictive control with guaranteed stability and constraint satisfaction. IEEE Control Systems Letters, 4(3), 719-724.

[5] Hu, H., Fazlyab, M., Morari, M., & Pappas, G. J. (2020, December). Reach-sdp: Reachability analysis of closed-loop systems with neural network controllers via semidefinite programming. In 2020 59th IEEE Conference on Decision and Control (CDC) (pp. 5929-5934). IEEE.

[6] Karg, B., & Lucia, S. (2020, December). Stability and feasibility of neural network-based controllers via output range analysis. In 2020 59th IEEE Conference on Decision and Control (CDC) (pp. 4947-4954). IEEE.

[7] Dai, H., Landry, B., Yang, L., Pavone, M., & Tedrake, R. (2021). Lyapunov-stable neural-network control. arXiv preprint arXiv:2109.14152.

[8] Tsay, C., Kronqvist, J., Thebelt, A., & Misener, R. (2021). Partition-based formulations for mixed-integer optimization of trained ReLU neural networks. Advances in Neural Information Processing Systems, 34.

[9] Anderson, R., Huchette, J., Ma, W., Tjandraatmadja, C., & Vielma, J. P. (2020). Strong mixed-integer programming formulations for trained neural networks. Mathematical Programming, 183(1), 3-39.