貝葉斯機(jī)器學(xué)習(xí)與形式化方法的結(jié)合：應(yīng)用于時(shí)空數(shù)據(jù)

Bayesian Machine Learning Meets Formal Methods: AnApplication to Spatio-Temporal Data

貝葉斯機(jī)器學(xué)習(xí)與形式化方法的結(jié)合：應(yīng)用于時(shí)空數(shù)據(jù)

https://dl.acm.org/doi/epdf/10.1145/3708479

摘要

我們提出一種跨學(xué)科框架，將貝葉斯預(yù)測(cè)推斷（Bayesian predictive inference）——一種機(jī)器學(xué)習(xí)中成熟可靠的工具——與形式化方法（formal methods）——植根于計(jì)算機(jī)科學(xué)領(lǐng)域——相結(jié)合。貝葉斯預(yù)測(cè)推斷通過采用生成預(yù)測(cè)分布的方法或模型，能夠一致地整合關(guān)于未知量的不確定性，進(jìn)而為決策問題提供信息支持。借助時(shí)空邏輯（spatio-temporal logic），我們將這些決策問題形式化為特定屬性，從而可對(duì)這些屬性在將來某一時(shí)刻、某一地點(diǎn)得以滿足的概率進(jìn)行建模與預(yù)測(cè)。此外，我們還可利用該方法論，直接依據(jù)模型對(duì)應(yīng)用驅(qū)動(dòng)型屬性（application-driven properties）滿足程度的預(yù)測(cè)能力，對(duì)其進(jìn)行評(píng)估與比較。

該方法通過一個(gè)城市交通應(yīng)用案例加以闡釋：我們以聚合的手機(jī)信令數(shù)據(jù)作為代理變量，表征米蘭市中心的人群密集程度。我們定義了若干與城市擁擠狀況相關(guān)的理想時(shí)空屬性，例如容錯(cuò)型網(wǎng)絡(luò)連通性或醫(yī)院可達(dá)性等。在從后驗(yàn)預(yù)測(cè)分布中抽取樣本并驗(yàn)證這些屬性后，我們基于模型的整體預(yù)測(cè)性能及其針對(duì)具體屬性的預(yù)測(cè)能力，對(duì)多種時(shí)空貝葉斯模型進(jìn)行了比較。

CCS 概念分類：
? 數(shù)學(xué)計(jì)算 → 貝葉斯計(jì)算；
? 軟件及其工程 → 形式化軟件驗(yàn)證；
? 計(jì)算方法學(xué) → 模型驗(yàn)證與確認(rèn)。

附加關(guān)鍵詞與短語：貝葉斯預(yù)測(cè)推斷、時(shí)空模型、形式化驗(yàn)證方法、后驗(yàn)預(yù)測(cè)驗(yàn)證、城市交通。

1 引言

形式化驗(yàn)證方法在計(jì)算機(jī)科學(xué)領(lǐng)域有著悠久的傳統(tǒng)。其最初源于硬件與軟件系統(tǒng)領(lǐng)域，旨在通過對(duì)復(fù)雜邏輯屬性滿足情況的驗(yàn)證，為所分析實(shí)現(xiàn)的正確性提供強(qiáng)有力的保障。盡管形式化方法最初是為確定性系統(tǒng)而發(fā)展起來的，但如今已在隨機(jī)系統(tǒng)中得到廣泛應(yīng)用——在隨機(jī)系統(tǒng)中，同一組輸入可能對(duì)應(yīng)多組隨機(jī)輸出。

針對(duì)隨機(jī)系統(tǒng)的傳統(tǒng)形式化驗(yàn)證方法是概率模型檢測(cè)（probabilistic model checking），由文獻(xiàn) [11, 33] 獨(dú)立提出。然而，對(duì)于規(guī)模龐大的隨機(jī)系統(tǒng)而言，基于數(shù)值計(jì)算的概率模型檢測(cè)在實(shí)踐中往往不可行 [37]，由此催生了新方法，例如統(tǒng)計(jì)模型檢測(cè)（Statistical Model Checking, SMC；參見 [23] 的最新綜述）。SMC 是概率模型檢測(cè)的一種基于仿真的變體：其核心思想是通過蒙特卡洛積分估算邏輯屬性滿足的概率——即從隨機(jī)系統(tǒng)中生成大量軌跡（trajectories），對(duì)每條軌跡判斷其是否滿足目標(biāo)邏輯屬性，再對(duì)所有仿真結(jié)果取算術(shù)平均。

得益于其天然的并行性，SMC 的計(jì)算瓶頸主要在于：在每次迭代中對(duì)復(fù)雜邏輯屬性進(jìn)行仿真與驗(yàn)證的開銷。此時(shí)，形式化方法便發(fā)揮關(guān)鍵作用——可將復(fù)雜屬性轉(zhuǎn)化為邏輯公式，并借助針對(duì)特定邏輯類型優(yōu)化的高效算法實(shí)現(xiàn)自動(dòng)驗(yàn)證。

將屬性表述為邏輯公式的主要優(yōu)勢(shì)在于：已有高效的監(jiān)控算法（monitoring algorithms）可自動(dòng)、快速地判斷這些屬性是否被滿足，以及滿足程度如何。此外，相較于自然語言描述，形式邏輯能確保屬性定義的無歧義性，從而降低因主觀理解偏差或誤讀而導(dǎo)致錯(cuò)誤的風(fēng)險(xiǎn)。正因其良好的可擴(kuò)展性，SMC 已日益廣泛地應(yīng)用于多個(gè)領(lǐng)域，尤其是生物系統(tǒng)與信息物理系統(tǒng)（例如文獻(xiàn) [31] 將連續(xù)時(shí)間馬爾可夫鏈模型用于共享單車系統(tǒng)的建模）。

現(xiàn)有 SMC 應(yīng)用通常將模型參數(shù)固定為特定取值（如最大似然估計(jì)值），并基于這些固定參數(shù)對(duì)隨機(jī)系統(tǒng)進(jìn)行仿真，未考慮參數(shù)不確定性如何自然傳播至屬性滿足概率之中。盡管已有對(duì) SMC 的拓展嘗試（如貝葉斯 SMC [38]）可納入關(guān)于屬性滿足概率的先驗(yàn)信息，但其生成的有限軌跡集仍來自參數(shù)固定的模型。另一種思路是文獻(xiàn) [6–8] 所采取的：將參數(shù)本身直接視為不確定量，并針對(duì)一組可能的參數(shù)組合計(jì)算屬性滿足概率。然而，這些工作雖然依據(jù)先驗(yàn)知識(shí)設(shè)定了參數(shù)范圍，但并未基于實(shí)際觀測(cè)數(shù)據(jù)對(duì)參數(shù)進(jìn)行估計(jì)。

本文提出一種貝葉斯機(jī)器學(xué)習(xí)方法，既可自然地處理不確定性傳播問題，又能同時(shí)從數(shù)據(jù)中學(xué)習(xí)參數(shù)的取值。我們所提出的框架將經(jīng)典 SMC 方法拓展為一個(gè)全貝葉斯框架：利用用于模型估計(jì)的馬爾可夫鏈蒙特卡洛（MCMC）算法，從貝葉斯預(yù)測(cè)分布中抽取軌跡，并對(duì)該軌跡集進(jìn)行驗(yàn)證與監(jiān)控。貝葉斯預(yù)測(cè)推斷通過提供完整的后驗(yàn)預(yù)測(cè)分布，可一致地刻畫被建模隨機(jī)變量（未知或未來取值）的不確定性。

這一新穎框架為數(shù)據(jù)建模與統(tǒng)計(jì)分析提供了一種統(tǒng)一途徑，能夠一致地納入所指定屬性的不確定性。我們相信，貝葉斯視角下的不確定性處理可極大豐富 SMC；同時(shí)，形式化方法在（貝葉斯）機(jī)器學(xué)習(xí)社區(qū)中的引入，亦為面向應(yīng)用的預(yù)測(cè)、模型評(píng)估與比較開辟了新路徑。

在大多數(shù)應(yīng)用場(chǎng)景中，（貝葉斯）機(jī)器學(xué)習(xí)模型的預(yù)測(cè)結(jié)果通常僅在事后（即估計(jì)完成后）與觀測(cè)數(shù)據(jù)進(jìn)行比對(duì)，以評(píng)估模型性能。然而，這些預(yù)測(cè)結(jié)果本身并不直接轉(zhuǎn)化為決策，而是需經(jīng)過變換、壓縮，并與決策問題相關(guān)的其他規(guī)則或約束條件相結(jié)合。舉例如下：

• 一套算法交易策略可能使用股票收益預(yù)測(cè)模型，并依規(guī)則“若預(yù)測(cè)收益分布的90%分位數(shù)連續(xù)三日超過10%，則下達(dá)賣出指令”來生成交易信號(hào)；
• 交通管理人員可能依據(jù)模型預(yù)測(cè)——當(dāng)城市主干道擁擠度將超過某閾值時(shí)——決定實(shí)施交通疏導(dǎo)。

