人工智能試圖模仿人類智能的計算系統，包括人類一些與智能具有直觀聯系的功能，例如學習、解決問題以及理性地思考和行動。在廣義地解釋上，AI 一詞涵蓋了許多密切相關的領域如機器學習。那些大量使用 AI 的系統在醫療保健、交通運輸、金融、社交網絡、電子商務和教育等領域都產生了重大的社會影響。

這種日益增長的社會影響，也帶來了一系列風險和擔憂，包括人工智能軟件中的錯誤、網絡攻擊和人工智能系統安全等方面。因此，AI 系統的驗證問題以及更廣泛的可信 AI 的話題已經開始引起研究界的關注。“可驗證 AI”已經被確立為設計 AI 系統的目標，一個可驗證的 AI 系統在特定的數學要求上具有強大的、理想情況下可證明的正確性保證。我們怎樣才能實現這個目標？

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

在計算機科學和工程領域，形式方法涉及系統的嚴格的數學規范、設計和驗證。其核心在于，形式方法是關于證明的：制定形成證明義務的規范，設計系統以履行這些義務，并通過算法證明搜索來驗證系統確實符合其規范。從規范驅動的測試和仿真到模型檢查和定理證明，一系列的形式化方法常被用于集成電路的計算機輔助設計，并已廣泛被用于發現軟件中的錯誤，分析網絡物理系統，并發現安全漏洞。

本文回顧了形式化方法傳統的應用方式，指明了形式化方法在 AI 系統中的五個獨特挑戰，包括：

• 開發關于環境的語言、算法
• 對復雜 ML 組件和系統進行抽象和表示
• 為 AI 系統和數據提出新的規范形式化方法和屬性
• 開發針對自動推理的可擴展計算引擎
• 開發針對建構中可信（trustworthy-by-construction）設計的算法和技術

在討論最新進展的基礎上，作者提出了解決以上挑戰的原則。本文不僅僅關注特定類型的 AI 組件如深度神經網絡，或特定的方法如強化學習，而是試圖涵蓋更廣泛的 AI 系統及其設計過程。此外，形式化方法只是通往可信 AI 的其中一種途徑，所以本文的觀點旨在對來自其他領域的方法加以補充。這些觀點很大程度上來源于對自主和半自主系統中使用 AI 所產生的問題的思考，在這些系統中，安全性和驗證性問題更加突出。

概述

圖 1 顯示了形式驗證、形式綜合和形式指導的運行時彈性的典型過程。形式驗證過程從三個輸入開始：

圖 1 ：用于驗證、綜合和運行時彈性的形式化方法

1. 要驗證的系統模型 S
2. 環境模型 E
3. 待驗證的屬性 Φ

驗證者生成“是”或“否”的答案作為輸出，來表明 S 是否滿足環境 E 中的屬性 Φ。通常，“否”輸出伴隨著反例，也稱為錯誤跟蹤（error trace），它是對系統的執行，表明 Φ 是如何被偽造的。一些驗證工具還包括帶有“是”答案的正確性證明或證書。我們對形式方法采取一種廣泛的視角，包括使用形式規范、驗證或綜合的某些方面的任何技術。例如，我們囊括了基于仿真的硬件驗證方法或基于模型的軟件測試方法，因為它們也使用正式的規范或模型來指導仿真或測試的過程。

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

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

圖 2：包含機器學習組件的閉環 CPS 示例

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

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

圖 3：可驗證 AI 的 5 個挑戰領域總結

環境建模

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

2.1 建模不確定性?

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

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

2.2 未知的變量?

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

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

2.3 模擬人類行為?

對于許多 AI 系統，例如半自動駕駛汽車，人類代理是環境和系統的關鍵部分。關于人類的人工模型無法充分捕捉人類行為的可變性和不確定性。另一方面，用于建模人類行為的數據驅動方法可能對 ML 模型使用的特征的表達能力和數據質量敏感。為了實現人類 AI 系統的高度保證，我們必須解決當前人類建模技術的局限性，并為其預測準確性和收斂性提供保障。

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

形式化規范

形式化驗證嚴重依賴于形式化規范——即對系統應該做什么的精確的數學陳述。即使在形式化方法已經取得相當大成功的領域，提出高質量的形式化規范也是一項挑戰，而 AI 系統尤其面臨著獨特的挑戰。

3.1 難以形式化的任務?

