We propose an interdisciplinary framework that combines Bayesian predictive inference, a well-established tool in Machine Learning, with Formal Methods rooted 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 decision problems into properties with the help of spatio-temporal logic, we can formulate and predict how likely such properties are to be satisfied in the future at a certain location. Moreover, we can leverage our methodology to evaluate and compare models directly on their ability to predict the satisfaction of application-driven properties. The approach is illustrated in 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.

翻译：我们提出了一种跨学科框架，将机器学习领域成熟工具——贝叶斯预测推理——与计算机科学领域的根基性形式化方法相结合。贝叶斯预测推理通过使用生成预测分布的方法或模型，能够一致地整合未知量的不确定性，进而为决策问题提供依据。借助时空逻辑将这些决策问题形式化为具体性质，我们可以预测这些性质在未来特定位置被满足的可能性。此外，该方法论可直接评估和比较模型预测应用驱动性质的能力。研究以城市流动性应用为例，用聚合手机信令数据代理米兰市中心拥挤度，定义了城市拥挤相关的若干理想时空性质（如容错网络、医院可达性）。在验证这些性质对后验预测分布抽样的满足情况后，我们基于整体预测性能与特定性质预测性能，比较了多种贝叶斯时空模型。