此類規(guī)則還可用于構(gòu)建預(yù)測(cè)模型（尤其是“黑箱”模型）的監(jiān)控機(jī)制，例如保障預(yù)測(cè)結(jié)果的公平性。

尤其對(duì)于高維復(fù)雜模型，這些與決策相關(guān)的規(guī)則或?qū)傩酝请S機(jī)變量的高度非線性函數(shù)，研究者所關(guān)注的正是其預(yù)測(cè)分布本身。對(duì)這類屬性進(jìn)行事前驗(yàn)證（ex-ante），以及將其納入事后模型檢驗(yàn)與比較（ex-post posterior model checking and comparison）之中，可為建模者與決策者提供寶貴的洞見，并使分析真正貼合具體決策問題的實(shí)際需求。我們主張：在評(píng)估與比較不同機(jī)器學(xué)習(xí)模型的性能時(shí)，應(yīng)聚焦于系統(tǒng)所需滿足的應(yīng)用導(dǎo)向與決策導(dǎo)向的具體要求或?qū)傩?/strong>。

為實(shí)現(xiàn)這一目標(biāo)，我們借鑒計(jì)算機(jī)科學(xué)中 SMC 與驗(yàn)證領(lǐng)域的既有成果，對(duì)這些屬性的后驗(yàn)預(yù)測(cè)滿足概率，以及其后驗(yàn)預(yù)測(cè)可靠性（或魯棒性）度量進(jìn)行近似估算。我們進(jìn)而將貝葉斯預(yù)測(cè)滿足概率與后驗(yàn)預(yù)測(cè)魯棒性定義為關(guān)鍵關(guān)注量（quantities of interest），并展示如何利用這些指標(biāo)對(duì)一組時(shí)空貝葉斯模型進(jìn)行比較。此類基于屬性的模型比較可補(bǔ)充傳統(tǒng)的預(yù)測(cè)評(píng)估指標(biāo)（如對(duì)數(shù)預(yù)測(cè)密度得分）；正如文獻(xiàn) [1] 在氣象預(yù)報(bào)領(lǐng)域所討論的，精心設(shè)計(jì)的、反映預(yù)報(bào)者關(guān)注信息的多元預(yù)報(bào)預(yù)排序函數(shù)（pre-rank functions），往往比通用指標(biāo)更具決策相關(guān)性。

我們通過時(shí)空面域數(shù)據(jù)（spatio-temporal areal data）演示該新方法：此類數(shù)據(jù)在多個(gè)面域單元（areal units）上隨時(shí)間采集，并可通過鄰接矩陣計(jì)算單元間的空間距離。具體而言，我們聚焦城市交通應(yīng)用——城市人口密度動(dòng)態(tài)在空間與時(shí)間維度上均呈現(xiàn)高度變異性。對(duì)此類問題構(gòu)建能準(zhǔn)確預(yù)測(cè)未來人口動(dòng)態(tài)的貝葉斯時(shí)空模型，對(duì)城市規(guī)劃決策者至關(guān)重要（例如用于資源配置、交通疏導(dǎo)、臨時(shí)擴(kuò)容移動(dòng)通信網(wǎng)絡(luò)），且對(duì)環(huán)境、經(jīng)濟(jì)與公共健康具有深遠(yuǎn)影響 [15]；后者在新冠疫情背景下尤為凸顯。

近年來，學(xué)界廣泛采用手機(jī)信令流量數(shù)據(jù)作為人口流動(dòng)的代理變量（參見 [4, 12, 15, 32] 及其中參考文獻(xiàn)），應(yīng)用涵蓋：無普查數(shù)據(jù)地區(qū)的人口密度估算 [36]、交通流量預(yù)測(cè) [19]、傳染病傳播建模 [5, 10] 等。然而，受限于手機(jī)數(shù)據(jù)的高維性，僅少數(shù)研究在城市規(guī)劃語境下采用復(fù)雜的（貝葉斯）建模工具：

• Cadonna 等人 [9] 基于意大利某電信公司數(shù)據(jù)，為米蘭各區(qū)域構(gòu)建了具空間聚類結(jié)構(gòu)的時(shí)空模型；
• Wang 等人 [35] 在中國深圳開展實(shí)證研究，將人口統(tǒng)計(jì)與混合用地指數(shù)納入貝葉斯建模框架，以探究人口波動(dòng)的空間格局。

為說明目的，本文采用“意大利電信大數(shù)據(jù)挑戰(zhàn)賽”（Telecom Italia Big Data Challenge）的開源數(shù)據(jù)：該數(shù)據(jù)集包含2013年11月至12月期間，米蘭市固定空間網(wǎng)格單元上聚合的電信活動(dòng)數(shù)據(jù)。我們的研究結(jié)果從兩方面深化了對(duì)米蘭城市動(dòng)態(tài)的理解：其一，通過選出性能最優(yōu)的模型，識(shí)別出具有相似時(shí)間模式的區(qū)域集群；其二，定量刻畫了所提出的時(shí)空屬性在何時(shí)、以何種程度得以滿足。

本文結(jié)構(gòu)如下：
第2節(jié)介紹面向時(shí)空數(shù)據(jù)的形式化驗(yàn)證概念，并提出若干新的、面向具體應(yīng)用場(chǎng)景的屬性；
第3節(jié)闡述貝葉斯預(yù)測(cè)框架如何納入不確定性，并提出基于屬性滿足情況的預(yù)測(cè)評(píng)估指標(biāo)；
第4節(jié)展示實(shí)證數(shù)據(jù)與分析結(jié)果；
第5節(jié)總結(jié)全文，并對(duì)未來研究方向進(jìn)行展望。

2 面向面域時(shí)空數(shù)據(jù)的形式化驗(yàn)證

2.1 所用形式邏輯簡(jiǎn)介

為將特定應(yīng)用場(chǎng)景的屬性融入貝葉斯機(jī)器學(xué)習(xí)工作流，我們引入形式化驗(yàn)證方法，用于指定并驗(yàn)證此類屬性。形式化驗(yàn)證方法的目標(biāo)是檢查一個(gè)（隨機(jī)）系統(tǒng)是否滿足某些以某種形式語言表述的屬性或要求。基于邏輯的形式化語言允許使用抽象且簡(jiǎn)潔的符號(hào)（而非詳盡具體的表達(dá)式）來定義屬性，從而能夠清晰、精確且無歧義地描述這些屬性。邏輯公式由預(yù)定義的語法生成，該語法規(guī)則規(guī)定了如何從原子命題出發(fā)遞歸地構(gòu)建公式。原子命題是任何邏輯的基本構(gòu)成單元，是必須為真或?yàn)榧俚年愂龌驍嘌浴４送猓壿嬤€配有驗(yàn)證算法，可自動(dòng)判斷系統(tǒng)是否滿足這些公式。

過去十年中，人們投入大量努力開發(fā)面向時(shí)空屬性的基于邏輯的規(guī)范語言與監(jiān)控框架。時(shí)空邏輯通過一組算子將原子命題組合成公式：包括基本的布爾算子——否定（?）和析取（∨），以及用于描述時(shí)間演進(jìn)的時(shí)序算子和用于空間推理的空間算子。

在本文中，我們采用被稱為時(shí)空可達(dá)與逃逸邏輯（Spatio-Temporal Reach and Escape Logic, STREL，[28]）的形式語言作為參考規(guī)范語言。接下來我們將更詳細(xì)地描述我們所關(guān)注的應(yīng)用場(chǎng)景、STREL 語言本身，以及它如何應(yīng)用于時(shí)空數(shù)據(jù)。在我們的應(yīng)用中，我們考慮一個(gè)由 i = 1, …, I 個(gè)區(qū)域組成的網(wǎng)格，覆蓋米蘭市中心，其中在 t = 1, …, T 時(shí)刻收集擁擠度測(cè)量值 y（此處一個(gè)時(shí)間點(diǎn)代表一個(gè)10分鐘的時(shí)間區(qū)間）。兩個(gè)面域單元 i 和 j 之間的距離是指從單元 i 到單元 j 所需“跳轉(zhuǎn)”（hops）或“跳躍”次數(shù)最少的路徑。該距離可通過使用對(duì)稱鄰接矩陣計(jì)算得出，其中第 i 行第 j 列（反之亦然）的元素在區(qū)域 i 和 j 相鄰時(shí)為1，否則為0。雖然該框架較為通用，但我們主要關(guān)注預(yù)測(cè)背景下的屬性。因此，我們將制定并考慮關(guān)于未來 h 步內(nèi)、給定時(shí)間 t 之后的擁擠度值的要求。我們所制定的每一項(xiàng)要求均可針對(duì)每個(gè)面域單元 i = 1, ..., I 進(jìn)行檢驗(yàn)。

STREL 的語法（文法）如下：

它定義了可用于構(gòu)建公式的規(guī)則（運(yùn)算符）集合，以及這些規(guī)則之間的組合方式。符號(hào) | 用于分隔不同的規(guī)則選項(xiàng)，表示在構(gòu)建公式時(shí)可從中任選其一。

