This paper presents a formal verification guided approach for a principled design and implementation of robust and resilient learning-enabled systems. We focus on learning-enabled state estimation systems (LE-SESs), which have been widely used in robotics applications to determine the current state (e.g., location, speed, direction, etc.) of a complex system. The LE-SESs are networked systems, composed of a set of connected components including: Bayes filters for state estimation, and neural networks for processing sensory input. We study LE-SESs from the perspective of formal verification, which determines the satisfiabilty of a system model against the specified properties. Over LE-SESs, we investigate two key properties -- robustness and resilience -- and provide their formal definitions. To enable formal verification, we reduce the LE-SESs to a novel class of labelled transition systems, named {PO}^2-LTS in the paper, and formally express the properties as constrained optimisation objectives. We prove that the verification problems are NP-complete. Based on {PO}^2-LTS and the optimisation objectives, practical verification algorithms are developed to check the satisfiability of the properties on the LE-SESs. As a major case study, we interrogate a real-world dynamic tracking system which uses a single Kalman Filter (KF) -- a special case of Bayes filter -- to localise and track a ground vehicle. Its perception system, based on convolutional neural networks, processes a high-resolution Wide Area Motion Imagery (WAMI) data stream. Experimental results show that our algorithms can not only verify the properties of the WAMI tracking system but also provide representative examples, the latter of which inspired us to take an enhanced LE-SESs design where runtime monitors or joint-KFs are required. Experimental results confirm the improvement in the robustness of the enhanced design.

翻译：本文提出了一种基于形式化验证的原则性方法，用于设计并实现鲁棒且弹性的学习型系统。我们聚焦于学习型状态估计系统（LE-SES），该系统在机器人领域广泛应用，用于确定复杂系统的当前状态（如位置、速度、方向等）。LE-SES属于网络化系统，由一组互联组件构成，包括用于状态估计的贝叶斯滤波器，以及用于处理感官输入的神经网络。我们从形式化验证视角研究LE-SES，该方法通过判定系统模型是否满足特定属性来验证其正确性。针对LE-SES，我们探讨了两个关键属性——鲁棒性与弹性，并给出了形式化定义。为实现形式化验证，我们将LE-SES约简为一类新型标注迁移系统（本文记为{PO}^2-LTS），并将属性形式化表述为约束优化目标。我们证明验证问题为NP完全问题。基于{PO}^2-LTS与优化目标，我们开发了实用化验证算法，以检验LE-SES上属性的可满足性。作为主要案例研究，我们检验了一个真实动态跟踪系统，该系统采用单一卡尔曼滤波器（KF，贝叶斯滤波器的特例）对地面车辆进行定位与跟踪，其基于卷积神经网络的感知系统处理高分辨率广域运动影像（WAMI）数据流。实验结果表明：我们的算法不仅能验证WAMI跟踪系统的属性，还能提供代表性反例；后者启发我们提出了增强型LE-SES设计（需运行时监控器或联合KF）。实验结果证实了增强设计在鲁棒性上的提升。