人工智能試圖模仿人類智能的計(jì)算系統(tǒng)，包括人類一些與智能具有直觀聯(lián)系的功能，例如學(xué)習(xí)、解決問題以及理性地思考和行動(dòng)。在廣義地解釋上，AI 一詞涵蓋了許多密切相關(guān)的領(lǐng)域如機(jī)器學(xué)習(xí)。那些大量使用 AI 的系統(tǒng)在醫(yī)療保健、交通運(yùn)輸、金融、社交網(wǎng)絡(luò)、電子商務(wù)和教育等領(lǐng)域都產(chǎn)生了重大的社會(huì)影響。

這種日益增長(zhǎng)的社會(huì)影響，也帶來了一系列風(fēng)險(xiǎn)和擔(dān)憂，包括人工智能軟件中的錯(cuò)誤、網(wǎng)絡(luò)攻擊和人工智能系統(tǒng)安全等方面。因此，AI 系統(tǒng)的驗(yàn)證問題以及更廣泛的可信 AI 的話題已經(jīng)開始引起研究界的關(guān)注?！翱沈?yàn)證 AI”已經(jīng)被確立為設(shè)計(jì) AI 系統(tǒng)的目標(biāo)，一個(gè)可驗(yàn)證的 AI 系統(tǒng)在特定的數(shù)學(xué)要求上具有強(qiáng)大的、理想情況下可證明的正確性保證。我們?cè)鯓硬拍軐?shí)現(xiàn)這個(gè)目標(biāo)？

最近，《ACM 通訊》（The Communications of ACM）上的一篇綜述文章，試圖從形式驗(yàn)證的角度來思考可證驗(yàn) AI 面臨的挑戰(zhàn)，并給出了一些原則性的解決方案。文章作者是加州伯克利分校電氣工程與計(jì)算機(jī)科學(xué)系的主任 S. Shankar Sastry 和 Sanjit A. Seshia 教授，以及斯坦福大學(xué)計(jì)算機(jī)科學(xué)系助理教授 Dorsa Sadigh。

在計(jì)算機(jī)科學(xué)和工程領(lǐng)域，形式方法涉及系統(tǒng)的嚴(yán)格的數(shù)學(xué)規(guī)范、設(shè)計(jì)和驗(yàn)證。其核心在于，形式方法是關(guān)于證明的：制定形成證明義務(wù)的規(guī)范，設(shè)計(jì)系統(tǒng)以履行這些義務(wù)，并通過算法證明搜索來驗(yàn)證系統(tǒng)確實(shí)符合其規(guī)范。從規(guī)范驅(qū)動(dòng)的測(cè)試和仿真到模型檢查和定理證明，一系列的形式化方法常被用于集成電路的計(jì)算機(jī)輔助設(shè)計(jì)，并已廣泛被用于發(fā)現(xiàn)軟件中的錯(cuò)誤，分析網(wǎng)絡(luò)物理系統(tǒng)，并發(fā)現(xiàn)安全漏洞。

本文回顧了形式化方法傳統(tǒng)的應(yīng)用方式，指明了形式化方法在 AI 系統(tǒng)中的五個(gè)獨(dú)特挑戰(zhàn)，包括：

• 開發(fā)關(guān)于環(huán)境的語(yǔ)言、算法
• 對(duì)復(fù)雜 ML 組件和系統(tǒng)進(jìn)行抽象和表示
• 為 AI 系統(tǒng)和數(shù)據(jù)提出新的規(guī)范形式化方法和屬性
• 開發(fā)針對(duì)自動(dòng)推理的可擴(kuò)展計(jì)算引擎
• 開發(fā)針對(duì)建構(gòu)中可信（trustworthy-by-construction）設(shè)計(jì)的算法和技術(shù)

在討論最新進(jìn)展的基礎(chǔ)上，作者提出了解決以上挑戰(zhàn)的原則。本文不僅僅關(guān)注特定類型的 AI 組件如深度神經(jīng)網(wǎng)絡(luò)，或特定的方法如強(qiáng)化學(xué)習(xí)，而是試圖涵蓋更廣泛的 AI 系統(tǒng)及其設(shè)計(jì)過程。此外，形式化方法只是通往可信 AI 的其中一種途徑，所以本文的觀點(diǎn)旨在對(duì)來自其他領(lǐng)域的方法加以補(bǔ)充。這些觀點(diǎn)很大程度上來源于對(duì)自主和半自主系統(tǒng)中使用 AI 所產(chǎn)生的問題的思考，在這些系統(tǒng)中，安全性和驗(yàn)證性問題更加突出。

概述

圖 1 顯示了形式驗(yàn)證、形式綜合和形式指導(dǎo)的運(yùn)行時(shí)彈性的典型過程。形式驗(yàn)證過程從三個(gè)輸入開始：

圖 1 ：用于驗(yàn)證、綜合和運(yùn)行時(shí)彈性的形式化方法

1. 要驗(yàn)證的系統(tǒng)模型 S
2. 環(huán)境模型 E
3. 待驗(yàn)證的屬性 Φ

驗(yàn)證者生成“是”或“否”的答案作為輸出，來表明 S 是否滿足環(huán)境 E 中的屬性 Φ。通常，“否”輸出伴隨著反例，也稱為錯(cuò)誤跟蹤（error trace），它是對(duì)系統(tǒng)的執(zhí)行，表明 Φ 是如何被偽造的。一些驗(yàn)證工具還包括帶有“是”答案的正確性證明或證書。我們對(duì)形式方法采取一種廣泛的視角，包括使用形式規(guī)范、驗(yàn)證或綜合的某些方面的任何技術(shù)。例如，我們囊括了基于仿真的硬件驗(yàn)證方法或基于模型的軟件測(cè)試方法，因?yàn)樗鼈円彩褂谜降囊?guī)范或模型來指導(dǎo)仿真或測(cè)試的過程。

要將形式驗(yàn)證應(yīng)用于 AI 系統(tǒng)，必須能夠以形式來表示至少 S、E 和 Φ 這三個(gè)輸入，理想情況下，會(huì)存在有效的決策程序來回答先前所描述的“是/否”問題。然而，即使要對(duì)三個(gè)輸入構(gòu)建良好的表示，也并不是一件簡(jiǎn)單的事，更不用說處理底層設(shè)計(jì)和驗(yàn)證問題的復(fù)雜性了。

