善恶之 demons 与 angels：有限精度下的安全控制保障

随着神经网络 (NN) 在安全关键型神经网络控制的网络-物理系统 (NNCS) 中变得越来越普遍，形式化保证其安全性变得至关重要。对于这些系统，安全性必须在整个运行过程中得到保证，这需要无限时间范围的验证。为了验证 NNCS 的无限时间范围安全性，最近的方法利用微分动态逻辑 (dL)。然而，这些 dL 基于的保证依赖于理想化的实值 NN 语义，未能考虑有限精度实现所引入的舍入误差。本文通过将鲁棒性纳入安全验证中，以有限精度扰动（在感知、执行和计算中）为单位，弥合了理论保证与实际实现之间的差距。我们将问题建模为一个由负责控制动作的善鬼和负责引入扰动的恶天使组成的混合博弈。这种表述使我们能够形式化证明对给定（有界）扰动的鲁棒性。借助该界限，我们采用最新的混合精度定点调谐器来合成可靠且高效的实现，从而提供一个完整的端到端解决方案。我们在汽车和航空领域的案例研究中进行评估，产生了具有严格无限时间范围安全保证的高效 NN 实现。