基于反例引导合成的黑箱非线性系统李亚诺稳定性认证（扩展版）

寻找李亚诺函数以认证控制系统的稳定性一直是验证安全关键系统的重要议题。大多数现有方法寻找李亚诺函数需要获取系统动力学。然而，在实际中准确描述控制系统的完整动力学极具具挑战性。最新趋势使用学习型控制系统进一步降低了透明度。因此，针对黑箱系统的方法将具有更广泛的应用前景。我们的工作源于最近利用采样和李亚诺连续性来近似未知动力学的想法。给定李亚诺常数，一个人可以推导出非统计的近似误差上界；因此，对这种近似的强有力认证可用于认证未知动力学。我们通过直接近似李亚诺函数的李导数而非动力学来显著改进这一想法。我们提出基于反例引导归纳合成（CEGIS）中学习者-验证者架构的框架。我们结合区域验证条件和反例引导采样的洞察，实现了对样本的引导搜索，以便逐区域证明稳定性。我们的CEGIS算法进一步保证终止。我们的Numerical实验表明，可以仅用几千个样本即可证明2D和3D系统的稳定性。我们的可视化结果揭示了证明稳定性较为困难的区域。在与现有黑箱方法相比，我们的方法在最佳情况下只需不足0.01%的样本。