基于 Zubov 采样与迭代域扩张的两阶段稳定神经网络控制器学习

基于学习的神经网络（NN）控制策略展现出了令人印象深刻的经验性能。然而，由于缺乏稳定且可扩展的训练与验证算法，获取这些学习到的神经控制器的稳定性保证和吸引域估计极具挑战性。尽管该领域先前的工作取得了巨大成功，但其框架中仍存在较多保守性。在这项工作中，我们提出了一种新颖的两阶段训练框架，以联合合成连续时间系统的控制器与 Lyapunov 函数。通过利用受 Zubov 启发的吸引域表征来直接估计稳定性边界，我们提出了一种新颖的训练数据采样策略和域更新机制，显著减少了训练中的保守性。此外，与现有的连续时间系统工作中依赖 SMT 求解器来形式化验证 Lyapunov 条件不同，我们将最先进的神经网络验证器 $\alpha,\!\beta$-CROWN 进行了扩展，使其具备通过动态系统 Jacobian 矩阵执行自动边界传播的能力，并提出了一种避免昂贵二分法的新颖验证方案。为了证明我们方法的有效性，我们在多个具有挑战性的多维度非线性系统上进行了合成与验证控制器的数值实验。我们表明，与基线相比，我们的训练可以产生体积大 $5 - 1.5\cdot 10^{5}$ 倍的吸引域，并且与传统的 SMT 求解器 dReal 相比，我们在连续系统上的验证速度可提高 $40-10{,}000$ 倍。我们的代码可在 https://github.com/Verified-Intelligence/Two-Stage_Neural_Controller_Training 获取。