我們這里通過半自動(dòng)駕駛領(lǐng)域的示例來說明本文的觀點(diǎn)。圖 2 顯示了一個(gè) AI 系統(tǒng)的說明性示例：一個(gè)閉環(huán) CPS，包括一輛帶有機(jī)器學(xué)習(xí)組件的半自動(dòng)車輛及其環(huán)境。具體來說，假設(shè)半自動(dòng)的“自我”（ego）車輛有一個(gè)自動(dòng)緊急制動(dòng)系統(tǒng) (AEBS)，該系統(tǒng)試圖對(duì)前方的物體進(jìn)行檢測(cè)和分類，并在需要避免碰撞時(shí)啟動(dòng)制動(dòng)器。圖 2 中，一個(gè) AEBS 包括一個(gè)由控制器（自動(dòng)制動(dòng)）、一個(gè)受控對(duì)象（受控的車輛子系統(tǒng)，包括自主堆棧的其他部分）和一個(gè)傳感器（攝像頭），以及一個(gè)使用 DNN 的感知組件。AEBS 與車輛環(huán)境相結(jié)合，形成一個(gè)閉環(huán) CPS。“自我”車輛的環(huán)境包括車輛外部（其他車輛、行人等）以及車輛內(nèi)部（例如駕駛員）的代理和對(duì)象。這種閉環(huán)系統(tǒng)的安全要求可以非形式地刻畫為以一種屬性，即在移動(dòng)的“自我”車輛與道路上的任何其他代理或物體之間保持安全距離。然而，這種系統(tǒng)在規(guī)范、建模和驗(yàn)證方面存在許多細(xì)微差別。

圖 2：包含機(jī)器學(xué)習(xí)組件的閉環(huán) CPS 示例

第一，考慮對(duì)半自動(dòng)車輛的環(huán)境進(jìn)行建模。即使是環(huán)境中有多少和哪些代理（包括人類和非人類）這樣的問題，也可能存在相當(dāng)大的不確定性，更不用說它們的屬性和行為了。第二，使用 AI 或 ML 的感知任務(wù)即使不是不可能，也很難形式化地加以規(guī)定。第三，諸如 DNN 之類的組件可能是在復(fù)雜、高維輸入空間上運(yùn)行的復(fù)雜、高維對(duì)象。因此，在生成形式驗(yàn)證過程的三個(gè)輸入 S、E、Φ 時(shí)，即便采用一種能夠使驗(yàn)證易于處理的形式，也十分具有挑戰(zhàn)性。

如果有人解決了這個(gè)問題，那就會(huì)面臨一項(xiàng)艱巨的任務(wù)，即驗(yàn)證一個(gè)如圖 2 那樣復(fù)雜的基于 AI 的 CPS。在這樣的 CPS 中，組合（模塊化）方法對(duì)于可擴(kuò)展性來說至關(guān)重要，但它會(huì)由于組合規(guī)范的難度之類的因素而難以實(shí)施。最后，建構(gòu)中修正的方法（correct-by-construction,CBC）有望實(shí)現(xiàn)可驗(yàn)證 AI，但它還處于起步階段，非常依賴于規(guī)范和驗(yàn)證方面的進(jìn)步。圖 3 總結(jié)了可驗(yàn)證 AI 的五個(gè)挑戰(zhàn)性領(lǐng)域。對(duì)于每個(gè)領(lǐng)域，我們將目前有前景的方法提煉成克服挑戰(zhàn)的三個(gè)原則，用節(jié)點(diǎn)表示。節(jié)點(diǎn)之間的邊緣顯示了可驗(yàn)證 AI 的哪些原則相互依賴，共同的依賴線程由單一顏色表示。下文將詳細(xì)闡述這些挑戰(zhàn)和相應(yīng)的原則。

圖 3：可驗(yàn)證 AI 的 5 個(gè)挑戰(zhàn)領(lǐng)域總結(jié)

環(huán)境建模

基于 AI/ML 的系統(tǒng)所運(yùn)行的環(huán)境通常很復(fù)雜， 比如對(duì)自動(dòng)駕駛汽車運(yùn)行的各種城市交通環(huán)境的建模。事實(shí)上，AI/ML 經(jīng)常被引入這些系統(tǒng)中以應(yīng)對(duì)環(huán)境的復(fù)雜性和不確定性。當(dāng)前的 ML 設(shè)計(jì)流程通常使用數(shù)據(jù)來隱性地規(guī)定環(huán)境。許多 AI 系統(tǒng)的目標(biāo)是在其運(yùn)行過程中發(fā)現(xiàn)并理解其環(huán)境，這與為先驗(yàn)指定的環(huán)境設(shè)計(jì)的傳統(tǒng)系統(tǒng)不同。然而，所有形式驗(yàn)證和綜合都與一個(gè)環(huán)境模型有關(guān)。因此，必須將有關(guān)輸入數(shù)據(jù)的假設(shè)和屬性解釋到環(huán)境模型中。我們將這種二分法提煉為 AI 系統(tǒng)環(huán)境建模的三個(gè)挑戰(zhàn)，并制定相應(yīng)的原則來解決這些挑戰(zhàn)。

2.1 建模不確定性?

在形式驗(yàn)證的傳統(tǒng)用法中，一種司空見慣的做法是將環(huán)境建模為受約束的非確定性過程，或者“干擾”。這種“過度近似”的環(huán)境建模能夠允許人們更為保守地捕捉環(huán)境的不確定性，而無需過于詳細(xì)的模型，這種模型的推理是很不高效的。然而，對(duì)于基于 AI 的自主性，純粹的非確定性建?？赡軙?huì)產(chǎn)生太多虛假的錯(cuò)誤報(bào)告，從而使驗(yàn)證過程在實(shí)踐中變得毫無用處。例如在對(duì)一輛自動(dòng)駕駛汽車的周圍車輛行為的建模中，周圍車輛的行為多種多樣，如果采用純粹的非確定性建模，就考慮不到總是意外發(fā)生的事故。此外，許多 AI/ML 系統(tǒng)隱式或顯式地對(duì)來自環(huán)境的數(shù)據(jù)或行為做出分布假設(shè)，從而需要進(jìn)行概率建模。由于很難準(zhǔn)確地確定潛在的分布，所以不能假定生成的概率模型是完美的，并且必須在模型本身中對(duì)建模過程中的不確定性加以表征。