圖 2 中 AEBS 控制器中的感知模塊必須檢測和分類對象，從而將車輛和行人與其他實體區分開來。在經典的形式方法意義上，這個模塊的準確性要求對每種類型的道路使用者和對象進行形式定義，這是極其困難的。這種問題存在于這個感知模塊的所有實現中，而不僅僅出現在基于深度學習的方法中。其他涉及感知和交流的任務也會出現類似的問題，比如自然語言處理。那么，我們如何為這樣的模塊指定精度屬性呢？規范語言應該是什么？我們可以使用哪些工具來構建規范？

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

3.2 定量規范 vs. 布爾規范?

傳統上，形式規范往往是布爾型的，它將給定的系統行為映射為“真”或“假”。然而，在 AI 和 ML 中，規范通常作為規范成本或獎勵的目標函數給出。此外，可能有多個目標，其中一些必須一起滿足，而另一些則可能需要在某些環境中相互權衡。統一布爾和定量兩種規范方法的最佳方式是什么？是否有能夠統一捕捉 AI 組件常見屬性（如魯棒性和公平性）的形式？

混合定量和布爾規范。布爾規范和定量規范都有其優點：布爾規范更容易組合，但目標函數有助于用基于優化的技術進行驗證和綜合，并定義更精細的屬性滿足粒度。彌補這一差距的一種方法是轉向定量規范語言，例如使用具有布爾和定量語義的邏輯（如度量時序邏輯），或將自動機與 RL 的獎勵函數相結合。另一種方法是將布爾和定量規范組合成一個通用的規范結構，例如一本規則手冊 ，手冊中的規范可以按層次結構進行組織、比較和匯總。有研究已經確定了 AI 系統的幾類屬性，包括魯棒性、公平性、隱私性、問責性和透明度。研究者正在提出新的形式主義，將形式方法和 ML 的思想聯系起來，以對這些屬性的變體（如語義魯棒性）進行建模。

3.3 數據 vs. 形式要求?

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

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

學習系統的建模

在形式驗證的大多數傳統應用中，系統 S 在設計時是固定的且已知的，比如它可以是一個程序，或者一個用編程語言或硬件描述語言來描述的電路。系統建模問題主要涉及的，是通過抽象掉不相關的細節，來將 S 減小到更易于處理的大小。AI 系統給系統建模帶來了非常不同的挑戰，這主要源于機器學習的使用：

高維輸入空間?

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

高維參數/狀態空間?

深度神經網絡等 ML 組件具有數千到數百萬個模型參數和原始組件。例如，圖 2 中使用的最先進的 DNN 有多達 6000 萬個參數和數十層組件。這就產生了巨大的驗證搜索空間，抽象過程需要非常仔細。

在線適應和進化?

一些學習系統如使用 RL 的機器人，會隨著它們遇到的新數據和新情況而發生進化。對于這樣的系統，設計時的驗證必須考慮系統行為的未來演變，或者隨著學習系統的發展逐步地在線執行。

在上下文中建模系統?

對于許多 AI/ML 組件，它們的規范僅僅由上下文來定義。例如，要驗證圖 2 中基于 DNN 的系統的安全性，就需要對環境進行建模。我們需要對 ML 組件及其上下文進行建模的技術，以便可以驗證在語義上有意義的屬性。

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

自動抽象和高效表示?

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

解釋與因果

如果學習者在其預測中附上關于預測是如何從數據和背景知識中產生的的解釋，那我們就可以簡化對學習系統進行建模的任務。這個想法并不新鮮，ML 社區已經對諸如“基于解釋的泛化”等術語進行了研究，但是最近，人們正在對使用邏輯來解釋學習系統的輸出重新產生了興趣。解釋生成有助于在設計時調試設計和規范，并有助于合成魯棒的 AI 系統以在運行時提供保障。包含因果推理和反事實推理的 ML  還可以幫助生成用于形式方法的解釋。

語義特征空間?

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

用于設計和驗證的計算引擎

硬件和軟件系統形式化方法的有效性，是由底層“計算引擎”的進步推動的——例如，布爾可滿足性求解 (SAT)、可滿足性模理論 (SMT) 和模型檢查。鑒于 AI/ML 系統規模、環境復雜性和所涉及的新型規范，需要一類新的計算引擎來進行高效且可擴展的訓練、測試、設計和驗證，實現這些進步必須克服的關鍵挑戰。

