贝叶斯机器学习与形式化方法的结合：时空数据的应用
Bayesian Machine Learning meets Formal Methods: An application to spatio-temporal data
AI总结：
本文提出结合贝叶斯预测推理与形式化方法的跨学科框架，用于时空数据决策问题，通过时空逻辑形式化属性并验证，还能比较模型预测性能，在城市移动性应用中得到验证。
摘要：
我们提出了一个跨学科框架，将机器学习中成熟的工具贝叶斯预测推理与计算机科学领域的形式化方法相结合。贝叶斯预测推理通过使用产生预测分布的方法或模型，能够连贯地纳入未知量的不确定性，进而为决策问题提供信息。借助时空逻辑将这些决策问题形式化为属性，我们可以制定并预测未来在特定位置满足这些属性的可能性。此外，我们可以利用该方法直接根据模型预测应用驱动属性满足情况的能力来评估和比较模型。该方法在城市移动性应用中得到了验证，其中米兰市中心的拥挤程度由聚合的手机流量数据代理。我们指定了几个与城市拥挤相关的理想时空属性，如容错网络或医院的可达性。在从后验预测分布中抽取样本验证这些属性后，我们基于整体和基于属性的预测性能比较了几种时空贝叶斯模型。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