概率形式建模。為了應(yīng)對(duì)這一挑戰(zhàn)，我們建議使用結(jié)合概率建模和非確定性建模的形式。在能夠可靠地指定或估計(jì)概率分布的情況下，可以使用概率建模。在其他情況下，非確定性建模可用于對(duì)環(huán)境行為進(jìn)行過度近似。雖然諸如馬爾可夫決策過程之類的形式主義已經(jīng)提供了一種混合概率和非確定性的方法，但我們相信，更豐富的形式主義如概率規(guī)劃范式，可以提供一種更具表達(dá)力和程序化的方式來對(duì)環(huán)境進(jìn)行建模。我們預(yù)測(cè)，在許多情況下，此類概率程序需要（部分地）從數(shù)據(jù)中進(jìn)行學(xué)習(xí)或合成。此時(shí)，學(xué)習(xí)參數(shù)中的任何不確定性都必須傳播到系統(tǒng)的其余部分，并在概率模型中加以表示。例如，凸馬爾可夫決策過程提供了一種方法來表示學(xué)習(xí)轉(zhuǎn)變概率值的不確定性，并擴(kuò)展了用于驗(yàn)證和控制的算法來解釋這種不確定性。

2.2 未知的變量?

在傳統(tǒng)的形式驗(yàn)證領(lǐng)域如驗(yàn)證設(shè)備驅(qū)動(dòng)程序中，系統(tǒng) S 與其環(huán)境 E 之間的接口定義良好，E 只能通過該接口與 S 進(jìn)行交互。對(duì)于基于 AI 的自主性而言，該接口是不完善的，它由傳感器和感知組件規(guī)定，這些組件只能部分且嘈雜地捕捉環(huán)境，而且無法捕捕捉 S 和 E 之間的所有交互。所有環(huán)境的變量（特征）都是已知的，更不用說被感知到的變量。即使在環(huán)境變量已知的受限場(chǎng)景中，也明顯缺乏有關(guān)其演變的信息，尤其是在設(shè)計(jì)的時(shí)候。此外，代表環(huán)境接口的激光雷達(dá)等傳感器建模也是一項(xiàng)重大的技術(shù)挑戰(zhàn)。

內(nèi)省環(huán)境建模。我們建議通過開發(fā)內(nèi)省的設(shè)計(jì)和驗(yàn)證方法來解決這個(gè)問題，也就是說，在系統(tǒng) S 中進(jìn)行內(nèi)省，來對(duì)關(guān)于環(huán)境 E 的假設(shè) A 進(jìn)行算法上的識(shí)別，該假設(shè)足以保證滿足規(guī)范 Φ。理想情況下，A 必須是此類假設(shè)中最弱的一個(gè)，并且還必須足夠高效，以便在設(shè)計(jì)時(shí)生成、并在運(yùn)行時(shí)監(jiān)控可用傳感器和有關(guān)環(huán)境的其他信息源，以及方便在假設(shè)被違反時(shí)可以采取緩解措施。此外，如果涉及人類操作員，人們可能希望 A 可以翻譯成可理解的解釋，也就是說 S 可以向人類“解釋”為什么它可能無法滿足規(guī)范 Φ。處理這些多重要求以及對(duì)良好傳感器模型的需求，使得內(nèi)省環(huán)境建模成為一個(gè)非常重要的問題。初步的工作表明，這種可監(jiān)控假設(shè)的提取在簡(jiǎn)單的情況下是可行的，雖然需要做更多的工作才能讓它具有實(shí)用性。

2.3 模擬人類行為?

對(duì)于許多 AI 系統(tǒng)，例如半自動(dòng)駕駛汽車，人類代理是環(huán)境和系統(tǒng)的關(guān)鍵部分。關(guān)于人類的人工模型無法充分捕捉人類行為的可變性和不確定性。另一方面，用于建模人類行為的數(shù)據(jù)驅(qū)動(dòng)方法可能對(duì) ML 模型使用的特征的表達(dá)能力和數(shù)據(jù)質(zhì)量敏感。為了實(shí)現(xiàn)人類 AI 系統(tǒng)的高度保證，我們必須解決當(dāng)前人類建模技術(shù)的局限性，并為其預(yù)測(cè)準(zhǔn)確性和收斂性提供保障。

主動(dòng)的數(shù)據(jù)驅(qū)動(dòng)建模。我們相信，人類建模需要一種主動(dòng)的數(shù)據(jù)驅(qū)動(dòng)方法，模型結(jié)構(gòu)和以數(shù)學(xué)形式表示的特征適合使用形式方法。人類建模的一個(gè)關(guān)鍵部分是捕捉人類意圖。我們提出了一個(gè)三管齊下的方法：基于專家知識(shí)來定義模型的模板或特征，用離線學(xué)習(xí)來完成模型以供設(shè)計(jì)時(shí)使用，以及在運(yùn)行時(shí)通過監(jiān)控和與環(huán)境交互來學(xué)習(xí)和更新環(huán)境模型。例如，已經(jīng)有研究表明，通過人類受試者實(shí)驗(yàn)從駕駛模擬器收集的數(shù)據(jù)，可用于生成人類駕駛員的行為模型，這些模型可用于驗(yàn)證和控制自動(dòng)駕駛汽車。此外，計(jì)算機(jī)安全領(lǐng)域的對(duì)抗性訓(xùn)練和攻擊技術(shù)可用于人類模型的主動(dòng)學(xué)習(xí)，并可針對(duì)導(dǎo)致不安全行為的特定人類動(dòng)作來進(jìn)一步設(shè)計(jì)模型。這些技術(shù)可以幫助開發(fā) human-AI 系統(tǒng)的驗(yàn)證算法。

形式化規(guī)范

