邁向可驗證的 AI：形式化方法的五大挑戰

人工智慧試圖模仿人類智慧的運算系統，包括人類一些與智慧有直覺聯繫的功能，例如學習、解決問題以及理性地思考和行動。在廣義地解釋上，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 有多達 6,000 萬個參數和數十層組件。這就產生了巨大的驗證搜尋空間，抽象過程需要非常仔細。

#

線上適應與演化

一些學習系統如使用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 有望繼續成為一個富有成效的研究領域。

#

以上是邁向可驗證的 AI：形式化方法的五大挑戰的詳細內容。更多資訊請關注PHP中文網其他相關文章！