Reinforcement learning (RL) algorithms interact with their environment in a
trial-and-error fashion. Such interactions can be expensive, inefficient, and
timely when learning on a physical system rather than in a simulation. This
work develops new runtime verification techniques to predict when the learning
phase has not met or will not meet qualitative and timely expectations. This
paper presents three verification properties concerning the quality and
timeliness of learning in RL algorithms. With each property, we propose design
steps for monitoring and assessing the properties during the system's
operation.

该研究提出了针对强化学习算法的运行时验证技术，用于预测学习阶段是否满足质量和及时性的期望，并提出了三个验证属性和相应的监测与评估步骤。

强化学习算法学习属性的运行时验证

Runtime Verification of Learning Properties for Reinforcement Learning  Algorithms

Deep neural networks (DNNs) are instrumental in realizing complex perception
systems. As many of these applications are safety-critical by design,
engineering rigor is required to ensure that the functional insufficiency of
the DNN-based perception is not the source of harm. In addition to conventional
static verification and testing techniques employed during the design phase,
there is a need for runtime verification techniques that can detect critical
events, diagnose issues, and even enforce requirements. This tutorial aims to
provide readers with a glimpse of techniques proposed in the literature. We
start with classical methods proposed in the machine learning community, then
highlight a few techniques proposed by the formal methods community. While we
surely can observe similarities in the design of monitors, how the decision
boundaries are created vary between the two communities. We conclude by
highlighting the need to rigorously design monitors, where data availability
outside the operational domain plays an important role.

深度神经网络在复杂感知系统方面起着重要作用，但为了确保其功能不足不会造成危害，除了静态验证和测试方法外，还需要运行时验证技术来检测关键事件、诊断问题并强制执行要求。本教程介绍了文献中提出的技术方法，包括机器学习界经典方法和形式方法界的一些技术，同时强调了严格设计监视器的重要性，其中操作域外的数据可用性起着重要作用。

运行时监测基于深度学习的感知

Runtime Monitoring DNN-Based Perception

As AI and machine-learned software are used increasingly for making decisions
that affect humans, it is imperative that they remain fair and unbiased in
their decisions. To complement design-time bias mitigation measures, runtime
verification techniques have been introduced recently to monitor the
algorithmic fairness of deployed systems. Previous monitoring techniques assume
full observability of the states of the (unknown) monitored system. Moreover,
they can monitor only fairness properties that are specified as arithmetic
expressions over the probabilities of different events. In this work, we extend
fairness monitoring to systems modeled as partially observed Markov chains
(POMC), and to specifications containing arithmetic expressions over the
expected values of numerical functions on event sequences. The only assumptions
we make are that the underlying POMC is aperiodic and starts in the stationary
distribution, with a bound on its mixing time being known. These assumptions
enable us to estimate a given property for the entire distribution of possible
executions of the monitored POMC, by observing only a single execution. Our
monitors observe a long run of the system and, after each new observation,
output updated PAC-estimates of how fair or biased the system is. The monitors
are computationally lightweight and, using a prototype implementation, we
demonstrate their effectiveness on several real-world examples.

随着人工智能和机器学习软件在影响人类的决策中的应用日益增多，保持公正无偏成为当务之急。为了补充设计时的偏见缓解措施，最近引入了运行时验证技术来监测部署系统的算法公平性。本研究将公平性监测扩展到部分观测的马尔可夫链 (POMC) 建模的系统，并且适用于包含事件序列中数值函数期望值的算术表达式的规范。我们的监测器通过仅观测到单个执行，估计了受监测的 POMC 可能执行的整个分布的给定属性。这些监测器在每次新观测后输出更新的 PAC 估计，以评估系统的公平性或偏见。监测器计算量轻，并使用原型实现在几个真实世界的示例中展示了其有效性。