形式化驗(yàn)證嚴(yán)重依賴于形式化規(guī)范——即對(duì)系統(tǒng)應(yīng)該做什么的精確的數(shù)學(xué)陳述。即使在形式化方法已經(jīng)取得相當(dāng)大成功的領(lǐng)域，提出高質(zhì)量的形式化規(guī)范也是一項(xiàng)挑戰(zhàn)，而 AI 系統(tǒng)尤其面臨著獨(dú)特的挑戰(zhàn)。

3.1 難以形式化的任務(wù)?

圖 2 中 AEBS 控制器中的感知模塊必須檢測(cè)和分類對(duì)象，從而將車輛和行人與其他實(shí)體區(qū)分開來。在經(jīng)典的形式方法意義上，這個(gè)模塊的準(zhǔn)確性要求對(duì)每種類型的道路使用者和對(duì)象進(jìn)行形式定義，這是極其困難的。這種問題存在于這個(gè)感知模塊的所有實(shí)現(xiàn)中，而不僅僅出現(xiàn)在基于深度學(xué)習(xí)的方法中。其他涉及感知和交流的任務(wù)也會(huì)出現(xiàn)類似的問題，比如自然語(yǔ)言處理。那么，我們?nèi)绾螢檫@樣的模塊指定精度屬性呢？規(guī)范語(yǔ)言應(yīng)該是什么？我們可以使用哪些工具來構(gòu)建規(guī)范？

端到端/系統(tǒng)水平的規(guī)范（End-to-end/system-level specifications）。為了應(yīng)對(duì)上述挑戰(zhàn)，我們可以對(duì)這個(gè)問題稍加變通。與其直接對(duì)難以形式化的任務(wù)進(jìn)行規(guī)范，不如首先專注于精確地指定 AI 系統(tǒng)的端到端行為。從這種系統(tǒng)水平的規(guī)范中，可以獲得對(duì)難以形式化的組件的輸入-輸出接口的約束。這些約束用作一個(gè)組件水平（component-level ）的規(guī)范，這個(gè)規(guī)范與整個(gè) AI 系統(tǒng)的上下文相關(guān)。對(duì)于圖 2 中的 AEBS 示例，這涉及對(duì)屬性 Φ 的規(guī)定，該屬性即在運(yùn)動(dòng)過程中與任何對(duì)象都保持最小距離，從中我們可得出對(duì) DNN 輸入空間的約束，在對(duì)抗分析中捕捉語(yǔ)義上有意義的輸入空間。

3.2 定量規(guī)范 vs. 布爾規(guī)范?

傳統(tǒng)上，形式規(guī)范往往是布爾型的，它將給定的系統(tǒng)行為映射為“真”或“假”。然而，在 AI 和 ML 中，規(guī)范通常作為規(guī)范成本或獎(jiǎng)勵(lì)的目標(biāo)函數(shù)給出。此外，可能有多個(gè)目標(biāo)，其中一些必須一起滿足，而另一些則可能需要在某些環(huán)境中相互權(quán)衡。統(tǒng)一布爾和定量?jī)煞N規(guī)范方法的最佳方式是什么？是否有能夠統(tǒng)一捕捉 AI 組件常見屬性（如魯棒性和公平性）的形式？

混合定量和布爾規(guī)范。布爾規(guī)范和定量規(guī)范都有其優(yōu)點(diǎn)：布爾規(guī)范更容易組合，但目標(biāo)函數(shù)有助于用基于優(yōu)化的技術(shù)進(jìn)行驗(yàn)證和綜合，并定義更精細(xì)的屬性滿足粒度。彌補(bǔ)這一差距的一種方法是轉(zhuǎn)向定量規(guī)范語(yǔ)言，例如使用具有布爾和定量語(yǔ)義的邏輯（如度量時(shí)序邏輯），或?qū)⒆詣?dòng)機(jī)與 RL 的獎(jiǎng)勵(lì)函數(shù)相結(jié)合。另一種方法是將布爾和定量規(guī)范組合成一個(gè)通用的規(guī)范結(jié)構(gòu)，例如一本規(guī)則手冊(cè) ，手冊(cè)中的規(guī)范可以按層次結(jié)構(gòu)進(jìn)行組織、比較和匯總。有研究已經(jīng)確定了 AI 系統(tǒng)的幾類屬性，包括魯棒性、公平性、隱私性、問責(zé)性和透明度。研究者正在提出新的形式主義，將形式方法和 ML 的思想聯(lián)系起來，以對(duì)這些屬性的變體（如語(yǔ)義魯棒性）進(jìn)行建模。

3.3 數(shù)據(jù) vs. 形式要求?

“數(shù)據(jù)即規(guī)范”的觀點(diǎn)在機(jī)器學(xué)習(xí)中很常見。有限輸入集上標(biāo)記的“真實(shí)”數(shù)據(jù)通常是關(guān)于正確行為的唯一規(guī)范。這與形式化方法非常不同，形式化方法通常以邏輯或自動(dòng)機(jī)的形式給出，它定義了遍歷所有可能輸入的正確行為的集合。數(shù)據(jù)和規(guī)范之間的差距值得注意，尤其是當(dāng)數(shù)據(jù)有限、有偏見或來自非專家時(shí)。我們需要技術(shù)來對(duì)數(shù)據(jù)的屬性進(jìn)行形式化，包括在設(shè)計(jì)時(shí)可用的數(shù)據(jù)和尚未遇到的數(shù)據(jù)。

規(guī)范挖掘(Specification mining)。為了彌合數(shù)據(jù)和形式規(guī)范之間的差距，我們建議使用算法從數(shù)據(jù)和其他觀察中來推斷規(guī)范——即所謂的規(guī)范挖掘技術(shù)。此類方法通?？捎糜?ML 組件，包括感知組件，因?yàn)樵谠S多情況下，它不需要具有精確的規(guī)范或人類可讀的規(guī)范。我們還可以使用規(guī)范挖掘方法，從演示或更復(fù)雜的多個(gè)代理（人類和人工智能）之間的交互形式來推斷人類意圖和其他屬性。

學(xué)習(xí)系統(tǒng)的建模

