0
| 本文作者： 我在思考中 | 2021-10-12 10:12 |
編譯 | 杏花
對于某些任務，人工智能系統(tǒng)已經(jīng)取得足夠好的表現(xiàn)，可以部署在我們的道路和家里。比如，物體識別可以幫助汽車識別道路；語音識別則有助于個性化語音助手（如Siri和Alexa）交流。對于其他任務，人工智能系統(tǒng)的表現(xiàn)甚至超過了人類，AlphaGo 就是第一個擊敗世界最強圍棋選手的計算機程序。
人工智能的前景廣闊。它們將開我們的車，它們將幫助醫(yī)生更準確地診斷疾病，它們將幫助法官做出更加一致的法庭裁決，它們將幫助雇主聘用更合適的求職者。
然而，我們也知道這些人工智能系統(tǒng)可能是不堪一擊且不公正的。在停車標志上涂鴉可以騙過分類器使其認為這不是停車標志。向良性皮膚病變的圖像中加入噪音也會欺騙分類器，使其誤以為是惡性的。美國法院使用的風險評估工具已被證明對黑人持有偏見，企業(yè)的招聘工具也被證明歧視女性。
那么，我們?nèi)绾尾拍軆冬F(xiàn)人工智能帶來好處的承諾，同時解決這些對人類和社會來說生死攸關的情況呢？簡而言之，我們怎樣才能實現(xiàn)可信AI？
本文的最終目的是團結(jié)計算機社區(qū)，通過來自多個研究社區(qū)和利益相關者的專業(yè)知識和情感，來支持一個關于可信AI的廣泛且長期的研究項目。本文側(cè)重于解決三個關鍵研究社區(qū)的問題，原因如下：可信AI在可信計算的基礎上增加了新的所需屬性；人工智能系統(tǒng)需要新的形式和技術，尤其是數(shù)據(jù)的使用提出了全新的研究問題；人工智能系統(tǒng)可能會受益于對確保可信度的正式方法的審查。通過將可信計算、形式方法和人工智能領域的研究人員聚集在一起，我們的目標是在可信AI領域內(nèi)培育一個跨學術界、產(chǎn)業(yè)界和政府的新型研究社區(qū)。
周以真（英文名Jeannette M. Wing），美國計算機科學家，曾任卡內(nèi)基-梅隆大學教授。美國國家自然基金會計算與信息科學工程部助理部長。ACM和IEEE會士。她的主要研究領域是形式方法、可信計算、分布式系統(tǒng)、編程語言等。現(xiàn)為哥倫比亞大學數(shù)據(jù)科學研究院主任、計算機科學教授，其長期研究興趣主要集中于網(wǎng)絡安全、數(shù)據(jù)隱私以及人工智能。
具有里程碑意義的1999年國家科學院網(wǎng)絡空間信任（Trust in Cyberspace 1999 National Academies）報告奠定了可信計算的基礎，此后，可信計算持續(xù)成為一個活躍的研究領域。
大約在同一時期，美國國家科學基金會（National Science Foundation）啟動了一系列關于信任的項目。從始于2001年的可信計算（Trusted Computing）為起點，到2004年的網(wǎng)絡信任（Cyber Trust），再到2007年的可信賴計算（Trustworthy Computing），以及2011年的安全可信的網(wǎng)絡空間（Secure and Trustworthy Cyberspace），計算機和信息科學與工程理事會（Computer and Information Science and Engineering Directorate）已經(jīng)發(fā)展成可信計算的學術研究社區(qū)。雖然它源于計算機科學社區(qū)，但現(xiàn)在支持可信計算的研究已跨越了美國國家科學基金會的多個部門，并涉及許多其他資助組織，包括通過網(wǎng)絡和信息技術研究與發(fā)展（NITRD）計劃和20個聯(lián)邦機構。
產(chǎn)業(yè)界也一直是可信計算的領導者和積極參與者。在比爾·蓋茨2002年1月的“可信計算（Trustworthy Computing）”備忘錄中，微軟向它的員工、客戶、股東和其他信息技術部門傳達了可信軟件和硬件產(chǎn)品的重要性。它提到了微軟內(nèi)部的一份白皮書，該白皮書確定了信任的四個支柱：安全、隱私、可靠和商業(yè)誠信。
經(jīng)過 20 年的投資和研發(fā)進步，“可信”已經(jīng)意味著一組（重疊的）屬性：
可靠性：系統(tǒng)做正確的事情嗎？
安全性：系統(tǒng)沒有危害嗎？
保密性：系統(tǒng)是否容易受到攻擊？
隱私性：系統(tǒng)是否保護個人的身份和數(shù)據(jù)?
可用性：當人類需要訪問系統(tǒng)時，系統(tǒng)是正常的嗎？
實用性：人類可以輕松使用它嗎?
我們希望這些屬性存在于硬件和軟件等計算系統(tǒng)中，以及存在于這些系統(tǒng)與人類和物理世界的交互。在過去的幾十年里，學術界和產(chǎn)業(yè)界在可信計算方面取得了巨大的進步。然而，隨著技術的進步和對手變得越來越復雜，可信計算仍然是一個艱難的夢想。
人工智能系統(tǒng)在利益屬性方面提高了標準。除了與可信計算相關的屬性(如前所述)，我們還需要(重疊的)屬性，例如：
準確性：與訓練和測試過的數(shù)據(jù)相比，人工智能系統(tǒng)在新的（不可見的）數(shù)據(jù)上表現(xiàn)如何?
魯棒性：系統(tǒng)的結(jié)果對輸入的變化有多敏感?
公平性：系統(tǒng)的結(jié)果是否公正?
問責制：什么人或什么物對系統(tǒng)的結(jié)果負責?
透明度：外部觀察員是否清楚系統(tǒng)的結(jié)果是如何產(chǎn)生的?
可理解性/可解釋性：系統(tǒng)的結(jié)果是否可以通過人類可以理解和/或?qū)ψ罱K用戶有意義的解釋來證明？
......和其他尚未確定的屬性。
機器學習社區(qū)將準確性視為黃金標準，但可信AI要求我們在這些屬性之間進行權衡。比如，我們也許愿意為了部署一個更公平的模型而舍棄一些準確性。此外，上述的某些屬性可能有不同的解釋，最終導致不同的形式。例如，有許多合理的公平概念，包括人口平等、機會均等和個人公平等等，這其中的一些概念彼此并不相容。
傳統(tǒng)的軟件和硬件系統(tǒng)由于其規(guī)模和組件之間的交互數(shù)量而變得復雜。在大多數(shù)情況下，我們可以根據(jù)離散邏輯和確定性狀態(tài)機來定義它們的行為。
今天的人工智能系統(tǒng)，尤其是那些使用深度神經(jīng)網(wǎng)絡的系統(tǒng)，給傳統(tǒng)的計算機系統(tǒng)增加了一個復雜的維度。這種復雜性是由于它們固有的概率性質(zhì)。通過概率，人工智能系統(tǒng)對人類行為和物理世界的不確定性進行建模。更多機器學習的最新進展依賴于大數(shù)據(jù)，這增加了它們的概率性質(zhì)，因為來自現(xiàn)實世界的數(shù)據(jù)只是概率空間中的點。因此，可信AI必然會將我們的注意力從傳統(tǒng)計算系統(tǒng)的主要確定性本質(zhì)轉(zhuǎn)向人工智能系統(tǒng)的概率本質(zhì)。
從驗證到信任
我們?nèi)绾卧O計、執(zhí)行和部署人工智能系統(tǒng)，使其值得信賴?
在計算系統(tǒng)中建立最終用戶信任的一種方法是形式驗證，其中屬性在一個大域中得到一勞永逸的證明，例如，對一個程序的所有輸入或者對于并發(fā)或分布式系統(tǒng)的所有行為。或者，驗證過程識別出的反例，例如，一個輸入值，其中程序產(chǎn)生錯誤的輸出或行為未能滿足所需屬性，從而提供關于如何改進系統(tǒng)的有價值的反饋。形式驗證的優(yōu)點是無需逐一測試單個輸入值或行為，這對于大型（或無限）狀態(tài)空間是不可能完全實現(xiàn)的。例如，在驗證緩存一致性協(xié)議和檢測設備驅(qū)動程序錯誤等形式方法的早期成功案例，導致了它們今天的可擴展性和實用性。這些方法現(xiàn)用于硬件和軟件行業(yè)，例如，英特爾、IBM、微軟和亞馬遜。由于形式方法語言、算法和工具的進步以及硬件和軟件的規(guī)模和復雜性的增加，在過去的幾年里，我們已經(jīng)看到了人們對形式驗證產(chǎn)生的新一輪興趣和興奮，特別是在確保系統(tǒng)基礎設施關鍵組件的正確性方面。
形式驗證是一種提供可證保證的方式，從而增加人們對系統(tǒng)將按預期運行的信任。
從傳統(tǒng)的形式方法到人工智能的形式方法。在傳統(tǒng)的形式方法中，我們想要證明一個模型M滿足（）一個屬性P。
M是要驗證的對象，它可以是一個程序，也可以是一個復雜系統(tǒng)的抽象模型，例如，并發(fā)的、分布式的或反應性的系統(tǒng)。P是用某種離散邏輯表示的正確性屬性。例如，M可能是使用鎖進行同步的并發(fā)程序，而P可能是“無死鎖”的。M 是無死鎖的證明意味著 M 的任何用戶都確信 M 永遠不會達到死鎖狀態(tài)。為了證明M滿足P，我們使用了形式化的數(shù)學邏輯，這是當今可擴展和實用的驗證工具的基礎，如模型檢驗器、定理證明器和可滿足模理論（SMT）求解器。
特別是當M是一個并發(fā)的、分布式或反應式的系統(tǒng)時，在傳統(tǒng)的形式方法中，我們經(jīng)常在驗證任務的制定中明確添加系統(tǒng)環(huán)境 E 的規(guī)范:
例如，如果M是一個并行進程，那么E可能是另一個與M交互的進程（然后我們可以寫成E || mp，其中||代表并行組合）。或者，如果M是設備驅(qū)動程序代碼，則E可能是操作系統(tǒng)的模型。又或者，如果M是一個控制系統(tǒng)，E則可能是關閉控制回路的環(huán)境模型。編寫E的規(guī)范是為了明確關于系統(tǒng)驗證環(huán)境的假設。
對于驗證人工智能系統(tǒng)，M可以解釋為一個復雜的系統(tǒng)，例如自動駕駛汽車，其中包含一個機器學習模型的組件，比如計算機視覺系統(tǒng)。在這里，我們想要證明P，打個比方，在E（交通、道路、行人、建筑物等）的背景下，相對于M（汽車）的安全性或穩(wěn)健性。我們可以把證明P看作是證明一個“系統(tǒng)級”屬性。Seshia等人用這個觀點闡述了形式規(guī)范的挑戰(zhàn)，其中深度神經(jīng)網(wǎng)絡可能是系統(tǒng)M的黑盒組件。
但是，對于機器學習模型我們能斷言什么呢？比如，DNN是這個系統(tǒng)的關鍵組成部分？我們是否可以驗證機器學習模型本身的穩(wěn)健性或公平性？是否有白盒驗證技術可以利用機器學習模型的結(jié)構？回答這些問題會帶來新的驗證挑戰(zhàn)。
驗證：機器學習模型M。為了驗證ML模型，我們重新解釋了M和P，其中M代表機器學習模型。P代表可信的屬性，例如安全性、穩(wěn)健性、隱私性或公平性。
與傳統(tǒng)的形式方法相比，驗證人工智能系統(tǒng)提出更多的要求。這里有兩個關鍵的區(qū)別：機器學習模型固有的概率性質(zhì)和數(shù)據(jù)的作用。
M和P的固有的概率性質(zhì)，因此需要概率推理()。ML模型M本身在語義和結(jié)構上都不同于典型的計算機程序。如前所述，它具有內(nèi)在的概率性，從現(xiàn)實世界中獲取輸入，這些輸入可能被數(shù)學建模為隨機過程，并產(chǎn)生與概率相關的輸出。在內(nèi)部，模型本身是基于概率的；例如，在深度神經(jīng)網(wǎng)絡中，邊緣上的標簽是概率，節(jié)點根據(jù)這些概率計算函數(shù)。從結(jié)構上講，因為機器生成了 ML 模型，所以 M 本身不一定是人類可讀或可理解的；粗略地說，DNN是由if-then-else語句組成的復雜結(jié)構，人類不太可能編寫這種語句。這種“中間代碼”表示在程序分析中開辟了新的研究方向。
屬性P本身可以在連續(xù)域而非（僅）離散域上表述，和/或使用來自概率和統(tǒng)計的表達式。深度神經(jīng)網(wǎng)絡的穩(wěn)健性被描述為對連續(xù)變量的預測，而公平性的特征是關于相對于實數(shù)的損失函數(shù)的期望（具體參見Dwork等人的研究）。差分隱私是根據(jù)相對于（小）真實值的概率差異來定義的。請注意，就像可信計算的實用性等屬性一樣，可信 AI 系統(tǒng)的一些所需屬性，例如透明度或道德感，尚未形式化或可能無法形式化。對于這些屬性，一個考慮法律、政策、行為和社會規(guī)則和規(guī)范的框架可以提供一個環(huán)境，在這個環(huán)境中可以回答一個可形式化的問題。簡而言之，人工智能系統(tǒng)的驗證將僅限于可以形式化的內(nèi)容。
形式驗證是一種提供可證保證的方式，從而增加人們對系統(tǒng)將按預期運行的信任。
這些固有的概率模型M和相關的所需信任屬性P需要可擴展的和/或新的驗證技術，這些技術適用于實數(shù)、非線性函數(shù)、概率分布、隨機過程等等。驗證人工智能系統(tǒng)的一個墊腳石是信息物理系統(tǒng)社區(qū)使用的概率邏輯和混合邏輯（參見Alur等人，Kwiatkowska等人和Platzer）。另一種方法是將時間邏輯規(guī)范直接集成到強化學習算法中。更具挑戰(zhàn)性的是，這些驗證技術需要對機器生成的代碼進行操作，尤其是本身可能無法確定生成的代碼
數(shù)據(jù)的作用。也許，傳統(tǒng)形式驗證和人工智能系統(tǒng)驗證之間更重要的區(qū)別在于數(shù)據(jù)的作用，用于訓練、測試和部署ML模型的數(shù)據(jù)。今天的ML模型是根據(jù)數(shù)據(jù)集D構建和使用的。為了驗證ML模型，我們提出對該數(shù)據(jù)的明確假設，并將驗證問題表述為:
數(shù)據(jù)分為可用數(shù)據(jù)和不可見數(shù)據(jù)，其中可用數(shù)據(jù)為手頭數(shù)據(jù)，用于培訓和測試M；而不可見數(shù)據(jù)是M需要（或期望）在之前沒有見過的情況下對其進行操作的數(shù)據(jù)。構建M背后的整個想法是，基于訓練和測試的數(shù)據(jù)，M能夠?qū)奈匆娺^的數(shù)據(jù)做出預測，且這個預測通常在一定程度上是準確的。
明確數(shù)據(jù)的作用提出了新的規(guī)范和驗證挑戰(zhàn)，可大致分為以下幾類，以及其相關的研究問題：
可用數(shù)據(jù)的收集和分區(qū):
對于給定的屬性P，需要多少數(shù)據(jù)才能建立一個模型M？深度學習的成功案例告訴我們，在準確性方面，數(shù)據(jù)越多，模型就越好，但其他屬性呢？添加更多的數(shù)據(jù)來訓練或測試M是否會使它更穩(wěn)健、更公平？或者它對屬性P沒有影響？如果所需的屬性不成立，需要收集哪些新數(shù)據(jù)？
我們?nèi)绾螌⒖捎茫ńo定）數(shù)據(jù)集劃分為訓練集和測試集？在構建模型 M 時，我們可以根據(jù)所需的屬性 P 對這種劃分做出什么保證？如果我們同時針對多個屬性訓練模型，我們是否會以不同的方式拆分數(shù)據(jù)？如果我們愿意用一種屬性交換另一種屬性，我們會以不同的方式來拆分數(shù)據(jù)嗎？
指定不可見數(shù)據(jù)：在形式化方法框架D中包含D，M P使我們有機會明確地陳述關于不可見數(shù)據(jù)的假設。
我們?nèi)绾沃付〝?shù)據(jù)和/或描述數(shù)據(jù)的屬性？例如，我們可以將D指定為一個隨機過程，它產(chǎn)生需要驗證ML模型的輸入。或者我們可以把D定義為數(shù)據(jù)分布。對于常見的統(tǒng)計模型，例如正態(tài)分布，我們可以根據(jù)其參數(shù)（例如均值和方差）指定 D。概率編程語言，例如 Stan，可能是指定統(tǒng)計模型的起點。但是，如果真實世界的大型數(shù)據(jù)集不符合常見的統(tǒng)計模型，或者有成千上萬的參數(shù)，又該怎么辦呢?
根據(jù)定義，在指定不可見的數(shù)據(jù)時，我們需要對不可見數(shù)據(jù)做出某些假設。這些假設會不會和我們一開始建立模型M時所做的假設一樣呢？更重要的是：我們?nèi)绾涡湃蜠的規(guī)范？這種看似邏輯的僵局類似于傳統(tǒng)驗證中的問題，給定一個M，我們需要假設元素的規(guī)范E和MP中元素E和P的規(guī)范是“正確的”。那么在驗證過程中，我們可能需要修改E和/或P（甚至M）。為了打破現(xiàn)有的循環(huán)推理，一種方法是使用不同的驗證方法來檢查 D 的規(guī)范；這種方法可以借鑒一系列統(tǒng)計工具。另一種方法是假設初始規(guī)范足夠小或足夠簡單，可以通過（例如，手動）檢查進行檢查；然后我們使用這個規(guī)范引導一個迭代的細化過程。（我們從形式方法的反例引導抽象和細化方法中獲得靈感。）這種細化過程可能需要修改D、M和/或P。
不可見數(shù)據(jù)的規(guī)范與M接受訓練和測試的數(shù)據(jù)規(guī)范有何關聯(lián)？
形式方法社區(qū)最近一直在探索人工智能系統(tǒng)的穩(wěn)健性，特別是用于自動駕駛汽車的圖像處理系統(tǒng)。
在傳統(tǒng)的驗證中，我們的目標是證明屬性P，一個普遍量化的語句：例如，對于整型變量x的所有輸入值，程序?qū)⒎祷匾粋€正整數(shù)；或者對于所有執(zhí)行序列x，系統(tǒng)不會死鎖。
因此，證明ML模型M中的P的第一個問題是：在P中，我們量化了什么？對于要在現(xiàn)實世界中部署的ML模型，一個合理的答案是對數(shù)據(jù)分布進行量化。但是ML模型僅適用于由現(xiàn)實世界現(xiàn)象形成的特定分布，而不適用于任意分布。我們不想為所有的數(shù)據(jù)分布證明一個屬性。對于我們在證明M的信任屬性時所量化的內(nèi)容和數(shù)據(jù)所代表的內(nèi)容之間的差異，這種見解導致了這個新的規(guī)范問題：
對于給定的 M，我們?nèi)绾沃付?P 應該保持的分布類別？以穩(wěn)健性和公平性作為兩個例子：
對于魯棒性，在對抗性機器學習設置中，我們可能想證明M對所有范數(shù)有界的擾動D是穩(wěn)健的。更有趣的是，我們可能想證明M對于手頭任務的所有“語義”或“結(jié)構”擾動都是穩(wěn)健的。例如，對于一些視覺任務，我們想要考慮旋轉(zhuǎn)或使圖像變暗，而不是僅僅改變?nèi)魏闻f像素。
對于公平性，我們可能想證明ML模型在給定數(shù)據(jù)集和所有“相似”（對于“相似”的正式概念）的所有不可見數(shù)據(jù)集上是公平的。訓練一種招聘工具，以決定在一個群體的申請者中面試誰，在未來的任何人群中都應該是公平的。我們?nèi)绾沃付ㄟ@些相關的分布?
為了構建一個既穩(wěn)健又公平的分類器，Mandal等人展示了如何調(diào)整在線學習算法，以找到對一類輸入分布公平的分類器。
驗證任務：一旦我們有了D和P的規(guī)范，給定一個M，我們就需要驗證M滿足P，給定我們對D中可用和不可見數(shù)據(jù)的任何假設，使用我們手頭上的任何邏輯框架。
我們?nèi)绾螜z查可用的數(shù)據(jù)以獲得所需的屬性？比如說，如果我們想要檢測一個數(shù)據(jù)集是否公平，我們應該檢查數(shù)據(jù)集的哪些方面？
如果我們發(fā)現(xiàn)屬性不存在，我們?nèi)绾涡迯湍Ｐ汀⑿薷膶傩裕蛘邲Q定收集哪些新數(shù)據(jù)來重新訓練模型？在傳統(tǒng)的驗證中，生成一個反例，例如，一個不滿足P的執(zhí)行路徑，有助于工程師調(diào)試他們的系統(tǒng)和/或設計。在ML模型的驗證中，“反例”的等效物是什么？我們?nèi)绾问褂盟?/span>
我們?nèi)绾卫貌豢梢姅?shù)據(jù)的顯式規(guī)范來幫助驗證任務？就像在驗證任務E, M P中明確環(huán)境規(guī)范E一樣，我們?nèi)绾卫妹鞔_的D規(guī)范？
我們?nèi)绾螖U展標準驗證技術來操作數(shù)據(jù)分布，也許可以利用我們形式上指定不可見數(shù)據(jù)的方式？
這兩個關鍵的區(qū)別——M的固有概率性質(zhì)和數(shù)據(jù)D的作用——為形式方法社區(qū)提供了研究機會，以推進人工智能系統(tǒng)的規(guī)范和驗證技術。
相關工作。形式方法社區(qū)最近一直在探索人工智能系統(tǒng)的穩(wěn)健性，特別是用于自動駕駛汽車的圖像處理系統(tǒng)。最先進的VerifAI系統(tǒng)探索了自動駕駛汽車穩(wěn)健性的驗證，依靠模擬來識別執(zhí)行軌跡，其中網(wǎng)絡物理系統(tǒng)（例如，自動駕駛汽車）的控制依賴于嵌入式 ML 模型可能出錯。ReluVal和Neurify等工具研究了DNN的穩(wěn)健性，特別是應用于自動駕駛汽車的安全性，包括自動駕駛汽車和飛機防撞系統(tǒng)。這些工具依靠區(qū)間分析來減少狀態(tài)探索，同時仍然提供強有力的保證。在F1/10賽車平臺上，使用Verisig驗證基于DNN的控制器的安全性的案例研究為比較不同的DNN配置和輸入數(shù)據(jù)的大小提供了基準，并識別了模擬和驗證之間的當前差距。
FairSquare2使用概率驗證來驗證ML模型的公平性。LightDP60將概率性程序轉(zhuǎn)換為非概率性程序，然后進行類型推斷以自動驗證不同隱私的隱私預算。
這些工具都體現(xiàn)了可信AI的精神，但每一個工具都只關注一個屬性。將他們的底層驗證技術擴展到工業(yè)規(guī)模的系統(tǒng)仍然是一個挑戰(zhàn)。
額外的形式方法機會。今天的人工智能系統(tǒng)是為了執(zhí)行特定任務而開發(fā)的，例如識別人臉或下圍棋。我們?nèi)绾慰紤]已部署的ML模型在規(guī)范和驗證問題中要執(zhí)行的任務？例如，考慮顯示進行圖像分析的ML模型M的穩(wěn)健性：對于識別道路上的汽車的任務，我們希望M對任何一側(cè)有凹痕的汽車圖像都是穩(wěn)健的；但對于汽車生產(chǎn)線的質(zhì)量控制任務，我們就不會這么做。
之前，我們主要關注形式方法中的驗證任務。但形式方法的機制最近也成功地用于程序合成。與其對模型 M 進行事后驗證，我們能否首先開發(fā)一種“構建正確”的方法來構建 M？例如，我們是否可以在訓練和測試M時添加所需的可信屬性P作為約束，以保證P在部署時成立（可能適用于給定的數(shù)據(jù)集或一類分布）？這種方法的一種變體是通過在每個步驟檢查算法不會不滿足不希望行為來指導 ML 算法設計過程。類似地，安全強化學習解決決策過程中的學習策略，其中安全性作為優(yōu)化的一個因素或探索的外部約束。
本文開頭列舉的有關可信AI的一系列屬性并不實用，但每個屬性對于建立信任都至關重要。擺在研究界面前的一項任務是制定出這些屬性的共性，然后可以在一個共同的邏輯框架中指定這些共性，類似于使用時間邏輯來指定安全性（“沒有壞事發(fā)生”）和活躍性（“最終有好事發(fā)生”）用來推理并發(fā)和分布式系統(tǒng)的正確性屬性。
組合推理使我們能夠?qū)Υ笮蛷碗s系統(tǒng)進行驗證。如何驗證AI系統(tǒng)的屬性“提升”組件以顯示該屬性適用于系統(tǒng)？相反地，我們該如何將AI系統(tǒng)分解成多個部分，根據(jù)給定屬性驗證每個部分，并斷言這個屬性對于整體成立？哪些屬性是全局的（避免組合），哪些是局部的？數(shù)十年來，對組合規(guī)范和驗證的形式化方法的研究為我們提供了一個很好的起點，即詞匯和框架。
統(tǒng)計學在模型檢查和模型評估方面有著豐富的歷史，使用的工具包括敏感性分析、預測評分、預測檢查、殘差分析和模型批評等。為了驗證ML模型滿足所需屬性，這些統(tǒng)計方法可以補充形式驗證方法，就像測試和模擬補充計算系統(tǒng)的驗證一樣。更相關的是，正如前面提到的“數(shù)據(jù)的作用”中所述，它們可以幫助評估用于指定D，M P問題中不可見數(shù)據(jù)D的任何統(tǒng)計模型。形式方法社區(qū)的一個機會是將這些統(tǒng)計技術與傳統(tǒng)的驗證技術相結(jié)合（有關這種組合的早期工作，請參考 Younes 等人的研究）。
構建可信AI社區(qū)
正如可信計算一樣，形式方法只是確保增加人工智能系統(tǒng)信任的一種方法。社區(qū)需要探索多種方法，尤其是組合方法，以實現(xiàn)可信AI。其他方法包括測試、模擬、運行時監(jiān)視、威脅建模、漏洞分析，以及對代碼和數(shù)據(jù)進行等效的設計和代碼審查。此外，除了技術挑戰(zhàn)，還有社會、政策、法律和倫理方面的挑戰(zhàn)。
2019年10月30日至11月1日，哥倫比亞大學數(shù)據(jù)科學研究所主辦了由 DSI 行業(yè)附屬機構 Capital One 贊助的關于可信AI的首屆研討會。它匯集了來自形式方法、安全和隱私、公平和機器學習的研究人員。來自業(yè)界的發(fā)言者對學術界正在追求的各種問題和方法進行了現(xiàn)實檢驗。與會者確定了研究面臨的挑戰(zhàn)領域，包括:
規(guī)范和驗證技術；
“正確構建”技術；
新的威脅模型和系統(tǒng)級對抗性攻擊；
審核考慮可解釋性、透明度和責任等屬性的人工智能系統(tǒng)的流程；
檢測偏差和去偏差數(shù)據(jù)的方法、機器學習算法及其輸出；
試驗可信屬性的系統(tǒng)基礎設施；
理解人為因素，例如，機器在哪些方面影響人類行為；
理解社會因素，包括社會福利、社會規(guī)范、道德、倫理和法律。
許多推動機器學習和人工智能前沿的科技公司并沒有坐以待斃。他們意識到可信AI對他們的客戶、業(yè)務和社會福利的重要性，主要關注的是公平性。IBM的AI Fairness 360提供了一個開源工具包，用于檢查數(shù)據(jù)集和機器學習模型中不必要的偏見。谷歌的TensorFlow工具包提供了“公平性指標”，用于評估二元和多類分類器的公平性。微軟的 Fairlearn 是一個開源包，供機器學習開發(fā)人員評估其系統(tǒng)的公平性并減輕觀察到的不公平。在2018年的F8大會上，F(xiàn)acebook宣布了其Fairness Flow 工具，旨在“衡量對特定群體的潛在偏見”。本著行業(yè)和政府合作的精神，亞馬遜和美國國家科學基金會自 2019 年開始合作資助“人工智能公平”計劃。
2016年，美國國防部高級研究計劃局（DARPA）通過啟動可解釋人工智能 （XAI） 計劃，專注于可解釋性。該計劃的目標是開發(fā)新的機器學習系統(tǒng)，可以“解釋其基本原理、描述其優(yōu)勢和劣勢，并傳達其對未來表現(xiàn)的理解。”有了可解釋性，終端用戶就會更加相信并采納系統(tǒng)的結(jié)果。
通過安全可信的網(wǎng)絡空間計劃（Secure and Trustworthy Cyberspace Program），國家科學基金會資助了一個由賓夕法尼亞州立大學領導的可信賴機器學習中心，來自斯坦福大學、加州大學伯克利分校、加州大學圣地亞哥分校、弗吉尼亞大學和威斯康星大學的研究人員也參與其中。他們的主要重點是解決對抗性機器學習，補充之前概述的形式方法。（為了充分披露，本文作者是該中心顧問委員會成員。）2019年10月，美國國家科學基金會宣布了一項資助國家人工智能研究所的新計劃。它命名的六個主題之一是“可信AI”，強調(diào)可靠性、可解釋性、隱私性和公平性等屬性。
NITRD關于人工智能和網(wǎng)絡安全的報告明確呼吁對人工智能系統(tǒng)的規(guī)范和驗證以及可信的人工智能決策進行研究。最后，在2020年12月，白宮簽署了一項關于可信AI的行政命令，為美國聯(lián)邦機構在其服務中采用人工智能提供指導，并促進公眾對人工智能的信任。
正如可信計算一樣，政府、學術界和產(chǎn)業(yè)界正在共同推動可信AI的新研究議程。我們正加大對這一圣杯的賭注！
雷鋒網(wǎng)