所有可使用 STREL 指定的屬性集合，是通過遞歸構(gòu)建公式而獲得的：從第一條規(guī)則 φ := ? 開始，該規(guī)則將屬性 φ 設(shè)定為一個(gè)原子命題 ?；然后迭代地利用文法中定義的一組算子構(gòu)建新的公式。原子命題可以描述位置或時(shí)間點(diǎn)的特征（例如，某個(gè)位置是否包含醫(yī)院，或某個(gè)時(shí)間點(diǎn)是否對(duì)應(yīng)午夜），或者可以被定義為涉及相關(guān)變量的不等式——例如，在我們的案例中，城市擁擠度 y 可表示為 y > c 或 y < c，其中 c ∈ ?。這些命題可以針對(duì)每個(gè)位置 i 和時(shí)間 s 進(jìn)行定義，從而將 y?,? 與位置和時(shí)間相關(guān)的閾值 c?,? 進(jìn)行比較。請(qǐng)注意，原子命題中使用的量是單變量的，且在撰寫本文時(shí)，邏輯本身無法將更復(fù)雜的不等式（如 y?,? > y?,??? + c?,?）表達(dá)為原子命題。

如上所述，?φ 表示命題 φ 的否定，表達(dá)式 φ? ∨ φ? 表示屬性 φ? 和 φ? 的析取。其他算子可通過組合這些算子獲得。例如，合取 φ? ∧ φ? 由 ?((?φ?) ∨ (?φ?)) 給出，而蘊(yùn)含 φ? → φ? 由 (?φ?) ∨ φ? 給出。

“最終”算子 F≤? 表示某個(gè)屬性在未來時(shí)間區(qū)間 (t, t+h] 內(nèi)至少發(fā)生一次，并且可以在每個(gè)位置 i 上進(jìn)行檢驗(yàn)。對(duì)于離散觀測(cè)系統(tǒng)，假設(shè)變量在時(shí)間點(diǎn)之間保持恒定行為。例如，在我們的案例中，公式 F≤?????(y > 1,000) 意味著在未來30分鐘內(nèi)，擁擠度水平必須至少有一次超過1,000。同樣，該屬性可以在每個(gè)位置 i 和每個(gè)時(shí)間點(diǎn) t ∈ 1, ..., T-h 上進(jìn)行評(píng)估。另一個(gè)時(shí)序算子是“始終”算子 G≤?φ，它可被定義為 G≤?φ ≡ ?F≤??φ。它檢查屬性 φ 在未來時(shí)間區(qū)間 (t, t+h] 內(nèi)的所有時(shí)間點(diǎn)上的出現(xiàn)情況。當(dāng)上下文要求對(duì)感興趣的時(shí)間段也設(shè)定下界時(shí)，我們采用基于區(qū)間的記號(hào)，如 F??,??，以表示區(qū)間 [t+a, t+b]。

最后，φ??≤dφ? 是距離 d ∈ ?? 的空間可達(dá)算子。它表示：僅需經(jīng)過滿足 φ? 的地點(diǎn)，即可到達(dá)滿足 φ? 的區(qū)域，且路徑總長度至多為 d。這同樣可以針對(duì)每個(gè)位置 i 進(jìn)行指定。例如，(y < 1,000)???? isHospital 可用于指定：你可以在僅經(jīng)過擁擠度低于1,000的地點(diǎn)的前提下，到達(dá)一個(gè)為醫(yī)院的位置（isHospital 為真）。

此外，還可以推導(dǎo)出其他空間算子。一個(gè)例子是“某處”算子 ?≤dφ ≡ TRUE ?≤dφ，它用于表示較寬松的空間要求，即檢查是否存在一個(gè)滿足 φ 的地點(diǎn)，且可通過一條最長距離為 d 的路徑到達(dá)（即，無需限制可達(dá)路徑上左側(cè)屬性 φ 必須始終成立）。例如，?≤???(y < 1,000) 意味著在1公里范圍內(nèi)，必須至少存在一個(gè)擁擠度低于1,000閾值的地點(diǎn)。

一旦屬性被指定為邏輯公式，便有專門針對(duì)所用邏輯類型設(shè)計(jì)的高效算法，可用于近似隨機(jī)系統(tǒng)關(guān)于這些屬性的行為。人們首先關(guān)注的是屬性滿足性 S?(y???:?, φ)，即：隨機(jī)變量 y（我們關(guān)注的量）在時(shí)間段 t 到 t+h 內(nèi)，是否滿足區(qū)域 i 的屬性 φ。請(qǐng)注意，鑒于我們關(guān)注的是 t 之后屬性的監(jiān)控，且假設(shè) t 到 t+1 之間的行為恒定，因此滿足性取決于 y???:? = (y?, y???, ..., y???)。此外，應(yīng)當(dāng)注意的是，區(qū)域 i 中空間屬性的滿足性不僅取決于該區(qū)域內(nèi)感興趣時(shí)間段內(nèi)的擁擠度值，還取決于其他區(qū)域的值。為此，STREL 提供了一個(gè)布爾監(jiān)控算法，該算法在檢查系統(tǒng)某一特定實(shí)現(xiàn)中給定邏輯公式的滿足性時(shí)，會(huì)返回“是/否”的答案。