在形式驗(yàn)證的大多數(shù)傳統(tǒng)應(yīng)用中，系統(tǒng) S 在設(shè)計(jì)時(shí)是固定的且已知的，比如它可以是一個(gè)程序，或者一個(gè)用編程語(yǔ)言或硬件描述語(yǔ)言來描述的電路。系統(tǒng)建模問題主要涉及的，是通過抽象掉不相關(guān)的細(xì)節(jié)，來將 S 減小到更易于處理的大小。AI 系統(tǒng)給系統(tǒng)建模帶來了非常不同的挑戰(zhàn)，這主要源于機(jī)器學(xué)習(xí)的使用：

高維輸入空間?

用于感知的 ML 組件通常在非常高維的輸入空間上運(yùn)行。比如，一個(gè)輸入的RGB 圖像可以是 1000 x 600 像素，它包含256((1000x600x3)) 個(gè)元素，輸入通常就是這樣的高維向量流。盡管研究人員已經(jīng)對(duì)高維輸入空間（如在數(shù)字電路中）使用了形式化方法，但基于 ML 的感知輸入空間的性質(zhì)是不同的，它不完全是布爾值，而是混合的，包括離散變量和連續(xù)變量。

高維參數(shù)/狀態(tài)空間?

深度神經(jīng)網(wǎng)絡(luò)等 ML 組件具有數(shù)千到數(shù)百萬個(gè)模型參數(shù)和原始組件。例如，圖 2 中使用的最先進(jìn)的 DNN 有多達(dá) 6000 萬個(gè)參數(shù)和數(shù)十層組件。這就產(chǎn)生了巨大的驗(yàn)證搜索空間，抽象過程需要非常仔細(xì)。

在線適應(yīng)和進(jìn)化?

一些學(xué)習(xí)系統(tǒng)如使用 RL 的機(jī)器人，會(huì)隨著它們遇到的新數(shù)據(jù)和新情況而發(fā)生進(jìn)化。對(duì)于這樣的系統(tǒng)，設(shè)計(jì)時(shí)的驗(yàn)證必須考慮系統(tǒng)行為的未來演變，或者隨著學(xué)習(xí)系統(tǒng)的發(fā)展逐步地在線執(zhí)行。

在上下文中建模系統(tǒng)?

對(duì)于許多 AI/ML 組件，它們的規(guī)范僅僅由上下文來定義。例如，要驗(yàn)證圖 2 中基于 DNN 的系統(tǒng)的安全性，就需要對(duì)環(huán)境進(jìn)行建模。我們需要對(duì) ML 組件及其上下文進(jìn)行建模的技術(shù)，以便可以驗(yàn)證在語(yǔ)義上有意義的屬性。

近年來，許多工作都專注于提高效率，來驗(yàn)證 DNN 的魯棒性和輸入-輸出屬性。然而，這還不夠，我們還需要在以下三個(gè)方面取得進(jìn)展：

自動(dòng)抽象和高效表示?

自動(dòng)生成系統(tǒng)的抽象一直是形式方法的關(guān)鍵，它在將形式方法的范圍擴(kuò)展到大型硬件和軟件系統(tǒng)方面發(fā)揮著至關(guān)重要的作用。為了解決基于 ML 的系統(tǒng)的超高維混合狀態(tài)空間和輸入空間方面的挑戰(zhàn)，我們需要開發(fā)有效的技術(shù)來將 ML 模型抽象為更易于形式分析的、更簡(jiǎn)單的模型。一些有希望的方向包括：使用抽象解釋來分析 DNN，開發(fā)用于偽造有 ML 組件的網(wǎng)絡(luò)物理系統(tǒng)的抽象，以及設(shè)計(jì)用于驗(yàn)證的新表示（比如星集）。

解釋與因果

如果學(xué)習(xí)者在其預(yù)測(cè)中附上關(guān)于預(yù)測(cè)是如何從數(shù)據(jù)和背景知識(shí)中產(chǎn)生的的解釋，那我們就可以簡(jiǎn)化對(duì)學(xué)習(xí)系統(tǒng)進(jìn)行建模的任務(wù)。這個(gè)想法并不新鮮，ML 社區(qū)已經(jīng)對(duì)諸如“基于解釋的泛化”等術(shù)語(yǔ)進(jìn)行了研究，但是最近，人們正在對(duì)使用邏輯來解釋學(xué)習(xí)系統(tǒng)的輸出重新產(chǎn)生了興趣。解釋生成有助于在設(shè)計(jì)時(shí)調(diào)試設(shè)計(jì)和規(guī)范，并有助于合成魯棒的 AI 系統(tǒng)以在運(yùn)行時(shí)提供保障。包含因果推理和反事實(shí)推理的 ML  還可以幫助生成用于形式方法的解釋。

語(yǔ)義特征空間?

當(dāng)生成的對(duì)抗性輸入和反例在所使用的 ML 模型的上下文中具有語(yǔ)義意義時(shí)，ML 模型的對(duì)抗性分析和形式驗(yàn)證就更有意義。例如，針對(duì)汽車顏色或一天中時(shí)間的微小變化來分析 DNN 對(duì)象檢測(cè)器的技術(shù)，比向少量任意選擇的像素添加噪聲的技術(shù)更有用。當(dāng)前，大多數(shù)的方法在這一點(diǎn)上都還達(dá)不到要求。我們需要語(yǔ)義對(duì)抗分析，即在ML 模型所屬系統(tǒng)的上下文中對(duì)它們進(jìn)行分析。其中額的一個(gè)關(guān)鍵步驟，是表示對(duì) ML 系統(tǒng)運(yùn)行的環(huán)境建模的語(yǔ)義特征空間，而不是為 ML 模型定義輸入空間的具體特征空間。這是符合直覺的，即與完整的具體特征空間相比，具體特征空間在語(yǔ)義上有意義的部分（如交通場(chǎng)景圖像）所形成的潛在空間要低得多。圖 2 中的語(yǔ)義特征空間是代表自動(dòng)駕駛汽車周圍 3D 世界的低維空間，而具體的特征空間是高維像素空間。由于語(yǔ)義特征空間的維數(shù)較低，因此可以更容易地進(jìn)行搜索。但是，我們還需要一個(gè)“渲染器”，將語(yǔ)義特征空間中的一個(gè)點(diǎn)映射到具體特征空間中的一個(gè)點(diǎn)。渲染器的屬性如可微性（differentiability），可以更容易地應(yīng)用形式化方法來執(zhí)行語(yǔ)義特征空間的目標(biāo)導(dǎo)向搜索。

