We propose an interdisciplinary framework, Bayesian formal predictive model assessment. It combines Bayesian predictive inference, a well established tool in statistics, with formal verification methods rooting in the computer science community. Bayesian predictive inference allows for coherently incorporating uncertainty about unknown quantities by making use of methods or models that produce predictive distributions, which in turn inform decision problems. By formalizing these problems and the corresponding properties, we can use spatio-temporal reach and escape logic to formulate and probabilistically assess their satisfaction. This way, competing models can directly be compared based on their ability to predict the property satisfaction a posteriori. The approach is illustrated on an urban mobility application, where the crowdedness in the center of Milan is proxied by aggregated mobile phone traffic data. We specify several desirable spatio-temporal properties related to city crowdedness such as a fault-tolerant network or the reachability of hospitals. After verifying these properties on draws from the posterior predictive distributions, we compare several spatio-temporal Bayesian models based on their overall and property-based predictive performance.
翻译:我们提议了一个跨学科框架,即贝耶斯正式预测模型评估,它把贝耶斯预测性预测性预测性推断(一种完善的统计工具)和计算机科学界的正规核查方法结合起来。贝耶斯预测性预测性推断(Bayesian 预测性预测性推断)通过使用产生预测性分布的方法或模型,可以一致地纳入未知数量的不确定性,这反过来又为决策问题提供信息。通过将这些问题和相应的特性正规化,我们可以使用空间时空影响和逃避逻辑来制定和概率评估其满意度。这样,竞争性模型可以根据其事后预测地产满意度的能力直接加以比较。该方法用城市流动应用程序加以说明,因为米兰市中心的拥挤程度通过综合移动电话流量数据加以补充。我们具体说明了与城市人口拥挤有关的一些可取的时空特性,例如过错容忍网络或医院的可达性。在根据事后预测性分布来核实这些特性后,我们根据总体和基于地产的预测性能来比较了几个喷口湾模型。