其次，人們還希望量化某一屬性的可靠性（reliability）。這通過魯棒性函數(shù) R?(y???:?, φ) 來衡量，該函數(shù)被定義為：在不改變屬性真值的前提下，所關(guān)注量可容忍的擾動(dòng)邊界 [13]。直觀而言，對(duì)于原子命題 y?,? > c?,?，其魯棒性值由所關(guān)注量 y?,? 與閾值 c?,? 的差值給出，即：R?(y?, φ) = y?,? - c?,?。形式上，滿足函數(shù) S 與魯棒性函數(shù) R 均基于邏輯算子遞歸定義（參見附錄 B 中對(duì)公式 (1) 所列規(guī)則的函數(shù)定義，或文獻(xiàn) [28] 以獲取更詳盡的闡述）。STREL 的定量監(jiān)控算法會(huì)計(jì)算給定系統(tǒng)實(shí)現(xiàn)下魯棒性函數(shù)的具體數(shù)值。布爾監(jiān)控與定量監(jiān)控之間存在一個(gè)“健全性”（soundness）性質(zhì)：正值對(duì)應(yīng)屬性滿足，負(fù)值則對(duì)應(yīng)屬性違反。我們建議感興趣的讀者參考文獻(xiàn) [28] 獲取關(guān)于該邏輯的完整且形式化的描述，或參考文獻(xiàn) [29] 查閱更多面向?qū)嵺`的案例研究。

本節(jié)余下部分將重點(diǎn)闡述采用 STREL 框架進(jìn)行屬性驗(yàn)證的關(guān)鍵優(yōu)勢(shì)。首要優(yōu)勢(shì)在于，STREL 是一種專門設(shè)計(jì)的規(guī)范語言，旨在與空間和時(shí)間概念的直覺認(rèn)知保持緊密聯(lián)系，從而能夠以簡(jiǎn)潔且易于理解的方式表達(dá)復(fù)雜的約束條件。請(qǐng)注意，STREL 已有配套的專用腳本語言可用，允許用戶幾乎用純英語來表述公式。此外，使用 STREL 算子指定需求的一個(gè)關(guān)鍵優(yōu)勢(shì)是：開源軟件 Moonlight [30] 可直接用于自動(dòng)驗(yàn)證一組給定預(yù)測(cè)是否滿足所提供的規(guī)范。最后，由 Moonlight 實(shí)現(xiàn)的 STREL 規(guī)范自動(dòng)監(jiān)控功能，采用了最先進(jìn)的算法，在內(nèi)存占用和計(jì)算時(shí)間效率方面表現(xiàn)優(yōu)異（通常優(yōu)于其他替代方案）。盡管針對(duì)特定規(guī)范定制的臨時(shí)算法可能更高效，但它們往往難以適應(yīng)隨監(jiān)測(cè)屬性演變而產(chǎn)生的變化。因此，該框架與 Moonlight 軟件所提供的通用性，確保了屬性規(guī)范能夠以最小的修改成本輕松適應(yīng)模型的變化。

2.2 擁擠度要求

2.2.1 要求的非正式描述。在本節(jié)中，我們提出了一些大城市擁擠度水平應(yīng)滿足的非正式屬性，以穩(wěn)健地應(yīng)對(duì)關(guān)鍵事件。設(shè) c 代表城市所有區(qū)域的統(tǒng)一擁擠度閾值。但請(qǐng)注意，該框架也可容納例如區(qū)域特定的閾值值。為簡(jiǎn)化表述，我們?cè)诖藘H限于使用一個(gè)通用的 c 值。該閾值通常由決策者知曉，并對(duì)應(yīng)于某個(gè)位置仍可被視為“不擁擠”的最大值。此外，令 hφ 表示用于某屬性或要求 φ 的未來時(shí)間步長。

我們所提出的框架的一個(gè)潛在利益相關(guān)方是一家電信公司，該公司希望擁有一個(gè)預(yù)測(cè)性預(yù)警系統(tǒng)，以確保其移動(dòng)網(wǎng)絡(luò)不會(huì)過載。以下三項(xiàng)屬性可能對(duì)電信公司具有吸引力：

P.1 過載是暫時(shí)的：如果在 t 時(shí)刻之后的一段時(shí)間內(nèi)，擁擠度水平超過閾值 c，則必須在 t + hP,1 時(shí)刻前回落至 c 以下。

P.2 過載是局部的：如果在某一特定位置，t + hP,2 時(shí)刻的擁擠度水平上升至 c 以上，則該位置與另一同時(shí)擁擠度低于 c 的位置之間的距離不得超過 dP,2。這是城市網(wǎng)格在試圖平衡過度負(fù)載時(shí)的一項(xiàng)最低空間要求。

P.3 網(wǎng)絡(luò)具備容錯(cuò)性：對(duì)于某一位置，在 (t, t + hP,3] 時(shí)間區(qū)間內(nèi)，該位置本身或其距離 dP,3 范圍內(nèi)的其他位置的擁擠度水平均應(yīng)始終低于 c，即必須能夠?qū)崿F(xiàn)緊急負(fù)載均衡。

除了上述與移動(dòng)網(wǎng)絡(luò)總體方面相關(guān)的各項(xiàng)要求外，為了從安全和生活質(zhì)量角度評(píng)估城市表現(xiàn)，考察城市在抵達(dá)某些關(guān)鍵興趣點(diǎn)方面的可達(dá)性也很有意義。例如，在緊急情況下，交通監(jiān)控機(jī)構(gòu)會(huì)關(guān)注以下要求（假設(shè)我們的擁擠度度量確實(shí)是城市人口密度的代理指標(biāo)）：

P.4 不擁擠可達(dá)性：任何城市中心的不擁擠地點(diǎn)，都必須能在 (t, t + hP,4] 時(shí)間區(qū)間內(nèi)，僅通過不擁擠的地點(diǎn)，抵達(dá)距離不超過 dP,4 的醫(yī)院。

2.2.2 要求的形式化。我們將在此展示如何使用第 2.1 節(jié)介紹的 STREL 邏輯來形式化上文所述的要求。前述要求將被逐步形式化為 STREL 公式，關(guān)鍵算子也將隨之逐一說明。在考察要求的形式化之前，我們首先引入原子屬性：

φ = (y > c)

即，擁擠度高于某一閾值 c。反之，公式 ?φ 表示擁擠度水平低于或等于閾值 c 的情形。該公式構(gòu)成了形式化我們各項(xiàng)要求的基本構(gòu)建模塊；事實(shí)上，第一個(gè)要求（關(guān)于臨時(shí)過載）可通過使用時(shí)序算子以如下方式表述：

φP.1 = φ → F≤hP,1?φ. (P.1)

第二個(gè)屬性（關(guān)于過載是局部的）可形式化為一個(gè)時(shí)空屬性：

φP.2 = F=hP,2(φ → ?≤dP,2?φ). (P.2)

請(qǐng)注意，此處的時(shí)序算子 F=hP,2 表示該要求應(yīng)在 hP,2 步之后的未來時(shí)刻成立。

第三，網(wǎng)絡(luò)的容錯(cuò)性是一個(gè)時(shí)空要求，可形式化為：

φP.3 = G≤hP,3(?≤dP,3?φ), (P.3)

其中，G≤hP,3 要求“某處”屬性在整個(gè)區(qū)間 (t, t + hP,3] 內(nèi)全局成立。

最后，對(duì)于與醫(yī)院可達(dá)性相關(guān)的要求，我們首先引入一個(gè)新的原子命題：

φ? = isHospital.

此處，φ? 是一個(gè)特殊命題，代表醫(yī)院位置，其含義是：僅當(dāng)當(dāng)前位置為醫(yī)院時(shí)，該命題才成立。對(duì) P.4 的第一種直接翻譯可能是：

F≤hP,4(?φ?≤dP,4φ?). (2)

雖然公式 (2) 中的要求從字面上形式化了 P.4，但它很可能給出了對(duì)該要求的一種不切實(shí)際的解釋。事實(shí)上，?φ?≤dP,4φ? 的意思是可以通過僅穿越不擁擠區(qū)域到達(dá)醫(yī)院，然而它并未考慮抵達(dá)該地點(diǎn)所需的行進(jìn)時(shí)間，這意味著只要存在一條通往醫(yī)院的不擁擠路徑，該屬性即被視為滿足（盡管實(shí)際行進(jìn)時(shí)間可能顯著更長）。下面提供一個(gè)更現(xiàn)實(shí)（盡管稍顯復(fù)雜）的版本：

屬性 φP.4（在符號(hào)使用上略有濫用）編碼了我們的要求，并展示了邏輯方法的靈活性。公式 (2) 中的“字面”要求表明，人們需要在時(shí)間區(qū)間 (t, t + hP,4] 內(nèi)最多移動(dòng) dP,4 個(gè)單元格，但它并未明確指定一個(gè)人在城市網(wǎng)格的不同單元格之間移動(dòng)的速度有多快。為了對(duì)該規(guī)范給出一個(gè)更現(xiàn)實(shí)的解釋，我們假設(shè)在一個(gè)時(shí)間單位內(nèi)（即，10分鐘），一個(gè)人只能從一個(gè)單元格移動(dòng)到下一個(gè)相鄰單元格。這種解釋轉(zhuǎn)化為 ψ?,?，它強(qiáng)制要求當(dāng)前位置在未來十分鐘內(nèi)不擁擠，并通過遞歸檢查 ψ?,? 迭代地執(zhí)行此操作 n 次，直到達(dá)到最大距離（以網(wǎng)格上的“跳數(shù)”計(jì)），此時(shí)它會(huì)在鄰近區(qū)域內(nèi)尋找醫(yī)院。這樣，分析 φP.4 的滿足性或魯棒性，不僅會(huì)提供有關(guān)醫(yī)院空間可達(dá)性的洞察，還會(huì)同時(shí)考慮抵達(dá)醫(yī)院所需的穿越時(shí)間。我們可以注意到，在這個(gè)例子中，當(dāng)用自然語言描述 φP.4 時(shí)，它會(huì)變得繁瑣且容易產(chǎn)生歧義，而公式 P.4 則展示了邏輯方法的靈活性。

3 使用形式化方法進(jìn)行預(yù)測(cè)模型檢驗(yàn)與模型比較

3.1 通過貝葉斯方法納入不確定性

我們的應(yīng)用旨在研究在固定網(wǎng)格區(qū)域內(nèi)按規(guī)律時(shí)間間隔觀測(cè)到的城市擁擠度行為。再次說明，令 y?,? 表示在時(shí)間點(diǎn) j 時(shí)區(qū)域 i 的擁擠度測(cè)量值，其中 i = 1, ..., I 代表城市網(wǎng)格中的面域單元，j = 1, ..., T 代表時(shí)間點(diǎn)。作為預(yù)測(cè)推斷的框架，我們假設(shè)截至?xí)r間 t < T 的觀測(cè)數(shù)據(jù)被用作訓(xùn)練樣本，而評(píng)估則在剩余的 t+1, ..., T 離散時(shí)間點(diǎn)上的觀測(cè)數(shù)據(jù)上進(jìn)行。通過使用 STREL，我們關(guān)注于探究未來擁擠度的兩個(gè)函數(shù)或統(tǒng)計(jì)量：即屬性滿足性（property satisfaction）和屬性魯棒性（property robustness）。為了將“滿足性”與“魯棒性”的概念擴(kuò)展至整個(gè)隨機(jī)系統(tǒng)，我們引入了兩個(gè)關(guān)鍵概念：(i) 屬性滿足性的貝葉斯預(yù)測(cè)概率；以及 (ii) 貝葉斯預(yù)測(cè)魯棒性的期望值。

正如引言中所述，傳統(tǒng)的 SMC 將模型參數(shù)視為固定值，從模型中生成大量軌跡，然后計(jì)算這些軌跡中有多少次滿足給定屬性。而在貝葉斯框架下，參數(shù)并非固定不變，而是根據(jù)專家知識(shí)或先驗(yàn)觀測(cè)賦予一個(gè)先驗(yàn)分布。在觀測(cè)數(shù)據(jù)后，我們便能獲得模型參數(shù)的后驗(yàn)概率分布。接下來，我們將展示如何運(yùn)用貝葉斯方法，在計(jì)算屬性滿足概率與魯棒性時(shí)，對(duì)參數(shù)的不確定性加以考量。我們首先引入貝葉斯預(yù)測(cè)密度。h 步超前的貝葉斯預(yù)測(cè)密度由下式給出：

其中，y?:?? 表示截至?xí)r間 t 為止隨機(jī)變量 y?:? = (y?, ..., y?) 的觀測(cè)值，每個(gè) y? 均為 I 維向量；κ 包含模型中所有待估計(jì)的參數(shù)與潛變量；p(κ | y?:??) 表示它們的后驗(yàn)分布；Κ 表示相應(yīng)的積分空間。可以看出，公式 (3) 中的預(yù)測(cè)密度是由似然函數(shù)的積分給出的。

該似然函數(shù)中，不可觀測(cè)變量 κ 的取值根據(jù)其后驗(yàn)分布進(jìn)行加權(quán)。這意味著，該預(yù)測(cè)密度整合了關(guān)于不可觀測(cè)變量向量的不確定性，以及在給定歷史數(shù)據(jù) y?:?? 條件下對(duì)未來值 y??? 的內(nèi)在不確定性。在我們所提出的模型中，后驗(yàn)分布 p(κ | y?:??) 可通過使用 MCMC 方法從截至?xí)r間 t 的后驗(yàn)分布中生成 M 個(gè)樣本 κ?:?? 來獲得。然后，可通過從由密度 p(y??? | y?:??, κ?:??) 所代表的每個(gè)分布中模擬 y????（m = 1, ..., M），從而獲得公式 (3) 中的預(yù)測(cè)分布。

基于此預(yù)測(cè)分布，我們現(xiàn)在可以定義屬性 φ 在位置 i、時(shí)間 t 的貝葉斯 h 步超前預(yù)測(cè)滿足概率——它是一個(gè)關(guān)于時(shí)間 t 的觀測(cè)值和未來值 y???:? = (y???, ..., y???) 的函數(shù)：

然而需注意，也可采用該分布的其他匯總統(tǒng)計(jì)量以輔助決策。例如，若需采取更保守的策略，可考慮魯棒性后驗(yàn)分布的更高分位數(shù)（如 90% 分位數(shù)）。

此處我們利用 STREL 的監(jiān)控算法，高效地從 m = 1 , … , M 個(gè)后驗(yàn)預(yù)測(cè)樣本中計(jì)算公式 (5) 與 (7)。需要指出的是，預(yù)測(cè)滿足概率與預(yù)測(cè)魯棒性均可視為經(jīng)典后驗(yàn)預(yù)測(cè)模型檢驗(yàn)（Posterior Predictive Check, PPC；參考文獻(xiàn) [16]）意義上的匯總統(tǒng)計(jì)量。在經(jīng)典 PPC 中，模型與數(shù)據(jù)之間的偏差通過一個(gè)或多個(gè)依賴于數(shù)據(jù)（可能還依賴于模型參數(shù)）的檢驗(yàn)統(tǒng)計(jì)量來度量 [16]。類似地，在本文框架中，這些匯總統(tǒng)計(jì)量依賴于數(shù)據(jù)與屬性設(shè)定，而模型參數(shù)在分析過程中保持固定。其中，滿足性是一個(gè)二元（0/1）統(tǒng)計(jì)量，而魯棒性是連續(xù)型統(tǒng)計(jì)量。可對(duì)這些統(tǒng)計(jì)量應(yīng)用諸如貝葉斯 p 值 [16] 等方法，以服務(wù)于模型評(píng)估目的。

因此，借助 STREL 對(duì)應(yīng)用導(dǎo)向?qū)傩缘谋O(jiān)控，我們得以基于后驗(yàn)預(yù)測(cè)分布，對(duì)所關(guān)注的匯總統(tǒng)計(jì)量開展一種更為形式化、系統(tǒng)化的評(píng)估。

3.2 基于屬性的模型比較

LPDS 僅依據(jù)在實(shí)際發(fā)生結(jié)果處的密度值來評(píng)估預(yù)測(cè)模型。然而，它并非唯一可用于評(píng)估概率預(yù)測(cè)性能的指標(biāo)。根據(jù)當(dāng)前應(yīng)用場(chǎng)景中希望關(guān)注的預(yù)測(cè)特征，可選用其他評(píng)分指標(biāo)。例如，另一個(gè)常用評(píng)分指標(biāo)是連續(xù)排序概率得分（Continuous Ranked Probability Score, CRPS；[25]），它獎(jiǎng)勵(lì)那些將概率質(zhì)量集中在實(shí)際觀測(cè)結(jié)果附近的預(yù)測(cè)分布。更廣義地說，這些評(píng)分指標(biāo)均是基于觀測(cè)數(shù)據(jù)、依據(jù)特定評(píng)分規(guī)則計(jì)算出的樣本估計(jì)值 [18]。有關(guān)基于 MCMC 輸出的評(píng)分規(guī)則估計(jì)方法綜述，可參見文獻(xiàn) [22]。

除上述成熟方法外，我們還提出一種增強(qiáng)型模型評(píng)估與比較框架：通過驗(yàn)證使用 STREL 定制化指定的形式化要求，該框架針對(duì)具體應(yīng)用量身打造，并反映機(jī)器學(xué)習(xí)模型的預(yù)測(cè)如何被用于決策制定。基于特定感興趣量（在我們的框架中即待驗(yàn)證的屬性）對(duì)預(yù)測(cè)模型的評(píng)估，取決于這些量的選擇。因此，應(yīng)利用領(lǐng)域知識(shí)來定義一組多樣化且相關(guān)的量或?qū)傩裕圆蹲筋A(yù)測(cè)質(zhì)量的不同維度。

在下文中，我們提出若干依賴于第 3.1 節(jié)所介紹屬性的后驗(yàn)預(yù)測(cè)滿足性與魯棒性的度量指標(biāo)。具體而言，我們將比較基于 M 條軌跡估算出的后驗(yàn)預(yù)測(cè)滿足性與魯棒性度量，與在時(shí)間 t 之后的觀測(cè)數(shù)據(jù) 上進(jìn)行的事后（ex-post）滿足性與魯棒性評(píng)估結(jié)果。基于后驗(yàn)預(yù)測(cè)分布的樣本，我們對(duì)以下指標(biāo)進(jìn)行計(jì)算，其中對(duì)于每個(gè)時(shí)間點(diǎn) t，我們?cè)谒形恢?i = 1, ..., I 上取平均：

BS（Brier Score）是一種嚴(yán)格的真分規(guī)則 [18]，常用于衡量預(yù)測(cè)概率的準(zhǔn)確性。MSE（均方誤差）衡量的是預(yù)測(cè)魯棒性后驗(yàn)均值的誤差，而 CRPS 則是一種嚴(yán)格的真分規(guī)則，它將預(yù)測(cè)魯棒性中的不確定性納入考量。

此外，我們還可計(jì)算滿足性后驗(yàn)預(yù)測(cè)分布的其他函數(shù)形式，這些函數(shù)在機(jī)器學(xué)習(xí)中被廣泛使用。一個(gè)例子是“滿足性被正確預(yù)測(cè)的位置百分比”（也稱為準(zhǔn)確率）。在此框架下，對(duì)于每一次抽樣 m，我們可以計(jì)算：

此外，除了考察被正確分類的位置所占的百分比外，我們還可計(jì)算滿足性被正確分類位置比例（即 召回率 ，recall）與模型預(yù)測(cè)為滿足屬性的位置中被正確分類比例（即 精確率 ，precision）二者的 調(diào)和平均數(shù) （即 F1 分?jǐn)?shù)）。

利用來自后驗(yàn)分布的 M M 個(gè)抽樣樣本，我們可以考察諸如 可信區(qū)間 （credible intervals）等匯總統(tǒng)計(jì)量，以更深入地理解后驗(yàn)分布的不確定性。

4 實(shí)證說明

4.1 數(shù)據(jù)

為說明所提出的框架，我們采用了一組數(shù)據(jù)集，該數(shù)據(jù)源自2013年11月某一周內(nèi)意大利米蘭市中心的通話詳單記錄（Call Detail Records, CDRs）。鑒于手機(jī)幾乎普及使用，CDR 數(shù)據(jù)是研究人口分布與人群移動(dòng)模式的一個(gè)寶貴代理指標(biāo) [32]，尤其在高頻、大范圍空間網(wǎng)絡(luò)中具有很高的研究潛力。移動(dòng)通信服務(wù)提供商每當(dāng)用戶設(shè)備狀態(tài)因用戶行為（如通話、發(fā)短信、上網(wǎng)）或技術(shù)原因（例如切換到信號(hào)更強(qiáng)的蜂窩基站）發(fā)生改變時(shí)，便會(huì)生成一條 CDR 記錄。

本文所使用的數(shù)據(jù)集是“意大利電信大數(shù)據(jù)挑戰(zhàn)賽”開源數(shù)據(jù)庫的一個(gè)子集，該數(shù)據(jù)庫包含多種地理定位、聚合且匿名化的數(shù)據(jù)集，涵蓋米蘭市及特倫托省（詳細(xì)描述參見文獻(xiàn) [3]）。電信活動(dòng)數(shù)據(jù)覆蓋2013年11月1日至12月16日時(shí)段，CDR 數(shù)據(jù)已在空間和時(shí)間維度上進(jìn)行了聚合。以米蘭為例，城市區(qū)域被劃分為一個(gè)由1,000個(gè)方格組成的網(wǎng)格，每個(gè)方格大小約為 235 米 × 235 米，CDR 數(shù)據(jù)在每個(gè)方格內(nèi)進(jìn)行聚合。此外，時(shí)間維度上按每10分鐘的時(shí)間段進(jìn)行聚合。數(shù)據(jù)庫中還提供了生成 CDR 的活動(dòng)類型信息：

• 短信服務(wù)（SMS）- 接收活動(dòng)：在給定時(shí)間段內(nèi)，某網(wǎng)格方格內(nèi)接收到的短信數(shù)量所對(duì)應(yīng)的比例活動(dòng)量。每當(dāng)用戶接收一條短信時(shí)，即生成一條 CDR。
• 短信服務(wù)（SMS）- 發(fā)送活動(dòng)：在給定時(shí)間段內(nèi)，某網(wǎng)格方格內(nèi)發(fā)送的短信數(shù)量所對(duì)應(yīng)的比例活動(dòng)量。每當(dāng)用戶發(fā)送一條短信時(shí)，即生成一條 CDR。
• 呼入活動(dòng)：在給定時(shí)間段內(nèi)，某網(wǎng)格方格內(nèi)接收到的通話次數(shù)所對(duì)應(yīng)的比例活動(dòng)量。每當(dāng)用戶接聽電話時(shí)，即生成一條 CDR。
• 呼出活動(dòng)：在給定時(shí)間段內(nèi)，某網(wǎng)格方格內(nèi)撥出的通話次數(shù)所對(duì)應(yīng)的比例活動(dòng)量。每當(dāng)用戶撥打電話時(shí)，即生成一條 CDR。
• 互聯(lián)網(wǎng)流量活動(dòng)：在給定時(shí)間段內(nèi)，某網(wǎng)格方格內(nèi)生成的 CDR 數(shù)量。每當(dāng)用戶發(fā)起或結(jié)束一次互聯(lián)網(wǎng)連接時(shí)，即生成一條 CDR；若同一連接持續(xù)超過15分鐘，或用戶傳輸數(shù)據(jù)量超過5MB，也會(huì)額外生成一條 CDR。

數(shù)據(jù)進(jìn)一步通過將每個(gè)類別中真實(shí)記錄數(shù)除以一個(gè)僅意大利電信知曉的常數(shù)進(jìn)行匿名化處理，從而隱藏了實(shí)際的通話、短信和互聯(lián)網(wǎng)連接數(shù)量。

我們選取了米蘭電信活動(dòng)數(shù)據(jù)集中2013年11月4日（周一）至11月11日（周一）期間的一個(gè)子集，共包含 T = 6 × 24 × 8 = 1,152 個(gè)時(shí)間點(diǎn)。我們進(jìn)一步將分析限定于中心區(qū)域的 21 × 21 網(wǎng)格（即 I = 441），其中最中心的單元格位于米蘭大教堂（Milan Duomo）所在地。該網(wǎng)格覆蓋面積約25平方公里。此外，我們將所有手機(jī)活動(dòng)度量值（即短信接收、短信發(fā)送、呼入、呼出和互聯(lián)網(wǎng)）的總和作為擁擠度的衡量指標(biāo)。我們采用這一聚合度量的原因在于：(i) 通話（呼入、呼出）與短信活動(dòng)在夜間較為稀疏（因?yàn)槿藗兒苌僭谖缫购蟠螂娫捇虬l(fā)短信）；(ii) 現(xiàn)代手機(jī)使用更依賴于上網(wǎng)或消息應(yīng)用（約2010年后流行起來）。因此，將互聯(lián)網(wǎng) CDR 與其他四項(xiàng)活動(dòng)一同考慮，能更真實(shí)地反映特定區(qū)域的擁擠程度。

圖1展示了整個(gè)分析期內(nèi)，在 21 × 21 網(wǎng)格上各10分鐘時(shí)間段平均后的擁擠度測(cè)量值。在圍繞米蘭大教堂（③）的中心網(wǎng)格方格以及上城區(qū)（兩個(gè)主要車站所在地：① 加里波第站 Garibaldi Station 和 ② 中央車站 Central Station）可明顯觀察到高擁擠度區(qū)域。另一方面，較低活動(dòng)水平的網(wǎng)格方格也清晰可見，例如地圖右側(cè)及右下角疊加在繁忙大道上的那些區(qū)域。

為了說明擁擠度度量的時(shí)間行為特征，我們?cè)趫D2中展示了包含三個(gè)代表性區(qū)域——③ 大教堂區(qū)、⑤ 納維利區(qū) Navigli 和 ④ 博科尼區(qū) Bocconi——的網(wǎng)格單元時(shí)間序列。我們觀察到，③ 大教堂區(qū)的活動(dòng)水平高于其他兩個(gè)區(qū)域，其高峰出現(xiàn)在工作日的中午和周末的下午早些時(shí)候。而⑤ 納維利區(qū)則以其多樣化的咖啡館、餐廳、酒吧和設(shè)計(jì)商店聞名，其活動(dòng)在工作日與周末均表現(xiàn)得更為均勻，高峰集中在傍晚時(shí)段。包含④ 博科尼大學(xué)的網(wǎng)格方格在工作日表現(xiàn)出清晰的活動(dòng)模式，而在周末（尤其是周日）活動(dòng)水平顯著降低。

數(shù)據(jù)中的季節(jié)性特征也可在圖3中識(shí)別，該圖通過柵格圖可視化了整個(gè)數(shù)據(jù)集。除了所有地點(diǎn)都存在的強(qiáng)烈日周期性外，不同區(qū)域之間還可觀察到不同的時(shí)間模式。大多數(shù)區(qū)域在周末呈現(xiàn)出相對(duì)較低的活動(dòng)水平，但工作日的活動(dòng)模式在不同區(qū)域組間存在差異。例如，網(wǎng)格中心部分（單元格ID 150–280）的工作日與周末擁擠度差異較大，而單元格ID 約為400的區(qū)域（地圖頂部單元格）在工作日和周末則表現(xiàn)出較為相似的活動(dòng)水平。

4.2 模型比較

我們?cè)诜治鲋胁捎昧硕鄠€(gè)貝葉斯模型，用于描述在固定網(wǎng)格區(qū)域內(nèi)按規(guī)律時(shí)間間隔觀測(cè)到的城市擁擠度。令 y?,? 表示在時(shí)間點(diǎn) j 時(shí)區(qū)域 i 的擁擠度測(cè)量值，其中 i = 1, ..., I 代表各區(qū)域，j = 1, ..., T 代表各時(shí)間點(diǎn)。從描述性圖表中可見，該測(cè)量值在日和周尺度上均表現(xiàn)出季節(jié)性行為，且這種行為在不同區(qū)域之間存在異質(zhì)性。與文獻(xiàn) [9] 類似，我們?cè)谀Ｐ蜆?gòu)建中通過采用以下動(dòng)態(tài)諧波回歸（dynamic harmonic regression）來刻畫這些特征：

其中，項(xiàng) ω? = k/T 是傅里葉頻率，其對(duì)應(yīng)的正弦波在觀測(cè)時(shí)間序列長度內(nèi)完成整數(shù)個(gè)周期，且 K 不能大于 T/2。為選擇諧波回歸的維度，我們檢查了 I = 21 × 21 = 441 條時(shí)間序列的估計(jì)譜密度（見圖4），并觀察到強(qiáng)烈的日內(nèi)和周內(nèi)季節(jié)性，其最大值對(duì)應(yīng)于24小時(shí)區(qū)間。我們利用該信息，在構(gòu)建諧波回歸時(shí)選取圖4中由垂直線標(biāo)記的12個(gè)頻率。這意味著我們的協(xié)變量向量 h? 的維度為24。

此外，為了捕捉擁擠度中的時(shí)空依賴性，誤差項(xiàng) η?,? 被分解為兩個(gè)組成部分：

η?,? = w?,? + e?,?,

其中，e?,? 獨(dú)立同分布地服從 N(0, σ2) 正態(tài)分布，而 w?,? 是一個(gè)時(shí)空隨機(jī)效應(yīng)，用于捕捉傅里葉協(xié)變量未能解釋的對(duì)數(shù)擁擠度測(cè)量值中的時(shí)空依賴性。

在下文中，我們將調(diào)查并比較不同模型在隨機(jī)效應(yīng)方面的預(yù)測(cè)性能。作為基線模型，我們考慮一個(gè)無隨機(jī)效應(yīng)（即 w?,? = 0）且所有區(qū)域共享同一組回歸系數(shù)的模型。我們所采用的最復(fù)雜模型是文獻(xiàn) [9] 中提出的一種模型，其中 w?,? 具有時(shí)空規(guī)范，且區(qū)域特定系數(shù) β? 通過貝葉斯非參數(shù)（Bayesian Non-Parametric, BNP）方法進(jìn)行聚類。這使我們能夠識(shí)別具有相似時(shí)間行為的區(qū)域集群，同時(shí)保持模型的簡(jiǎn)潔性。模型中通過假設(shè)空間上的條件自回歸（Conditional Autoregressive, CAR）先驗(yàn)和時(shí)間動(dòng)態(tài)上的自回歸（Autoregressive, AR）過程來引入時(shí)空依賴性。我們將這種依賴結(jié)構(gòu)稱為 CAR-AR。當(dāng)再引入一層系數(shù)聚類時(shí)，我們將該模型記為 CAR-AR-BNP。

除了 CAR-AR-BNP 模型外，我們還考慮了三個(gè) CAR-AR 模型，它們均假設(shè)所有區(qū)域共享同一組回歸系數(shù)向量，并采用正態(tài)先驗(yàn)：(i) 一個(gè)空間自相關(guān)參數(shù) ρ 固定為 0 的模型（CAR-AR (ρ = 0)）——這意味著僅存在時(shí)間依賴結(jié)構(gòu)；(ii) 一個(gè)空間自相關(guān)參數(shù) ρ 固定為 0.5 的模型（CAR-AR (ρ = 0.5)）——這意味著存在適度空間依賴的時(shí)間依賴結(jié)構(gòu)；(iii) 一個(gè)空間自相關(guān)參數(shù) ρ 在 MCMC 過程中被估計(jì)的模型（CAR-AR）。關(guān)于這些模型及其使用 MCMC 的估計(jì)過程的更多細(xì)節(jié)，可參見附錄 A。

為評(píng)估不同模型的性能，我們基于滾動(dòng)窗口設(shè)置了一個(gè)樣本外實(shí)驗(yàn)：首先在2013年11月4日00:00（周一）至11月10日23:50（周日）的數(shù)據(jù)上訓(xùn)練貝葉斯模型。隨后，我們生成一步、兩步和三步超前預(yù)測(cè)，并計(jì)算用于11月11日00:00 至 00:20 的模型選擇預(yù)測(cè)指標(biāo)。在另一個(gè)獨(dú)立的估計(jì)過程中，我們將訓(xùn)練數(shù)據(jù)窗口每次向前移動(dòng)10分鐘，并迭代重新估計(jì)模型，直至達(dá)到樣本末尾。

所有結(jié)果均基于 Gibbs 采樣器的10,000次迭代，其中前5,000次作為預(yù)熱期（burn-in）被舍棄。應(yīng)用了50的稀釋參數(shù)（thinning parameter），最終獲得100個(gè)可用于推斷的樣本。盡管該樣本數(shù)量小于貝葉斯推斷通常所用的數(shù)量，但這是為了使屬性驗(yàn)證（特別是屬性 P.4）在本地機(jī)器上更具計(jì)算可行性而特意選擇的——因?yàn)榭臻g算子的計(jì)算復(fù)雜度與位置數(shù)量呈二次方增長，而其他算子的復(fù)雜度僅隨位置數(shù)量線性增長。1 如果可訪問工作站集群，則可通過并行化屬性驗(yàn)證過程來增加迭代次數(shù)。各模型的跡線圖顯示所有參數(shù)均表現(xiàn)出可接受的收斂性及良好的混合效果。

圖5展示了2013年11月11日（周一）的累積一步超前（h = 1）和三步超前（h = 3）對(duì)數(shù)預(yù)測(cè)貝葉斯因子：

其中 B 被設(shè)定為一個(gè)基線模型。我們觀察到，所有將空間和/或時(shí)間相關(guān)性納入考量的模型均優(yōu)于基線模型，而 CAR-AR-BNP 模型表現(xiàn)最佳——盡管其優(yōu)勢(shì)并不十分顯著，但仍優(yōu)于純 CAR-AR 模型。在三步超前預(yù)測(cè)方面，CAR-AR-BNP 模型表現(xiàn)更優(yōu)；但我們同時(shí)也觀察到，在午夜之后以及 07:00 至 09:00 時(shí)段，所有 CAR-AR 模型的表現(xiàn)反而劣于基線模型（參見累積對(duì)數(shù)貝葉斯因子曲線中的負(fù)斜率）。此外，在約 19:00 時(shí)，CAR-AR 模型的性能增益有所減弱，此時(shí)曲線斜率不再陡峭。這些結(jié)果暗示：空間依賴參數(shù) ρ 可能在一天中不同時(shí)段發(fā)生變化。我們將這一模型擴(kuò)展留待未來研究。

最后，我們還基于第 3.2 節(jié)所介紹的屬性滿足性與魯棒性預(yù)測(cè)指標(biāo)，考察了五個(gè)模型的性能。所有屬性所使用的參數(shù)為：c = 500，hP,1 = hP,3 = 30 分鐘，hP,2 = 10 分鐘，hP,4 = 40 分鐘，dP,2 = dP,3 = 1 個(gè)單元格，dP,4 = 4 個(gè)單元格。圖6 展示了四個(gè)屬性在每個(gè)測(cè)試時(shí)段內(nèi)、所有位置平均后的魯棒性根均方誤差（MSE）、CRPS 以及滿足性 Brier 得分（BS）。該圖可用于判斷在所驗(yàn)證屬性的具體興趣維度上，哪個(gè)模型表現(xiàn)最佳。

例如，可以看出，AR 模型在所有屬性的滿足性指標(biāo)上表現(xiàn)相似；而在屬性 P.2 和 P.3 的魯棒性方面，CAR-AR-BNP 模型表現(xiàn)更優(yōu)。在同一時(shí)間段（07:00–09:00 高峰期），該模型在屬性 P.4 上的表現(xiàn)也優(yōu)于其他模型，因此若建模者關(guān)注此特定時(shí)間段內(nèi)的性能，則應(yīng)選擇該模型。另一方面，需注意的是，所有模型在正午時(shí)段關(guān)于屬性 P.4 的準(zhǔn)確率與 F1 分?jǐn)?shù)均伴隨較大不確定性，因此可預(yù)期在此時(shí)間段內(nèi)的預(yù)測(cè)可靠性較低。表1 展示了四個(gè)屬性在時(shí)間和空間上平均后的滿足性 BS、魯棒性 MSE 與 CRPS。我們觀察到，CAR-AR-BNP 模型在所檢驗(yàn)的各項(xiàng)指標(biāo)中表現(xiàn)最優(yōu)，但部分屬性上的性能差異并不顯著。

在圖7 中，我們針對(duì)屬性 P.4，展示了 CAR-AR-BNP 模型與基線模型在一天中三個(gè)不同時(shí)段（午夜、08:00、12:00）下，各位置的魯棒性 CRPS 與滿足性 BS。此類可視化有助于我們?cè)u(píng)估模型在空間網(wǎng)格上的表現(xiàn)。我們觀察到，相較于基線模型，CAR-AR-BNP 模型在魯棒性方面表現(xiàn)相當(dāng)令人滿意。但在滿足性方面，即使使用 CAR-AR-BNP 模型，在午夜及 08:00 時(shí)，市中心仍存在一些區(qū)域的滿足性未能被充分預(yù)測(cè)。

4.3 帶空間聚類的時(shí)空模型結(jié)果

以下我們呈現(xiàn) CAR-AR-BNP 模型的結(jié)果。圖8 的上方面板展示了通過應(yīng)用 Binder 損失函數(shù)對(duì)聚類分配向量樣本進(jìn)行分析后識(shí)別出的三個(gè)聚類，而下方面板則展示了每個(gè)聚類內(nèi)所有位置平均后的擁擠度測(cè)量值。

• 藍(lán)色聚類：其特點(diǎn)是周末與工作日之間的擁擠度差異較小，活動(dòng)高峰出現(xiàn)在早晨（工作日更顯著）以及傍晚（周日效應(yīng)更強(qiáng)）。⑤ Navigli 區(qū)域?qū)儆谠撍{(lán)色聚類。
• 黃色聚類：包含工作日活動(dòng)水平高、周末活動(dòng)水平低的區(qū)域，且日內(nèi)活動(dòng)峰值約在中午。該聚類的典型區(qū)域?yàn)榇髮W(xué)中心或市中心，大多數(shù)辦公樓位于此處。
• 綠色聚類：是規(guī)模最小的一個(gè)聚類，其特征是周末活動(dòng)急劇下降。該聚類對(duì)應(yīng)的區(qū)域是 Porta Romana，此處擁有同名火車站，主要服務(wù)于通勤者進(jìn)入市區(qū)。此外，某些相對(duì)孤立、被其他聚類區(qū)域包圍但仍歸屬于某單一聚類的區(qū)域，其成因似乎是可解釋的，并非由模型偽影導(dǎo)致。例如，綠色聚類中部的黃色方格即為一座大型購物中心所在地。

最后，用于衡量時(shí)間和空間依賴性的參數(shù)的后驗(yàn)均值表明，在空間和時(shí)間維度上均存在強(qiáng)烈的持續(xù)性。

4.4 帶空間聚類的時(shí)空模型之擁擠度要求驗(yàn)證

4.4.1 P.1 —— 過載是暫時(shí)的圖9 展示了基于屬性 P.1 評(píng)估所得的估計(jì)后驗(yàn)滿足概率及魯棒性度量的后驗(yàn)均值。需注意，P.1 僅通過時(shí)序算子定義屬性，其中我們?cè)O(shè)定 hP,1 = 30 分鐘。也就是說，我們檢驗(yàn)擁擠度變量是否始終低于 c = 500；若其超過此值，則必須在30分鐘內(nèi)回落至該值以下。從結(jié)果來看，城市大致可分為兩個(gè)宏觀區(qū)域：歷史與金融中心在繁忙時(shí)段不太可能滿足該屬性，而住宅區(qū)則幾乎總是滿足該屬性。一個(gè)相關(guān)的例外來自⑤ Navigli 區(qū)域（地圖左下角）：事實(shí)上，這是一個(gè)充滿活力的區(qū)域，許多年輕人居住于此，擁有眾多旅游地標(biāo)和活躍的商業(yè)區(qū)。我們可以看到，該區(qū)域長期持續(xù)違反我們的要求，但觀察其魯棒性值可知，其實(shí)際值接近于零，意味著這種違規(guī)程度很小，從網(wǎng)絡(luò)容量角度來看并不嚴(yán)重。

4.4.2 P.2 —— 過載是局部的圖10 展示了基于屬性 P.2 在一天中三個(gè)不同時(shí)段評(píng)估所得的估計(jì)后驗(yàn)滿足概率及魯棒性度量的后驗(yàn)均值。請(qǐng)注意，該屬性僅基于對(duì)未來時(shí)間 t + hP,2（hP,2 = 10 分鐘）鄰近位置（dP,2 = 1 個(gè)單元格）的預(yù)測(cè)。正如直觀預(yù)期，該屬性在城市中心的大部分區(qū)域表現(xiàn)出較高的滿足率與魯棒性（通常至少有一個(gè)未擁擠區(qū)域與擁擠區(qū)域相連）。一個(gè)顯著的例外是③ Duomo 區(qū)域——在一天中最繁忙時(shí)段（18:20），人群會(huì)從該區(qū)域擴(kuò)散至其他熱點(diǎn)區(qū)域。然而，通過觀察不同時(shí)間點(diǎn)的魯棒性后驗(yàn)預(yù)測(cè)均值，我們能更清晰地理解過度擁擠的空間分布。事實(shí)上，很明顯③ Duomo 是最有可能遭受過度擁擠的區(qū)域，且無法根據(jù)鄰近區(qū)域狀態(tài)實(shí)施負(fù)載均衡策略。相反，其他區(qū)域（如⑤ Navigli 區(qū)域）則表現(xiàn)出更安全的空間行為，原因或是它們僅輕微超過閾值，或是被擁擠度更低的區(qū)域所環(huán)繞。

4.4.3 P.3 —— 網(wǎng)絡(luò)具備容錯(cuò)性圖11 展示了基于屬性 P.3 在一天中三個(gè)不同時(shí)段評(píng)估所得的估計(jì)后驗(yàn)滿足概率及魯棒性度量的后驗(yàn)均值。屬性 P.3 要求在 hP,3 = 30 分鐘內(nèi)，始終存在一個(gè)距離 dP,3 = 1 的鄰近未擁擠區(qū)域。讀者首先可能注意到的是，該屬性呈現(xiàn)出與 P.1–P.2 類似的視覺模式，但總體而言其滿足可能性較低。這種行為是可預(yù)期的，因?yàn)閺倪壿嫻奖旧砑纯煽闯觯?/p>

P.3 實(shí)際上與 P.1–P.2 中蘊(yùn)含關(guān)系（“→”）右側(cè)的結(jié)構(gòu)相似，但其要求更為嚴(yán)格（必須在接下來的半小時(shí)內(nèi)存在一個(gè)未擁擠區(qū)域）。這一觀察揭示了邏輯方法在驗(yàn)證與規(guī)范可解釋性方面的一個(gè)關(guān)鍵優(yōu)勢(shì)：從非正式角度看，P.1 和 P.2 描述的是不同于 P.3 的不同方面；然而，所得結(jié)果表明，P.3 能夠有效取代 P.1–P.2，作為一個(gè)同時(shí)涵蓋兩者的綜合規(guī)范。事實(shí)上，P.3 總結(jié)了一個(gè)容錯(cuò)系統(tǒng)的理想行為。驗(yàn)證該屬性清晰地表明，城市被劃分為兩個(gè)部分：旅游最集中的區(qū)域較難滿足該屬性，而住宅區(qū)和非旅游區(qū)則更有可能滿足。

4.4.4 P.4 —— 不擁擠可達(dá)性圖12 展示了在 hP,4 = 40 分鐘、dP,4 = 4 個(gè)單元格（約1公里）條件下驗(yàn)證屬性 P.4 的結(jié)果。（H）圓圈標(biāo)記醫(yī)院位置，其中該屬性在所有情況下均被平凡滿足。從圖中可立即觀察到，角落區(qū)域距離市中心任何一家醫(yī)院都太遠(yuǎn)，意味著從這些地方前往市中心是不切實(shí)際的。然而，有趣的是，盡管在繁忙時(shí)段（如18:20）抵達(dá)醫(yī)院從來都不容易，但② Central Station 仍處于一個(gè)較優(yōu)的位置（因其距離不遠(yuǎn)且不太擁擠），相反，① Garibaldi Station 則處于一個(gè)不利位置，因?yàn)樵趽頂D時(shí)段它幾乎無法到達(dá)。更糟糕的是③ Duomo 區(qū)域——盡管其地理位置靠近醫(yī)院，但在擁擠時(shí)段卻經(jīng)歷極高的人群密度，使得按我們所定義的要求抵達(dá)醫(yī)院幾乎不可能；而在中等擁擠時(shí)段則相對(duì)容易。最后，網(wǎng)格角落及底部中心那些始終失敗的區(qū)域告訴我們另一件事：對(duì)于我們所考慮的空間配置，它們總是違反“在 dP,4 范圍內(nèi)抵達(dá)市中心醫(yī)院”的要求。

這初看可能令人驚訝，但查看城市的更大范圍地圖便可澄清：這些區(qū)域?qū)嶋H上更靠近位于我們網(wǎng)格之外的醫(yī)院，因此無法被我們的模型完全分析。

5 討論

本文提出了一種用于預(yù)測(cè)模型檢驗(yàn)與比較的框架。除常見方法外，我們特別倡導(dǎo)：應(yīng)明確指定模型預(yù)測(cè)結(jié)果所需滿足的具體（時(shí)空）屬性。在獲得貝葉斯預(yù)測(cè)分布所生成的軌跡樣本后，可借助形式化驗(yàn)證方法中的高效技術(shù)，對(duì)每條軌跡逐一驗(yàn)證這些屬性，從而近似得到屬性滿足的后驗(yàn)預(yù)測(cè)概率及其后驗(yàn)預(yù)測(cè)魯棒性。最終，還可通過將這些度量結(jié)果與觀測(cè)數(shù)據(jù)中的實(shí)際取值進(jìn)行事后（ex post）比較，實(shí)現(xiàn)對(duì)模型的綜合評(píng)估。

我們通過以下實(shí)例對(duì)該方法進(jìn)行了闡釋：首先，基于米蘭市聚合手機(jī)數(shù)據(jù)構(gòu)建了若干貝葉斯時(shí)空模型，用以刻畫區(qū)域?qū)用娴膿頂D度；其次，為城市網(wǎng)絡(luò)中的擁擠度水平設(shè)定了若干屬性，以確保其在面臨關(guān)鍵事件時(shí)仍具備穩(wěn)健性。我們對(duì)多種模型設(shè)定進(jìn)行了比較，包括：含與不含隨機(jī)效應(yīng)的諧波回歸模型，以及一種對(duì)區(qū)域特定諧波回歸系數(shù)進(jìn)行聚類的模型。結(jié)果表明，后者（即聚類模型）在所提出的各項(xiàng)評(píng)估指標(biāo)下表現(xiàn)最優(yōu)。盡管如此，該模型仍可進(jìn)一步優(yōu)化——例如引入時(shí)間維度上的動(dòng)態(tài)聚類，或允許自回歸（AR）隨機(jī)效應(yīng)的持續(xù)性參數(shù)隨時(shí)間演化。

本文所提框架的核心主張?jiān)谟冢簯?yīng)充分利用貝葉斯預(yù)測(cè)推斷所提供的豐富信息，即通過后驗(yàn)預(yù)測(cè)分布的樣本抽取，依據(jù)那些可直接轉(zhuǎn)化為決策依據(jù)的屬性，對(duì)模型進(jìn)行評(píng)估。為此，我們展示了不同模型設(shè)定在傳統(tǒng)性能指標(biāo)與形式化驗(yàn)證中所用的后驗(yàn)預(yù)測(cè)度量?jī)煞矫娴谋憩F(xiàn)差異，突顯了該框架在連接建模與決策之間的橋梁作用。

在更大尺度上，通過充分利用貝葉斯建模與形式化驗(yàn)證方法之間的協(xié)同效應(yīng)，我們還倡導(dǎo)開發(fā)并應(yīng)用可解釋算法——即將與決策相關(guān)的屬性直接嵌入數(shù)據(jù)分析流程之中。因此，本文所提出的框架在可持續(xù)城市發(fā)展與城市交通領(lǐng)域具有顯著應(yīng)用潛力：這些應(yīng)用場(chǎng)景涉及高度復(fù)雜的系統(tǒng)與多元利益相關(guān)方，且通常對(duì)決策過程的透明性有著迫切需求。我們期望本文的案例闡釋能為未來更廣泛的實(shí)踐應(yīng)用鋪平道路。

原文：https://dl.acm.org/doi/epdf/10.1145/3708479