用于設(shè)計(jì)和驗(yàn)證的計(jì)算引擎

硬件和軟件系統(tǒng)形式化方法的有效性，是由底層“計(jì)算引擎”的進(jìn)步推動(dòng)的——例如，布爾可滿足性求解 (SAT)、可滿足性模理論 (SMT) 和模型檢查。鑒于 AI/ML 系統(tǒng)規(guī)模、環(huán)境復(fù)雜性和所涉及的新型規(guī)范，需要一類新的計(jì)算引擎來進(jìn)行高效且可擴(kuò)展的訓(xùn)練、測(cè)試、設(shè)計(jì)和驗(yàn)證，實(shí)現(xiàn)這些進(jìn)步必須克服的關(guān)鍵挑戰(zhàn)。

5.1 數(shù)據(jù)集設(shè)計(jì)?

數(shù)據(jù)是機(jī)器學(xué)習(xí)的基本起點(diǎn)，提高 ML 系統(tǒng)質(zhì)量就必須提高它所學(xué)習(xí)數(shù)據(jù)的質(zhì)量。形式化方法如何幫助 ML 數(shù)據(jù)系統(tǒng)地選擇、設(shè)計(jì)和擴(kuò)充？

ML 的數(shù)據(jù)生成與硬件和軟件的測(cè)試生成問題有相似之處。形式化方法已被證明對(duì)系統(tǒng)的、基于約束的測(cè)試生成是有效的，但這與對(duì)人工智能系統(tǒng)的要求不同，約束類型可能要復(fù)雜得多——例如，對(duì)使用傳感器從復(fù)雜環(huán)境（如交通狀況）捕獲的數(shù)據(jù)的“真實(shí)性”進(jìn)行編碼要求。我們不僅需要生成具有特定特征的數(shù)據(jù)項(xiàng)（如發(fā)現(xiàn)錯(cuò)誤的測(cè)試），還需要生成滿足分布約束的集合；數(shù)據(jù)生成必須滿足數(shù)據(jù)集大小和多樣性的目標(biāo)，以進(jìn)行有效的訓(xùn)練和泛化。這些要求都需要開發(fā)一套新的形式化技術(shù)。

形式方法中的受控隨機(jī)化。數(shù)據(jù)集設(shè)計(jì)的這個(gè)問題有很多方面，首先必須定義“合法”輸入的空間，以便根據(jù)應(yīng)用程序語(yǔ)義正確形成示例；其次，需要捕獲與現(xiàn)實(shí)世界數(shù)據(jù)相似性度量的約束；第三，通常需要對(duì)生成的示例的分布進(jìn)行約束，以獲得學(xué)習(xí)算法收斂到真實(shí)概念的保證。

我們相信這些方面可以通過隨機(jī)形式方法來解決——用于生成受形式約束和分布要求的數(shù)據(jù)的隨機(jī)算法。一類稱為控制即興創(chuàng)作的新技術(shù)是很有前景的，即興創(chuàng)作的生成要滿足三個(gè)約束的隨機(jī)字符串（示例）x：

• 定義合法x空間的硬約束
• 一個(gè)軟約束，定義生成的x必須如何與真實(shí)世界的示例相似
• 定義輸出分布約束的隨機(jī)性要求

目前，控制即興理論仍處于起步階段，我們才剛剛開始了解計(jì)算復(fù)雜性并設(shè)計(jì)有效的算法。反過來，即興創(chuàng)作依賴于計(jì)算問題的最新進(jìn)展，例如約束隨機(jī)抽樣、模型計(jì)數(shù)和基于概率編程的生成方法。

5.2 定量驗(yàn)證?

除了通過傳統(tǒng)指標(biāo)（狀態(tài)空間維度、組件數(shù)量等）衡量AI 系統(tǒng)規(guī)模之外，組件的類型可能要復(fù)雜得多。例如，自主和半自主車輛及其控制器必須建模為混合動(dòng)力系統(tǒng)，結(jié)合離散和連續(xù)動(dòng)力學(xué)；此外，環(huán)境中的代表（人類、其他車輛）可能需要建模為概率過程。最后，需求可能不僅涉及傳統(tǒng)關(guān)于安全性和活性的布爾規(guī)范，還包括對(duì)系統(tǒng)魯棒性和性能的定量要求，然而大多數(shù)現(xiàn)有的驗(yàn)證方法，都是針對(duì)回答布爾驗(yàn)證問題。為了解決這一差距，必須開發(fā)用于定量驗(yàn)證的新可擴(kuò)展引擎。

定量語(yǔ)義分析。一般來說，人工智能系統(tǒng)的復(fù)雜性和異構(gòu)性意味著，規(guī)范的形式驗(yàn)證（布爾或定量）是不可判定的——例如，即便是確定線性混合系統(tǒng)的狀態(tài)是否可達(dá)，也是不可判定的。為了克服計(jì)算復(fù)雜性帶來的這一障礙，人們必須在語(yǔ)義特征空間上使用概率和定量驗(yàn)證的新技術(shù)，以增強(qiáng)本節(jié)前面討論的抽象和建模方法。對(duì)于同時(shí)具有布爾和定量語(yǔ)義的規(guī)范形式，在諸如度量時(shí)間邏輯之類的形式中，將驗(yàn)證表述為優(yōu)化，對(duì)于統(tǒng)一來自形式方法的計(jì)算方法和來自優(yōu)化文獻(xiàn)的計(jì)算方法至關(guān)重要。例如在基于模擬的時(shí)間邏輯證偽中，盡管它們必須應(yīng)用于語(yǔ)義特征空間以提高效率，這種偽造技術(shù)也可用于系統(tǒng)地、對(duì)抗性地生成 ML 組件的訓(xùn)練數(shù)據(jù)。概率驗(yàn)證的技術(shù)應(yīng)該超越傳統(tǒng)的形式，如馬爾科夫鏈或MDPs，以驗(yàn)證語(yǔ)義特征空間上的概率程序。同樣，關(guān)于SMT求解的工作必須擴(kuò)展到更有效地處理成本約束--換句話說，將SMT求解與優(yōu)化方法相結(jié)合。

