论文标题
使用混合构成编程对神经网络控制器的稳定性验证
Stability Verification of Neural Network Controllers using Mixed-Integer Programming
论文作者
论文摘要
我们提出了一个框架，用于稳定验证混合智能线性编程（MILP）代表控制策略。该框架比较了固定的候选策略，该策略承认有效的参数化，可以以低计算成本进行评估，与固定基线策略进行评估，该策略已知稳定但评估昂贵。我们根据基线策略的最坏情况近似误差为候选策略的闭环稳定性提供了足够的条件，我们表明可以通过求解混合企业二次计划（MIQP）来检查这些条件。此外，我们证明了候选策略的稳定区域的外部和内部近似可以通过求解MILP来计算。所提出的框架足以适应包括Relu神经网络（NNS），参数二次计划的最佳解决方案图以及模型预测性控制（MPC）策略的广泛候选策略。我们还根据提出的框架在Python中提供了一个开源工具箱，该工具箱可以轻松验证自定义NN架构和MPC公式。我们在DC-DC Power Converter案例研究中展示了框架的灵活性和可靠性，并研究了其计算复杂性。
We propose a framework for the stability verification of Mixed-Integer Linear Programming (MILP) representable control policies. This framework compares a fixed candidate policy, which admits an efficient parameterization and can be evaluated at a low computational cost, against a fixed baseline policy, which is known to be stable but expensive to evaluate. We provide sufficient conditions for the closed-loop stability of the candidate policy in terms of the worst-case approximation error with respect to the baseline policy, and we show that these conditions can be checked by solving a Mixed-Integer Quadratic Program (MIQP). Additionally, we demonstrate that an outer and inner approximation of the stability region of the candidate policy can be computed by solving an MILP. The proposed framework is sufficiently general to accommodate a broad range of candidate policies including ReLU Neural Networks (NNs), optimal solution maps of parametric quadratic programs, and Model Predictive Control (MPC) policies. We also present an open-source toolbox in Python based on the proposed framework, which allows for the easy verification of custom NN architectures and MPC formulations. We showcase the flexibility and reliability of our framework in the context of a DC-DC power converter case study and investigate its computational complexity.
