Conformal Prediction for STL Runtime Verification
Conformal Prediction for STL Runtime Verification
复制标题
DOI：
10.1145/3576841.3585927
复制
发表时间：
2022-11
期刊：
影响因子：
--
通讯作者：
Lars Lindemann;Xin Qin;Jyotirmoy V. Deshmukh;George Pappas
中科院分区：
文献类型：
--
作者：
Lars Lindemann;Xin Qin;Jyotirmoy V. Deshmukh;George Pappas
我们对预测学习系统在运行过程中的故障很感兴趣。特别地，我们考虑了随机学习系统和信号时序逻辑规范，并且我们想要计算当前系统轨迹违反规范的概率。本文提出了两种预测运行时验证算法，根据当前观察到的系统轨迹预测未来的系统状态。由于这些预测可能不准确，我们通过使用保形预测（一种用于不确定性量化的统计工具）构建预测区域来量化预测不确定性。我们的第一个算法直接为规范的满意度度量构造了一个预测区域，这样我们就可以以期望的置信度预测规范违反。第二种算法首先构建系统未来状态的预测区域，并利用这些预测区域获得满意度度量的预测区域。据我们所知，这些是预测运行时验证算法的第一个正式保证，该算法适用于广泛使用的轨迹预测器，如rnn和lstm，同时计算简单，不需要对底层分布进行假设。我们提出了F-16飞机和自动驾驶汽车的数值实验。
We are interested in predicting failures of learning-enabled systems during their operation. Particularly, we consider stochastic learning-enabled systems and signal temporal logic specifications, and we want to calculate the probability that the current system trajectory will violate the specification. The paper presents two predictive runtime verification algorithms that predict future system states from the current observed system trajectory. As these predictions may not be accurate, we construct prediction regions that quantify prediction uncertainty by using conformal prediction, a statistical tool for uncertainty quantification. Our first algorithm directly constructs a prediction region for the satisfaction measure of the specification so that we can predict specification violations with a desired confidence. The second algorithm constructs prediction regions for future system states first, and uses these to obtain a prediction region for the satisfaction measure. To the best of our knowledge, these are the first formal guarantees for a predictive runtime verification algorithm that applies to widely used trajectory predictors such as RNNs and LSTMs, while being computationally simple and making no assumptions on the underlying distribution. We present numerical experiments of an F-16 aircraft and a self-driving car.