我們需要了解在設(shè)計(jì)時(shí)可以保證什么，設(shè)計(jì)過程如何有助于運(yùn)行時(shí)的安全操作，以及設(shè)計(jì)時(shí)和運(yùn)行時(shí)技術(shù)如何有效地互操作。

5.3 AI/ML 的組合推理?

對(duì)于擴(kuò)展到大型系統(tǒng)的正式方法，組合（模塊化）推理是必不可少的。在組合驗(yàn)證中，一個(gè)大型系統(tǒng)（例如，程序）被拆分為它的組件（例如，程序），每個(gè)組件都根據(jù)規(guī)范進(jìn)行驗(yàn)證，然后組件規(guī)范一起產(chǎn)生系統(tǒng)級(jí)規(guī)范。組合驗(yàn)證的一個(gè)常見方法是使用假設(shè)-保證合同，例如一個(gè)過程假設(shè)一些關(guān)于它的開始狀態(tài)（前置條件），反過來又保證其結(jié)束狀態(tài)（后置條件），類似的假設(shè)-保證范式已被開發(fā)并應(yīng)用于并發(fā)的軟件和硬件系統(tǒng)。

然而，這些范式并不涵蓋人工智能系統(tǒng)，這在很大程度上是由于 "形式化規(guī)范 "一節(jié)中討論的人工智能系統(tǒng)的規(guī)范化挑戰(zhàn)。組合式驗(yàn)證需要組合式規(guī)范——也就是說，組件必須是可形式化的。然而，正如“形式化規(guī)范”中所述，可能無法正式指定一個(gè)感知組件的正確行為。因此，挑戰(zhàn)之一就是開發(fā)不依賴于有完整組合規(guī)范的組合推理技術(shù)。此外，人工智能系統(tǒng)的定量和概率性質(zhì)，要求將組合推理的理論擴(kuò)展到定量系統(tǒng)和規(guī)范。

推斷組件合同。人工智能系統(tǒng)的組合式設(shè)計(jì)和分析需要在多個(gè)方面取得進(jìn)展。首先，需要在一些有前景的初步工作基礎(chǔ)上，為這些系統(tǒng)的語(yǔ)義空間開發(fā)概率保證設(shè)計(jì)和驗(yàn)證的理論。第二，必須設(shè)計(jì)出新的歸納綜合技術(shù)，以算法方式生成假設(shè)-保證合同，減少規(guī)范負(fù)擔(dān)并促進(jìn)組合推理。第三，為了處理諸如感知等沒有精確正式規(guī)格的組件的情況，我們提出了從系統(tǒng)級(jí)分析中推斷組件級(jí)約束的技術(shù)，并使用這種約束將組件級(jí)分析，包括對(duì)抗性分析，集中在搜索輸入空間的 "相關(guān) "部分。

建構(gòu)中修正智能系統(tǒng)

在理想的世界中，驗(yàn)證將與設(shè)計(jì)過程相結(jié)合，因此系統(tǒng)是“在建構(gòu)中修正的”。例如，驗(yàn)證可以與編譯/合成步驟交錯(cuò)進(jìn)行，假設(shè)在集成電路中常見的寄存器傳輸級(jí)（RTL）設(shè)計(jì)流程中，或許它可以被集成到合成算法中，以確保實(shí)現(xiàn)滿足規(guī)范。我們能不能為人工智能系統(tǒng)設(shè)計(jì)一個(gè)合適的在建構(gòu)中逐步修正的設(shè)計(jì)流程？

6.1 ML 組件的規(guī)范驅(qū)動(dòng)設(shè)計(jì)

給定一個(gè)正式的規(guī)范，我們能否設(shè)計(jì)一個(gè)可證明滿足該規(guī)范的機(jī)器學(xué)習(xí)組件（模型）？這種全新的 ML 組件設(shè)計(jì)有很多方面：（1）設(shè)計(jì)數(shù)據(jù)集，（2） 綜合模型的結(jié)構(gòu)，（3）生成一組有代表性的特征，（4） 綜合超參數(shù)和 ML 算法選擇的其他方面，以及（5）在綜合失敗時(shí)自動(dòng)化調(diào)試 ML 模型或規(guī)范的技術(shù)。

ML 組件的正式合成。解決前面所列出一些問題的解決方案正在出現(xiàn)，可以使用語(yǔ)義損失函數(shù)或通過認(rèn)證的魯棒性在 ML 模型上強(qiáng)制執(zhí)行屬性，這些技術(shù)可以與神經(jīng)架構(gòu)搜索等方法相結(jié)合，以生成正確構(gòu)建的 DNN。另一種方法是基于新興的形式歸納綜合理論，即從滿足形式化規(guī)范的程序?qū)嵗羞M(jìn)行綜合。解決形式歸納綜合問題的最常見方法是使用 oracle-guided 方法，其中將學(xué)習(xí)者與回答查詢的 oracle 配對(duì)；如示例中圖2，oracle 可以是一個(gè)偽造者，它生成反例，顯示學(xué)習(xí)組件的故障如何違反系統(tǒng)級(jí)規(guī)范。最后，使用定理證明來確保用于訓(xùn)練 ML 模型的算法的正確性，也是朝著建構(gòu)修正的 ML 組件邁出的重要一步。

6.2 基于機(jī)器學(xué)習(xí)的系統(tǒng)設(shè)計(jì)?

第二個(gè)挑戰(zhàn)，是設(shè)計(jì)一個(gè)包含學(xué)習(xí)和非學(xué)習(xí)組件的整體系統(tǒng)。目前已經(jīng)出現(xiàn)的幾個(gè)研究問題：我們能否計(jì)算出可以限制 ML 組件運(yùn)行的安全范圍？我們能否設(shè)計(jì)一種控制或規(guī)劃算法來克服它接收輸入的基于 ML 感知組件的限制？我們可以為人工智能系統(tǒng)設(shè)計(jì)組合設(shè)計(jì)理論嗎？當(dāng)兩個(gè) ML 模型用于感知兩種不同類型的傳感器數(shù)據(jù)（例如，LiDAR 和視覺圖像），并且每個(gè)模型在某些假設(shè)下都滿足其規(guī)范，那么二者在什么條件下可以一起使用、以提高可靠性整體系統(tǒng)？

