0
作者 | Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry
編譯 | 李梅、黃楠
編輯 | 陳彩嫻
人工智能試圖模仿人類智能的計算系統(tǒng)，包括人類一些與智能具有直觀聯(lián)系的功能，例如學習、解決問題以及理性地思考和行動。在廣義地解釋上，AI 一詞涵蓋了許多密切相關(guān)的領(lǐng)域如機器學習。那些大量使用 AI 的系統(tǒng)在醫(yī)療保健、交通運輸、金融、社交網(wǎng)絡(luò)、電子商務(wù)和教育等領(lǐng)域都產(chǎn)生了重大的社會影響。
這種日益增長的社會影響，也帶來了一系列風險和擔憂，包括人工智能軟件中的錯誤、網(wǎng)絡(luò)攻擊和人工智能系統(tǒng)安全等方面。因此，AI 系統(tǒng)的驗證問題以及更廣泛的可信 AI 的話題已經(jīng)開始引起研究界的關(guān)注。“可驗證 AI”已經(jīng)被確立為設(shè)計 AI 系統(tǒng)的目標，一個可驗證的 AI 系統(tǒng)在特定的數(shù)學要求上具有強大的、理想情況下可證明的正確性保證。我們怎樣才能實現(xiàn)這個目標？
最近，《ACM 通訊》（The Communications of ACM）上的一篇綜述文章，試圖從形式驗證的角度來思考可證驗 AI 面臨的挑戰(zhàn)，并給出了一些原則性的解決方案。文章作者是加州伯克利分校電氣工程與計算機科學系的主任 S. Shankar Sastry 和 Sanjit A. Seshia 教授，以及斯坦福大學計算機科學系助理教授 Dorsa Sadigh。
在計算機科學和工程領(lǐng)域，形式方法涉及系統(tǒng)的嚴格的數(shù)學規(guī)范、設(shè)計和驗證。其核心在于，形式方法是關(guān)于證明的：制定形成證明義務(wù)的規(guī)范，設(shè)計系統(tǒng)以履行這些義務(wù)，并通過算法證明搜索來驗證系統(tǒng)確實符合其規(guī)范。從規(guī)范驅(qū)動的測試和仿真到模型檢查和定理證明，一系列的形式化方法常被用于集成電路的計算機輔助設(shè)計，并已廣泛被用于發(fā)現(xiàn)軟件中的錯誤，分析網(wǎng)絡(luò)物理系統(tǒng)，并發(fā)現(xiàn)安全漏洞。
本文回顧了形式化方法傳統(tǒng)的應(yīng)用方式，指明了形式化方法在 AI 系統(tǒng)中的五個獨特挑戰(zhàn)，包括：
開發(fā)關(guān)于環(huán)境的語言、算法
對復雜 ML 組件和系統(tǒng)進行抽象和表示
為 AI 系統(tǒng)和數(shù)據(jù)提出新的規(guī)范形式化方法和屬性
開發(fā)針對自動推理的可擴展計算引擎
開發(fā)針對建構(gòu)中可信（trustworthy-by-construction）設(shè)計的算法和技術(shù)
在討論最新進展的基礎(chǔ)上，作者提出了解決以上挑戰(zhàn)的原則。本文不僅僅關(guān)注特定類型的 AI 組件如深度神經(jīng)網(wǎng)絡(luò)，或特定的方法如強化學習，而是試圖涵蓋更廣泛的 AI 系統(tǒng)及其設(shè)計過程。此外，形式化方法只是通往可信 AI 的其中一種途徑，所以本文的觀點旨在對來自其他領(lǐng)域的方法加以補充。這些觀點很大程度上來源于對自主和半自主系統(tǒng)中使用 AI 所產(chǎn)生的問題的思考，在這些系統(tǒng)中，安全性和驗證性問題更加突出。
圖 1 顯示了形式驗證、形式綜合和形式指導的運行時彈性的典型過程。形式驗證過程從三個輸入開始：
要驗證的系統(tǒng)模型 S
環(huán)境模型 E
待驗證的屬性 Φ
驗證者生成“是”或“否”的答案作為輸出，來表明 S 是否滿足環(huán)境 E 中的屬性 Φ。通常，“否”輸出伴隨著反例，也稱為錯誤跟蹤（error trace），它是對系統(tǒng)的執(zhí)行，表明 Φ 是如何被偽造的。一些驗證工具還包括帶有“是”答案的正確性證明或證書。我們對形式方法采取一種廣泛的視角，包括使用形式規(guī)范、驗證或綜合的某些方面的任何技術(shù)。例如，我們囊括了基于仿真的硬件驗證方法或基于模型的軟件測試方法，因為它們也使用正式的規(guī)范或模型來指導仿真或測試的過程。
要將形式驗證應(yīng)用于 AI 系統(tǒng)，必須能夠以形式來表示至少 S、E 和 Φ 這三個輸入，理想情況下，會存在有效的決策程序來回答先前所描述的“是/否”問題。然而，即使要對三個輸入構(gòu)建良好的表示，也并不是一件簡單的事，更不用說處理底層設(shè)計和驗證問題的復雜性了。
我們這里通過半自動駕駛領(lǐng)域的示例來說明本文的觀點。圖 2 顯示了一個 AI 系統(tǒng)的說明性示例：一個閉環(huán) CPS，包括一輛帶有機器學習組件的半自動車輛及其環(huán)境。具體來說，假設(shè)半自動的“自我”（ego）車輛有一個自動緊急制動系統(tǒng) (AEBS)，該系統(tǒng)試圖對前方的物體進行檢測和分類，并在需要避免碰撞時啟動制動器。圖 2 中，一個 AEBS 包括一個由控制器（自動制動）、一個受控對象（受控的車輛子系統(tǒng)，包括自主堆棧的其他部分）和一個傳感器（攝像頭），以及一個使用 DNN 的感知組件。AEBS 與車輛環(huán)境相結(jié)合，形成一個閉環(huán) CPS?！白晕摇避囕v的環(huán)境包括車輛外部（其他車輛、行人等）以及車輛內(nèi)部（例如駕駛員）的代理和對象。這種閉環(huán)系統(tǒng)的安全要求可以非形式地刻畫為以一種屬性，即在移動的“自我”車輛與道路上的任何其他代理或物體之間保持安全距離。然而，這種系統(tǒng)在規(guī)范、建模和驗證方面存在許多細微差別。
圖 2：包含機器學習組件的閉環(huán) CPS 示例
第一，考慮對半自動車輛的環(huán)境進行建模。即使是環(huán)境中有多少和哪些代理（包括人類和非人類）這樣的問題，也可能存在相當大的不確定性，更不用說它們的屬性和行為了。第二，使用 AI 或 ML 的感知任務(wù)即使不是不可能，也很難形式化地加以規(guī)定。第三，諸如 DNN 之類的組件可能是在復雜、高維輸入空間上運行的復雜、高維對象。因此，在生成形式驗證過程的三個輸入 S、E、Φ 時，即便采用一種能夠使驗證易于處理的形式，也十分具有挑戰(zhàn)性。
如果有人解決了這個問題，那就會面臨一項艱巨的任務(wù)，即驗證一個如圖 2 那樣復雜的基于 AI 的 CPS。在這樣的 CPS 中，組合（模塊化）方法對于可擴展性來說至關(guān)重要，但它會由于組合規(guī)范的難度之類的因素而難以實施。最后，建構(gòu)中修正的方法（correct-by-construction,CBC）有望實現(xiàn)可驗證 AI，但它還處于起步階段，非常依賴于規(guī)范和驗證方面的進步。圖 3 總結(jié)了可驗證 AI 的五個挑戰(zhàn)性領(lǐng)域。對于每個領(lǐng)域，我們將目前有前景的方法提煉成克服挑戰(zhàn)的三個原則，用節(jié)點表示。節(jié)點之間的邊緣顯示了可驗證 AI 的哪些原則相互依賴，共同的依賴線程由單一顏色表示。下文將詳細闡述這些挑戰(zhàn)和相應(yīng)的原則。
圖 3：可驗證 AI 的 5 個挑戰(zhàn)領(lǐng)域總結(jié)
基于 AI/ML 的系統(tǒng)所運行的環(huán)境通常很復雜， 比如對自動駕駛汽車運行的各種城市交通環(huán)境的建模。事實上，AI/ML 經(jīng)常被引入這些系統(tǒng)中以應(yīng)對環(huán)境的復雜性和不確定性。當前的 ML 設(shè)計流程通常使用數(shù)據(jù)來隱性地規(guī)定環(huán)境。許多 AI 系統(tǒng)的目標是在其運行過程中發(fā)現(xiàn)并理解其環(huán)境，這與為先驗指定的環(huán)境設(shè)計的傳統(tǒng)系統(tǒng)不同。然而，所有形式驗證和綜合都與一個環(huán)境模型有關(guān)。因此，必須將有關(guān)輸入數(shù)據(jù)的假設(shè)和屬性解釋到環(huán)境模型中。我們將這種二分法提煉為 AI 系統(tǒng)環(huán)境建模的三個挑戰(zhàn)，并制定相應(yīng)的原則來解決這些挑戰(zhàn)。
2.1 建模不確定性
在形式驗證的傳統(tǒng)用法中，一種司空見慣的做法是將環(huán)境建模為受約束的非確定性過程，或者“干擾”。這種“過度近似”的環(huán)境建模能夠允許人們更為保守地捕捉環(huán)境的不確定性，而無需過于詳細的模型，這種模型的推理是很不高效的。然而，對于基于 AI 的自主性，純粹的非確定性建?？赡軙a(chǎn)生太多虛假的錯誤報告，從而使驗證過程在實踐中變得毫無用處。例如在對一輛自動駕駛汽車的周圍車輛行為的建模中，周圍車輛的行為多種多樣，如果采用純粹的非確定性建模，就考慮不到總是意外發(fā)生的事故。此外，許多 AI/ML 系統(tǒng)隱式或顯式地對來自環(huán)境的數(shù)據(jù)或行為做出分布假設(shè)，從而需要進行概率建模。由于很難準確地確定潛在的分布，所以不能假定生成的概率模型是完美的，并且必須在模型本身中對建模過程中的不確定性加以表征。
概率形式建模。為了應(yīng)對這一挑戰(zhàn)，我們建議使用結(jié)合概率建模和非確定性建模的形式。在能夠可靠地指定或估計概率分布的情況下，可以使用概率建模。在其他情況下，非確定性建?？捎糜趯Νh(huán)境行為進行過度近似。雖然諸如馬爾可夫決策過程之類的形式主義已經(jīng)提供了一種混合概率和非確定性的方法，但我們相信，更豐富的形式主義如概率規(guī)劃范式，可以提供一種更具表達力和程序化的方式來對環(huán)境進行建模。我們預(yù)測，在許多情況下，此類概率程序需要（部分地）從數(shù)據(jù)中進行學習或合成。此時，學習參數(shù)中的任何不確定性都必須傳播到系統(tǒng)的其余部分，并在概率模型中加以表示。例如，凸馬爾可夫決策過程提供了一種方法來表示學習轉(zhuǎn)變概率值的不確定性，并擴展了用于驗證和控制的算法來解釋這種不確定性。
2.2 未知的變量
在傳統(tǒng)的形式驗證領(lǐng)域如驗證設(shè)備驅(qū)動程序中，系統(tǒng) S 與其環(huán)境 E 之間的接口定義良好，E 只能通過該接口與 S 進行交互。對于基于 AI 的自主性而言，該接口是不完善的，它由傳感器和感知組件規(guī)定，這些組件只能部分且嘈雜地捕捉環(huán)境，而且無法捕捕捉 S 和 E 之間的所有交互。所有環(huán)境的變量（特征）都是已知的，更不用說被感知到的變量。即使在環(huán)境變量已知的受限場景中，也明顯缺乏有關(guān)其演變的信息，尤其是在設(shè)計的時候。此外，代表環(huán)境接口的激光雷達等傳感器建模也是一項重大的技術(shù)挑戰(zhàn)。
內(nèi)省環(huán)境建模。我們建議通過開發(fā)內(nèi)省的設(shè)計和驗證方法來解決這個問題，也就是說，在系統(tǒng) S 中進行內(nèi)省，來對關(guān)于環(huán)境 E 的假設(shè) A 進行算法上的識別，該假設(shè)足以保證滿足規(guī)范 Φ。理想情況下，A 必須是此類假設(shè)中最弱的一個，并且還必須足夠高效，以便在設(shè)計時生成、并在運行時監(jiān)控可用傳感器和有關(guān)環(huán)境的其他信息源，以及方便在假設(shè)被違反時可以采取緩解措施。此外，如果涉及人類操作員，人們可能希望 A 可以翻譯成可理解的解釋，也就是說 S 可以向人類“解釋”為什么它可能無法滿足規(guī)范 Φ。處理這些多重要求以及對良好傳感器模型的需求，使得內(nèi)省環(huán)境建模成為一個非常重要的問題。初步的工作表明，這種可監(jiān)控假設(shè)的提取在簡單的情況下是可行的，雖然需要做更多的工作才能讓它具有實用性。
2.3 模擬人類行為
對于許多 AI 系統(tǒng)，例如半自動駕駛汽車，人類代理是環(huán)境和系統(tǒng)的關(guān)鍵部分。關(guān)于人類的人工模型無法充分捕捉人類行為的可變性和不確定性。另一方面，用于建模人類行為的數(shù)據(jù)驅(qū)動方法可能對 ML 模型使用的特征的表達能力和數(shù)據(jù)質(zhì)量敏感。為了實現(xiàn)人類 AI 系統(tǒng)的高度保證，我們必須解決當前人類建模技術(shù)的局限性，并為其預(yù)測準確性和收斂性提供保障。
主動的數(shù)據(jù)驅(qū)動建模。我們相信，人類建模需要一種主動的數(shù)據(jù)驅(qū)動方法，模型結(jié)構(gòu)和以數(shù)學形式表示的特征適合使用形式方法。人類建模的一個關(guān)鍵部分是捕捉人類意圖。我們提出了一個三管齊下的方法：基于專家知識來定義模型的模板或特征，用離線學習來完成模型以供設(shè)計時使用，以及在運行時通過監(jiān)控和與環(huán)境交互來學習和更新環(huán)境模型。例如，已經(jīng)有研究表明，通過人類受試者實驗從駕駛模擬器收集的數(shù)據(jù)，可用于生成人類駕駛員的行為模型，這些模型可用于驗證和控制自動駕駛汽車。此外，計算機安全領(lǐng)域的對抗性訓練和攻擊技術(shù)可用于人類模型的主動學習，并可針對導致不安全行為的特定人類動作來進一步設(shè)計模型。這些技術(shù)可以幫助開發(fā) human-AI 系統(tǒng)的驗證算法。
形式化驗證嚴重依賴于形式化規(guī)范——即對系統(tǒng)應(yīng)該做什么的精確的數(shù)學陳述。即使在形式化方法已經(jīng)取得相當大成功的領(lǐng)域，提出高質(zhì)量的形式化規(guī)范也是一項挑戰(zhàn)，而 AI 系統(tǒng)尤其面臨著獨特的挑戰(zhàn)。
3.1 難以形式化的任務(wù)
圖 2 中 AEBS 控制器中的感知模塊必須檢測和分類對象，從而將車輛和行人與其他實體區(qū)分開來。在經(jīng)典的形式方法意義上，這個模塊的準確性要求對每種類型的道路使用者和對象進行形式定義，這是極其困難的。這種問題存在于這個感知模塊的所有實現(xiàn)中，而不僅僅出現(xiàn)在基于深度學習的方法中。其他涉及感知和交流的任務(wù)也會出現(xiàn)類似的問題，比如自然語言處理。那么，我們?nèi)绾螢檫@樣的模塊指定精度屬性呢？規(guī)范語言應(yīng)該是什么？我們可以使用哪些工具來構(gòu)建規(guī)范？
端到端/系統(tǒng)水平的規(guī)范（End-to-end/system-level specifications）。為了應(yīng)對上述挑戰(zhàn)，我們可以對這個問題稍加變通。與其直接對難以形式化的任務(wù)進行規(guī)范，不如首先專注于精確地指定 AI 系統(tǒng)的端到端行為。從這種系統(tǒng)水平的規(guī)范中，可以獲得對難以形式化的組件的輸入-輸出接口的約束。這些約束用作一個組件水平（component-level ）的規(guī)范，這個規(guī)范與整個 AI 系統(tǒng)的上下文相關(guān)。對于圖 2 中的 AEBS 示例，這涉及對屬性 Φ 的規(guī)定，該屬性即在運動過程中與任何對象都保持最小距離，從中我們可得出對 DNN 輸入空間的約束，在對抗分析中捕捉語義上有意義的輸入空間。
3.2 定量規(guī)范 vs. 布爾規(guī)范
傳統(tǒng)上，形式規(guī)范往往是布爾型的，它將給定的系統(tǒng)行為映射為“真”或“假”。然而，在 AI 和 ML 中，規(guī)范通常作為規(guī)范成本或獎勵的目標函數(shù)給出。此外，可能有多個目標，其中一些必須一起滿足，而另一些則可能需要在某些環(huán)境中相互權(quán)衡。統(tǒng)一布爾和定量兩種規(guī)范方法的最佳方式是什么？是否有能夠統(tǒng)一捕捉 AI 組件常見屬性（如魯棒性和公平性）的形式？
混合定量和布爾規(guī)范。布爾規(guī)范和定量規(guī)范都有其優(yōu)點：布爾規(guī)范更容易組合，但目標函數(shù)有助于用基于優(yōu)化的技術(shù)進行驗證和綜合，并定義更精細的屬性滿足粒度。彌補這一差距的一種方法是轉(zhuǎn)向定量規(guī)范語言，例如使用具有布爾和定量語義的邏輯（如度量時序邏輯），或?qū)⒆詣訖C與 RL 的獎勵函數(shù)相結(jié)合。另一種方法是將布爾和定量規(guī)范組合成一個通用的規(guī)范結(jié)構(gòu)，例如一本規(guī)則手冊 ，手冊中的規(guī)范可以按層次結(jié)構(gòu)進行組織、比較和匯總。有研究已經(jīng)確定了 AI 系統(tǒng)的幾類屬性，包括魯棒性、公平性、隱私性、問責性和透明度。研究者正在提出新的形式主義，將形式方法和 ML 的思想聯(lián)系起來，以對這些屬性的變體（如語義魯棒性）進行建模。
3.3 數(shù)據(jù) vs. 形式要求
“數(shù)據(jù)即規(guī)范”的觀點在機器學習中很常見。有限輸入集上標記的“真實”數(shù)據(jù)通常是關(guān)于正確行為的唯一規(guī)范。這與形式化方法非常不同，形式化方法通常以邏輯或自動機的形式給出，它定義了遍歷所有可能輸入的正確行為的集合。數(shù)據(jù)和規(guī)范之間的差距值得注意，尤其是當數(shù)據(jù)有限、有偏見或來自非專家時。我們需要技術(shù)來對數(shù)據(jù)的屬性進行形式化，包括在設(shè)計時可用的數(shù)據(jù)和尚未遇到的數(shù)據(jù)。
規(guī)范挖掘(Specification mining)。 為了彌合數(shù)據(jù)和形式規(guī)范之間的差距，我們建議使用算法從數(shù)據(jù)和其他觀察中來推斷規(guī)范——即所謂的規(guī)范挖掘技術(shù)。此類方法通?？捎糜?ML 組件，包括感知組件，因為在許多情況下，它不需要具有精確的規(guī)范或人類可讀的規(guī)范。我們還可以使用規(guī)范挖掘方法，從演示或更復雜的多個代理（人類和人工智能）之間的交互形式來推斷人類意圖和其他屬性。
在形式驗證的大多數(shù)傳統(tǒng)應(yīng)用中，系統(tǒng) S 在設(shè)計時是固定的且已知的，比如它可以是一個程序，或者一個用編程語言或硬件描述語言來描述的電路。系統(tǒng)建模問題主要涉及的，是通過抽象掉不相關(guān)的細節(jié)，來將 S 減小到更易于處理的大小。AI 系統(tǒng)給系統(tǒng)建模帶來了非常不同的挑戰(zhàn)，這主要源于機器學習的使用：
高維輸入空間
用于感知的 ML 組件通常在非常高維的輸入空間上運行。比如，一個輸入的RGB 圖像可以是 1000 x 600 像素，它包含256((1000x600x3)) 個元素，輸入通常就是這樣的高維向量流。盡管研究人員已經(jīng)對高維輸入空間（如在數(shù)字電路中）使用了形式化方法，但基于 ML 的感知輸入空間的性質(zhì)是不同的，它不完全是布爾值，而是混合的，包括離散變量和連續(xù)變量。
高維參數(shù)/狀態(tài)空間
深度神經(jīng)網(wǎng)絡(luò)等 ML 組件具有數(shù)千到數(shù)百萬個模型參數(shù)和原始組件。例如，圖 2 中使用的最先進的 DNN 有多達 6000 萬個參數(shù)和數(shù)十層組件。這就產(chǎn)生了巨大的驗證搜索空間，抽象過程需要非常仔細。
在線適應(yīng)和進化
一些學習系統(tǒng)如使用 RL 的機器人，會隨著它們遇到的新數(shù)據(jù)和新情況而發(fā)生進化。對于這樣的系統(tǒng)，設(shè)計時的驗證必須考慮系統(tǒng)行為的未來演變，或者隨著學習系統(tǒng)的發(fā)展逐步地在線執(zhí)行。
在上下文中建模系統(tǒng)
對于許多 AI/ML 組件，它們的規(guī)范僅僅由上下文來定義。例如，要驗證圖 2 中基于 DNN 的系統(tǒng)的安全性，就需要對環(huán)境進行建模。我們需要對 ML 組件及其上下文進行建模的技術(shù)，以便可以驗證在語義上有意義的屬性。
近年來，許多工作都專注于提高效率，來驗證 DNN 的魯棒性和輸入-輸出屬性。然而，這還不夠，我們還需要在以下三個方面取得進展：
自動抽象和高效表示
自動生成系統(tǒng)的抽象一直是形式方法的關(guān)鍵，它在將形式方法的范圍擴展到大型硬件和軟件系統(tǒng)方面發(fā)揮著至關(guān)重要的作用。為了解決基于 ML 的系統(tǒng)的超高維混合狀態(tài)空間和輸入空間方面的挑戰(zhàn)，我們需要開發(fā)有效的技術(shù)來將 ML 模型抽象為更易于形式分析的、更簡單的模型。一些有希望的方向包括：使用抽象解釋來分析 DNN，開發(fā)用于偽造有 ML 組件的網(wǎng)絡(luò)物理系統(tǒng)的抽象，以及設(shè)計用于驗證的新表示（比如星集）。
解釋與因果
如果學習者在其預(yù)測中附上關(guān)于預(yù)測是如何從數(shù)據(jù)和背景知識中產(chǎn)生的的解釋，那我們就可以簡化對學習系統(tǒng)進行建模的任務(wù)。這個想法并不新鮮，ML 社區(qū)已經(jīng)對諸如“基于解釋的泛化”等術(shù)語進行了研究，但是最近，人們正在對使用邏輯來解釋學習系統(tǒng)的輸出重新產(chǎn)生了興趣。解釋生成有助于在設(shè)計時調(diào)試設(shè)計和規(guī)范，并有助于合成魯棒的 AI 系統(tǒng)以在運行時提供保障。包含因果推理和反事實推理的 ML 還可以幫助生成用于形式方法的解釋。
語義特征空間
當生成的對抗性輸入和反例在所使用的 ML 模型的上下文中具有語義意義時，ML 模型的對抗性分析和形式驗證就更有意義。例如，針對汽車顏色或一天中時間的微小變化來分析 DNN 對象檢測器的技術(shù)，比向少量任意選擇的像素添加噪聲的技術(shù)更有用。當前，大多數(shù)的方法在這一點上都還達不到要求。我們需要語義對抗分析，即在ML 模型所屬系統(tǒng)的上下文中對它們進行分析。其中額的一個關(guān)鍵步驟，是表示對 ML 系統(tǒng)運行的環(huán)境建模的語義特征空間，而不是為 ML 模型定義輸入空間的具體特征空間。這是符合直覺的，即與完整的具體特征空間相比，具體特征空間在語義上有意義的部分（如交通場景圖像）所形成的潛在空間要低得多。圖 2 中的語義特征空間是代表自動駕駛汽車周圍 3D 世界的低維空間，而具體的特征空間是高維像素空間。由于語義特征空間的維數(shù)較低，因此可以更容易地進行搜索。但是，我們還需要一個“渲染器”，將語義特征空間中的一個點映射到具體特征空間中的一個點。渲染器的屬性如可微性（differentiability），可以更容易地應(yīng)用形式化方法來執(zhí)行語義特征空間的目標導向搜索。
硬件和軟件系統(tǒng)形式化方法的有效性，是由底層“計算引擎”的進步推動的——例如，布爾可滿足性求解 (SAT)、可滿足性模理論 (SMT) 和模型檢查。鑒于 AI/ML 系統(tǒng)規(guī)模、環(huán)境復雜性和所涉及的新型規(guī)范，需要一類新的計算引擎來進行高效且可擴展的訓練、測試、設(shè)計和驗證，實現(xiàn)這些進步必須克服的關(guān)鍵挑戰(zhàn)。
5.1 數(shù)據(jù)集設(shè)計
數(shù)據(jù)是機器學習的基本起點，提高 ML 系統(tǒng)質(zhì)量就必須提高它所學習數(shù)據(jù)的質(zhì)量。形式化方法如何幫助 ML 數(shù)據(jù)系統(tǒng)地選擇、設(shè)計和擴充？
ML 的數(shù)據(jù)生成與硬件和軟件的測試生成問題有相似之處。形式化方法已被證明對系統(tǒng)的、基于約束的測試生成是有效的，但這與對人工智能系統(tǒng)的要求不同，約束類型可能要復雜得多——例如，對使用傳感器從復雜環(huán)境（如交通狀況）捕獲的數(shù)據(jù)的“真實性”進行編碼要求。我們不僅需要生成具有特定特征的數(shù)據(jù)項（如發(fā)現(xiàn)錯誤的測試），還需要生成滿足分布約束的集合；數(shù)據(jù)生成必須滿足數(shù)據(jù)集大小和多樣性的目標，以進行有效的訓練和泛化。這些要求都需要開發(fā)一套新的形式化技術(shù)。
形式方法中的受控隨機化。數(shù)據(jù)集設(shè)計的這個問題有很多方面，首先必須定義“合法”輸入的空間，以便根據(jù)應(yīng)用程序語義正確形成示例；其次，需要捕獲與現(xiàn)實世界數(shù)據(jù)相似性度量的約束；第三，通常需要對生成的示例的分布進行約束，以獲得學習算法收斂到真實概念的保證。
我們相信這些方面可以通過隨機形式方法來解決——用于生成受形式約束和分布要求的數(shù)據(jù)的隨機算法。一類稱為控制即興創(chuàng)作的新技術(shù)是很有前景的，即興創(chuàng)作的生成要滿足三個約束的隨機字符串（示例）x：
定義合法x空間的硬約束
一個軟約束，定義生成的x必須如何與真實世界的示例相似
定義輸出分布約束的隨機性要求
目前，控制即興理論仍處于起步階段，我們才剛剛開始了解計算復雜性并設(shè)計有效的算法。反過來，即興創(chuàng)作依賴于計算問題的最新進展，例如約束隨機抽樣、模型計數(shù)和基于概率編程的生成方法。
5.2 定量驗證
除了通過傳統(tǒng)指標（狀態(tài)空間維度、組件數(shù)量等）衡量AI 系統(tǒng)規(guī)模之外，組件的類型可能要復雜得多。例如，自主和半自主車輛及其控制器必須建模為混合動力系統(tǒng)，結(jié)合離散和連續(xù)動力學；此外，環(huán)境中的代表（人類、其他車輛）可能需要建模為概率過程。最后，需求可能不僅涉及傳統(tǒng)關(guān)于安全性和活性的布爾規(guī)范，還包括對系統(tǒng)魯棒性和性能的定量要求，然而大多數(shù)現(xiàn)有的驗證方法，都是針對回答布爾驗證問題。為了解決這一差距，必須開發(fā)用于定量驗證的新可擴展引擎。
定量語義分析。一般來說，人工智能系統(tǒng)的復雜性和異構(gòu)性意味著，規(guī)范的形式驗證（布爾或定量）是不可判定的——例如，即便是確定線性混合系統(tǒng)的狀態(tài)是否可達，也是不可判定的。為了克服計算復雜性帶來的這一障礙，人們必須在語義特征空間上使用概率和定量驗證的新技術(shù)，以增強本節(jié)前面討論的抽象和建模方法。對于同時具有布爾和定量語義的規(guī)范形式，在諸如度量時間邏輯之類的形式中，將驗證表述為優(yōu)化，對于統(tǒng)一來自形式方法的計算方法和來自優(yōu)化文獻的計算方法至關(guān)重要。例如在基于模擬的時間邏輯證偽中，盡管它們必須應(yīng)用于語義特征空間以提高效率，這種偽造技術(shù)也可用于系統(tǒng)地、對抗性地生成 ML 組件的訓練數(shù)據(jù)。概率驗證的技術(shù)應(yīng)該超越傳統(tǒng)的形式，如馬爾科夫鏈或MDPs，以驗證語義特征空間上的概率程序。同樣，關(guān)于SMT求解的工作必須擴展到更有效地處理成本約束--換句話說，將SMT求解與優(yōu)化方法相結(jié)合。
5.3 AI/ML 的組合推理
對于擴展到大型系統(tǒng)的正式方法，組合（模塊化）推理是必不可少的。在組合驗證中，一個大型系統(tǒng)（例如，程序）被拆分為它的組件（例如，程序），每個組件都根據(jù)規(guī)范進行驗證，然后組件規(guī)范一起產(chǎn)生系統(tǒng)級規(guī)范。組合驗證的一個常見方法是使用假設(shè)-保證合同，例如一個過程假設(shè)一些關(guān)于它的開始狀態(tài)（前置條件），反過來又保證其結(jié)束狀態(tài)（后置條件），類似的假設(shè)-保證范式已被開發(fā)并應(yīng)用于并發(fā)的軟件和硬件系統(tǒng)。
然而，這些范式并不涵蓋人工智能系統(tǒng)，這在很大程度上是由于 "形式化規(guī)范 "一節(jié)中討論的人工智能系統(tǒng)的規(guī)范化挑戰(zhàn)。組合式驗證需要組合式規(guī)范——也就是說，組件必須是可形式化的。然而，正如“形式化規(guī)范”中所述，可能無法正式指定一個感知組件的正確行為。因此，挑戰(zhàn)之一就是開發(fā)不依賴于有完整組合規(guī)范的組合推理技術(shù)。此外，人工智能系統(tǒng)的定量和概率性質(zhì)，要求將組合推理的理論擴展到定量系統(tǒng)和規(guī)范。
推斷組件合同。人工智能系統(tǒng)的組合式設(shè)計和分析需要在多個方面取得進展。首先，需要在一些有前景的初步工作基礎(chǔ)上，為這些系統(tǒng)的語義空間開發(fā)概率保證設(shè)計和驗證的理論。第二，必須設(shè)計出新的歸納綜合技術(shù)，以算法方式生成假設(shè)-保證合同，減少規(guī)范負擔并促進組合推理。第三，為了處理諸如感知等沒有精確正式規(guī)格的組件的情況，我們提出了從系統(tǒng)級分析中推斷組件級約束的技術(shù)，并使用這種約束將組件級分析，包括對抗性分析，集中在搜索輸入空間的 "相關(guān) "部分。
在理想的世界中，驗證將與設(shè)計過程相結(jié)合，因此系統(tǒng)是“在建構(gòu)中修正的”。例如，驗證可以與編譯/合成步驟交錯進行，假設(shè)在集成電路中常見的寄存器傳輸級（RTL）設(shè)計流程中，或許它可以被集成到合成算法中，以確保實現(xiàn)滿足規(guī)范。我們能不能為人工智能系統(tǒng)設(shè)計一個合適的在建構(gòu)中逐步修正的設(shè)計流程？
6.1 ML 組件的規(guī)范驅(qū)動設(shè)計
給定一個正式的規(guī)范，我們能否設(shè)計一個可證明滿足該規(guī)范的機器學習組件（模型）？這種全新的 ML 組件設(shè)計有很多方面：（1）設(shè)計數(shù)據(jù)集，（2） 綜合模型的結(jié)構(gòu)，（3）生成一組有代表性的特征，（4） 綜合超參數(shù)和 ML 算法選擇的其他方面，以及（5）在綜合失敗時自動化調(diào)試 ML 模型或規(guī)范的技術(shù)。
ML 組件的正式合成。解決前面所列出一些問題的解決方案正在出現(xiàn)，可以使用語義損失函數(shù)或通過認證的魯棒性在 ML 模型上強制執(zhí)行屬性，這些技術(shù)可以與神經(jīng)架構(gòu)搜索等方法相結(jié)合，以生成正確構(gòu)建的 DNN。另一種方法是基于新興的形式歸納綜合理論，即從滿足形式化規(guī)范的程序?qū)嵗羞M行綜合。解決形式歸納綜合問題的最常見方法是使用 oracle-guided 方法，其中將學習者與回答查詢的 oracle 配對；如示例中圖2，oracle 可以是一個偽造者，它生成反例，顯示學習組件的故障如何違反系統(tǒng)級規(guī)范。最后，使用定理證明來確保用于訓練 ML 模型的算法的正確性，也是朝著建構(gòu)修正的 ML 組件邁出的重要一步。
6.2 基于機器學習的系統(tǒng)設(shè)計
第二個挑戰(zhàn)，是設(shè)計一個包含學習和非學習組件的整體系統(tǒng)。目前已經(jīng)出現(xiàn)的幾個研究問題：我們能否計算出可以限制 ML 組件運行的安全范圍？我們能否設(shè)計一種控制或規(guī)劃算法來克服它接收輸入的基于 ML 感知組件的限制？我們可以為人工智能系統(tǒng)設(shè)計組合設(shè)計理論嗎？當兩個 ML 模型用于感知兩種不同類型的傳感器數(shù)據(jù)（例如，LiDAR 和視覺圖像），并且每個模型在某些假設(shè)下都滿足其規(guī)范，那么二者在什么條件下可以一起使用、以提高可靠性整體系統(tǒng)？
在這一挑戰(zhàn)上，取得進展的一個突出例子是基于安全學習的控制的工作。這種方法預(yù)先計算了一個安全包絡(luò)線，并使用學習算法在該包絡(luò)線內(nèi)調(diào)整控制器，需要基于例如可達性分析、來有效計算此類安全包絡(luò)的技術(shù)；同樣，安全 RL 領(lǐng)域也取得了顯著進展。
然而，這些并沒有完全解決機器學習對感知和預(yù)測帶來的挑戰(zhàn)——例如，可證明安全的端到端深度強化學習尚未實現(xiàn)。
6.3 為彈性 AI 橋接設(shè)計時間和運行時間
正如“環(huán)境建模”部分所討論的那樣，許多 AI 系統(tǒng)在無法先驗指定的環(huán)境中運行，因此總會有無法保證正確性的環(huán)境。在運行時實現(xiàn)容錯和錯誤恢復的技術(shù)，對人工智能系統(tǒng)具有重要作用。我們需要系統(tǒng)地理解在設(shè)計時可以保證什么，設(shè)計過程如何有助于人工智能系統(tǒng)在運行時的安全和正確運行，以及設(shè)計時和運行時技術(shù)如何有效地互操作。
對此，關(guān)于容錯和可靠系統(tǒng)的文獻為我們提供了開發(fā)運行時保證技術(shù)的基礎(chǔ)——即運行時驗證和緩解技術(shù)；例如 Simplex 方法，就提供了一種將復雜但容易出錯的模塊與安全的、正式驗證的備份模塊相結(jié)合的方法。最近，結(jié)合設(shè)計時和運行時保證方法的技術(shù)顯示了未驗證的組件、包括那些基于人工智能和 ML 的組件，可以被包裹在運行時保證框架中，以提供安全運行的保證。但目前這些僅限于特定類別的系統(tǒng)，或者它們需要手動設(shè)計運行時監(jiān)視器和緩解策略，在諸如內(nèi)省環(huán)境建模、人工智能的監(jiān)測器和安全回退策略的合成等方法上，還有更多的工作需要做。
此處討論的建構(gòu)中修正智能系統(tǒng)的設(shè)計方法可能會引入開銷，使其更難以滿足性能和實時要求。但我們相信（也許是非直覺的），在以下意義上，形式化方法甚至可以幫助提高系統(tǒng)的性能或能源效率。
傳統(tǒng)的性能調(diào)優(yōu)往往與上下文無關(guān)——例如，任務(wù)需要獨立于它們運行的環(huán)境來滿足最后期限。但如果設(shè)計時就對這些環(huán)境進行正式表征，并在運行時對其進行監(jiān)控，如果其系統(tǒng)運行經(jīng)過正式驗證是安全的，那么在這種環(huán)境下，ML 模型就可以用準確性來換取更高的效率。這種權(quán)衡可能是未來研究的一個富有成果的領(lǐng)域。
從形式化方法的角度來看，我們剖析了設(shè)計高保證人工智能系統(tǒng)的問題。如圖3所示，我們確定了將形式化方法應(yīng)用于 AI 系統(tǒng)的五個主要挑戰(zhàn)，并對這五項挑戰(zhàn)中的每一項都制定了三項設(shè)計和驗證原則，這些原則有希望解決這個挑戰(zhàn)。
圖 3 中的邊顯示了這些原則之間的依賴關(guān)系，例如運行時保證依賴于自省和數(shù)據(jù)驅(qū)動的環(huán)境建模，以提取可監(jiān)測的假設(shè)和環(huán)境模型。同樣，為了進行系統(tǒng)級分析，我們需要進行組合推理和抽象，其中一些 AI 組件可能需要挖掘規(guī)范，而其他組件則通過形式化的歸納綜合構(gòu)建生成正確的結(jié)構(gòu)。
自 2016 年以來，包括作者在內(nèi)的幾位研究人員一直致力于應(yīng)對這些挑戰(zhàn)，當時本文已發(fā)表的原始版本介紹了一些樣本進展。我們已經(jīng)開發(fā)了開源工具 VerifAI 和 Scenic，它們實現(xiàn)了基于本文所述原則的技術(shù)，并已應(yīng)用于自動駕駛和航空航天領(lǐng)域的工業(yè)規(guī)模系統(tǒng)。這些成果只是一個開始，還有很多事情要做。在未來的幾年里，可驗證 AI 有望繼續(xù)成為一個富有成效的研究領(lǐng)域。
原文鏈接：https://cacm.acm.org/magazines/2022/7/262079-toward-verified-artificial-intelligence/fulltext
雷峰網(wǎng)版權(quán)文章，未經(jīng)授權(quán)禁止轉(zhuǎn)載。詳情見轉(zhuǎn)載須知。