5.1 數據集設計?

數據是機器學習的基本起點，提高 ML 系統質量就必須提高它所學習數據的質量。形式化方法如何幫助 ML 數據系統地選擇、設計和擴充？

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

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

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

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

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

5.2 定量驗證?

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

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

我們需要了解在設計時可以保證什么，設計過程如何有助于運行時的安全操作，以及設計時和運行時技術如何有效地互操作。

5.3 AI/ML 的組合推理?

對于擴展到大型系統的正式方法，組合（模塊化）推理是必不可少的。在組合驗證中，一個大型系統（例如，程序）被拆分為它的組件（例如，程序），每個組件都根據規范進行驗證，然后組件規范一起產生系統級規范。組合驗證的一個常見方法是使用假設-保證合同，例如一個過程假設一些關于它的開始狀態（前置條件），反過來又保證其結束狀態（后置條件），類似的假設-保證范式已被開發并應用于并發的軟件和硬件系統。

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

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

建構中修正智能系統

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

6.1 ML 組件的規范驅動設計

給定一個正式的規范，我們能否設計一個可證明滿足該規范的機器學習組件（模型）？這種全新的 ML 組件設計有很多方面：（1）設計數據集，（2） 綜合模型的結構，（3）生成一組有代表性的特征，（4） 綜合超參數和 ML 算法選擇的其他方面，以及（5）在綜合失敗時自動化調試 ML 模型或規范的技術。

ML 組件的正式合成。解決前面所列出一些問題的解決方案正在出現，可以使用語義損失函數或通過認證的魯棒性在 ML 模型上強制執行屬性，這些技術可以與神經架構搜索等方法相結合，以生成正確構建的 DNN。另一種方法是基于新興的形式歸納綜合理論，即從滿足形式化規范的程序實例中進行綜合。解決形式歸納綜合問題的最常見方法是使用 oracle-guided 方法，其中將學習者與回答查詢的 oracle 配對；如示例中圖2，oracle 可以是一個偽造者，它生成反例，顯示學習組件的故障如何違反系統級規范。最后，使用定理證明來確保用于訓練 ML 模型的算法的正確性，也是朝著建構修正的 ML 組件邁出的重要一步。

6.2 基于機器學習的系統設計?

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

在這一挑戰上，取得進展的一個突出例子是基于安全學習的控制的工作。這種方法預先計算了一個安全包絡線，并使用學習算法在該包絡線內調整控制器，需要基于例如可達性分析、來有效計算此類安全包絡的技術；同樣，安全 RL 領域也取得了顯著進展。

然而，這些并沒有完全解決機器學習對感知和預測帶來的挑戰——例如，可證明安全的端到端深度強化學習尚未實現。

6.3 為彈性 AI 橋接設計時間和運行時間?

正如“環境建模”部分所討論的那樣，許多 AI 系統在無法先驗指定的環境中運行，因此總會有無法保證正確性的環境。在運行時實現容錯和錯誤恢復的技術，對人工智能系統具有重要作用。我們需要系統地理解在設計時可以保證什么，設計過程如何有助于人工智能系統在運行時的安全和正確運行，以及設計時和運行時技術如何有效地互操作。

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

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

傳統的性能調優往往與上下文無關——例如，任務需要獨立于它們運行的環境來滿足最后期限。但如果設計時就對這些環境進行正式表征，并在運行時對其進行監控，如果其系統運行經過正式驗證是安全的，那么在這種環境下，ML 模型就可以用準確性來換取更高的效率。這種權衡可能是未來研究的一個富有成果的領域。

結論

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

圖 3 中的邊顯示了這些原則之間的依賴關系，例如運行時保證依賴于自省和數據驅動的環境建模，以提取可監測的假設和環境模型。同樣，為了進行系統級分析，我們需要進行組合推理和抽象，其中一些 AI 組件可能需要挖掘規范，而其他組件則通過形式化的歸納綜合構建生成正確的結構。

自 2016 年以來，包括作者在內的幾位研究人員一直致力于應對這些挑戰，當時本文已發表的原始版本介紹了一些樣本進展。我們已經開發了開源工具 VerifAI 和 Scenic，它們實現了基于本文所述原則的技術，并已應用于自動駕駛和航空航天領域的工業規模系統。這些成果只是一個開始，還有很多事情要做。在未來的幾年里，可驗證 AI 有望繼續成為一個富有成效的研究領域。