在這一挑戰(zhàn)上，取得進(jìn)展的一個(gè)突出例子是基于安全學(xué)習(xí)的控制的工作。這種方法預(yù)先計(jì)算了一個(gè)安全包絡(luò)線，并使用學(xué)習(xí)算法在該包絡(luò)線內(nèi)調(diào)整控制器，需要基于例如可達(dá)性分析、來有效計(jì)算此類安全包絡(luò)的技術(shù)；同樣，安全 RL 領(lǐng)域也取得了顯著進(jìn)展。

然而，這些并沒有完全解決機(jī)器學(xué)習(xí)對(duì)感知和預(yù)測(cè)帶來的挑戰(zhàn)——例如，可證明安全的端到端深度強(qiáng)化學(xué)習(xí)尚未實(shí)現(xiàn)。

6.3 為彈性 AI 橋接設(shè)計(jì)時(shí)間和運(yùn)行時(shí)間?

正如“環(huán)境建?！辈糠炙懻摰哪菢?，許多 AI 系統(tǒng)在無法先驗(yàn)指定的環(huán)境中運(yùn)行，因此總會(huì)有無法保證正確性的環(huán)境。在運(yùn)行時(shí)實(shí)現(xiàn)容錯(cuò)和錯(cuò)誤恢復(fù)的技術(shù)，對(duì)人工智能系統(tǒng)具有重要作用。我們需要系統(tǒng)地理解在設(shè)計(jì)時(shí)可以保證什么，設(shè)計(jì)過程如何有助于人工智能系統(tǒng)在運(yùn)行時(shí)的安全和正確運(yùn)行，以及設(shè)計(jì)時(shí)和運(yùn)行時(shí)技術(shù)如何有效地互操作。

對(duì)此，關(guān)于容錯(cuò)和可靠系統(tǒng)的文獻(xiàn)為我們提供了開發(fā)運(yùn)行時(shí)保證技術(shù)的基礎(chǔ)——即運(yùn)行時(shí)驗(yàn)證和緩解技術(shù)；例如 Simplex 方法，就提供了一種將復(fù)雜但容易出錯(cuò)的模塊與安全的、正式驗(yàn)證的備份模塊相結(jié)合的方法。最近，結(jié)合設(shè)計(jì)時(shí)和運(yùn)行時(shí)保證方法的技術(shù)顯示了未驗(yàn)證的組件、包括那些基于人工智能和 ML 的組件，可以被包裹在運(yùn)行時(shí)保證框架中，以提供安全運(yùn)行的保證。但目前這些僅限于特定類別的系統(tǒng)，或者它們需要手動(dòng)設(shè)計(jì)運(yùn)行時(shí)監(jiān)視器和緩解策略，在諸如內(nèi)省環(huán)境建模、人工智能的監(jiān)測(cè)器和安全回退策略的合成等方法上，還有更多的工作需要做。

此處討論的建構(gòu)中修正智能系統(tǒng)的設(shè)計(jì)方法可能會(huì)引入開銷，使其更難以滿足性能和實(shí)時(shí)要求。但我們相信（也許是非直覺的），在以下意義上，形式化方法甚至可以幫助提高系統(tǒng)的性能或能源效率。

傳統(tǒng)的性能調(diào)優(yōu)往往與上下文無關(guān)——例如，任務(wù)需要獨(dú)立于它們運(yùn)行的環(huán)境來滿足最后期限。但如果設(shè)計(jì)時(shí)就對(duì)這些環(huán)境進(jìn)行正式表征，并在運(yùn)行時(shí)對(duì)其進(jìn)行監(jiān)控，如果其系統(tǒng)運(yùn)行經(jīng)過正式驗(yàn)證是安全的，那么在這種環(huán)境下，ML 模型就可以用準(zhǔn)確性來?yè)Q取更高的效率。這種權(quán)衡可能是未來研究的一個(gè)富有成果的領(lǐng)域。

結(jié)論

從形式化方法的角度來看，我們剖析了設(shè)計(jì)高保證人工智能系統(tǒng)的問題。如圖3所示，我們確定了將形式化方法應(yīng)用于 AI 系統(tǒng)的五個(gè)主要挑戰(zhàn)，并對(duì)這五項(xiàng)挑戰(zhàn)中的每一項(xiàng)都制定了三項(xiàng)設(shè)計(jì)和驗(yàn)證原則，這些原則有希望解決這個(gè)挑戰(zhàn)。

圖 3 中的邊顯示了這些原則之間的依賴關(guān)系，例如運(yùn)行時(shí)保證依賴于自省和數(shù)據(jù)驅(qū)動(dòng)的環(huán)境建模，以提取可監(jiān)測(cè)的假設(shè)和環(huán)境模型。同樣，為了進(jìn)行系統(tǒng)級(jí)分析，我們需要進(jìn)行組合推理和抽象，其中一些 AI 組件可能需要挖掘規(guī)范，而其他組件則通過形式化的歸納綜合構(gòu)建生成正確的結(jié)構(gòu)。

自 2016 年以來，包括作者在內(nèi)的幾位研究人員一直致力于應(yīng)對(duì)這些挑戰(zhàn)，當(dāng)時(shí)本文已發(fā)表的原始版本介紹了一些樣本進(jìn)展。我們已經(jīng)開發(fā)了開源工具 VerifAI 和 Scenic，它們實(shí)現(xiàn)了基于本文所述原則的技術(shù)，并已應(yīng)用于自動(dòng)駕駛和航空航天領(lǐng)域的工業(yè)規(guī)模系統(tǒng)。這些成果只是一個(gè)開始，還有很多事情要做。在未來的幾年里，可驗(yàn)證 AI 有望繼續(xù)成為一個(gè)富有成效的研究領(lǐng)域。