如何創(chuàng)建能夠安全地導(dǎo)航我們世界的人工智能

在過去的幾十年里，前所未有的技術(shù)進步使我們能夠升級和現(xiàn)代化大部分基礎(chǔ)設(shè)施并解決許多長期存在的后勤問題。例如，Babylon Health的AI驅(qū)動智能手機應(yīng)用程序正在幫助評估北倫敦120萬患者的優(yōu)先級，電子轉(zhuǎn)移使我們能夠在世界任何地方即時匯款，并且在過去的20年中，GPS徹底改變了我們的導(dǎo)航方式，我們?nèi)绾胃櫤瓦\送貨物，以及我們?nèi)绾喂芾斫煌ā?/p>

然而，指數(shù)增長伴隨著必須導(dǎo)航的一系列障礙。最重要的問題是，預(yù)測各種技術(shù)將如何演變是非常困難的。因此，規(guī)劃未來并確保實施必要的安全功能變得具有挑戰(zhàn)性。

當(dāng)涉及可能帶來存在挑戰(zhàn)的技術(shù)時，這種不確定性尤其令人擔(dān)憂 - 例如人工智能。

然而，盡管明天的AI具有不可預(yù)測的性質(zhì)，但某些挑戰(zhàn)是可以預(yù)見的。例如，無論AI代理商最終采取的發(fā)展路徑如何，這些系統(tǒng)都需要能夠做出明智的決策，使其能夠在我們的物理世界中無縫安全地移動。實際上，人工智能最有影響力的用途之一包括自動駕駛汽車，機器人外科醫(yī)生，用戶感知智能電網(wǎng)和飛機控制系統(tǒng)等技術(shù) - 所有這些都將先進的決策過程與運動物理結(jié)合起來。

這種系統(tǒng)被稱為網(wǎng)絡(luò)物理系統(tǒng)(CPS)。下一代先進的CPS可以引領(lǐng)我們進入一個安全的新時代，將崩潰率降低90%，每年為世界各國節(jié)省數(shù)千億美元- 但前提是這些系統(tǒng)本身正確實施。

這就是卡內(nèi)基梅隆大學(xué)計算機科學(xué)副教授安德烈·普拉澤(Andre Platzer)所在的地方.Platzer的研究致力于確保CPS有益于人類并且不會造成傷害。實際上，這意味著確保系統(tǒng)靈活，可靠和可預(yù)測。

擁有安全系統(tǒng)意味著什么?

網(wǎng)絡(luò)物理系統(tǒng)已經(jīng)以某種形式出現(xiàn)了很長一段時間。例如，空中交通管制系統(tǒng)長期以來一直依賴CPS型技術(shù)來避免碰撞，交通管理和許多其他決策任務(wù)。但是，Platzer指出，隨著CPS的不斷發(fā)展，以及越來越需要集成更復(fù)雜的自動化和學(xué)習(xí)技術(shù)，確保CPS做出可靠和安全的決策變得更加困難。

為了更好地澄清問題的本質(zhì)，Platzer轉(zhuǎn)向自動駕駛車輛。在像這樣的先進系統(tǒng)中，他指出我們需要確保技術(shù)足夠復(fù)雜以實現(xiàn)靈活性，因為它必須能夠安全地響應(yīng)它所面臨的任何情況。從這個意義上說，“如果他們不僅僅運行非常簡單的[控制系統(tǒng)]，CPS就處于最佳狀態(tài)，但如果它們運行的??是更復(fù)雜和先進的系統(tǒng)，”Platzer指出。然而，當(dāng)CPS利用高級自治時，因為它們非常復(fù)雜，所以要證明它們正在進行系統(tǒng)的合理選擇變得更加困難。

在這方面，系統(tǒng)越復(fù)雜，我們就越不得不犧牲一些可預(yù)測性，從而犧牲系統(tǒng)的安全性。正如Platzer所闡述的那樣，“在安全方面為您提供可預(yù)測性的簡單性與您在人工智能方面需要的靈活性有些不一致。”

因此，最終目標是在靈活性和可預(yù)測性之間找到平衡 - 在先進學(xué)習(xí)技術(shù)和安全證明之間 - 以確保CPS能夠安全有效地執(zhí)行其任務(wù)。Platzer將這一總體目標描述為一種平衡行為，并指出，“利用網(wǎng)絡(luò)物理系統(tǒng)，為了使復(fù)雜性變得可行和可擴展，保持系統(tǒng)盡可能簡單也很重要。”

如何使系統(tǒng)安全

導(dǎo)航此問題的第一步是確定研究人員如何驗證CPS是否真正安全。在這方面，Platzer指出，他的研究是由這個核心問題所驅(qū)動的：如果科學(xué)家對自動駕駛汽車或飛機這樣的行為有一個數(shù)學(xué)模型，并且他們有信心控制器的所有行為是安全的，他們?nèi)绾巫C明事實確實如此?

答案是一個自動定理證明器，它是一個計算機程序，可以幫助開發(fā)嚴格的數(shù)學(xué)正確性證明。

對于CPS，最高的安全標準是這樣的數(shù)學(xué)正確性證明，表明系統(tǒng)總是為任何給定的輸入產(chǎn)生正確的輸出。它通過使用正式的數(shù)學(xué)方法來證明或反駁系統(tǒng)底層控制算法的正確性。

在確定并創(chuàng)建了這種證明技術(shù)之后，Platzer聲稱下一步是使用它來增強人工智能學(xué)習(xí)代理的功能 - 增加其復(fù)雜性，同時驗證其安全性。

最終，Platzer希望這將最終使技術(shù)能夠讓CPS從預(yù)期結(jié)果未能成為現(xiàn)實的準確模型的情況中恢復(fù)過來。例如，如果自動駕駛汽車假設(shè)另一輛汽車在實際減速時加速，則需要能夠快速糾正此錯誤并切換到正確的現(xiàn)實數(shù)學(xué)模型。

這種無縫轉(zhuǎn)換越復(fù)雜，它們實現(xiàn)起來就越復(fù)雜。但它們是安全性和靈活性的最終融合，換句話說，是人工智能與安全防護技術(shù)的最終結(jié)合。

創(chuàng)造明天的技術(shù)

到目前為止，Platzer研究的最大進展之一是KeYmaera X prover，Platzer將其定義為“我們安全技術(shù)可靠性方面的巨大飛躍，遠遠超出其他任何人的做法。用于分析網(wǎng)絡(luò)物理系統(tǒng)。“

由Platzer及其團隊創(chuàng)建的KeYmaera X證明器是一種工具，允許用戶通過易于使用的界面輕松可靠地為CPS構(gòu)建數(shù)學(xué)正確性證明。

從技術(shù)上講，KeYmaera X是一個混合系統(tǒng)定理證明器，它將受控系統(tǒng)的控制程序和物理行為分析在一起，以便為復(fù)雜的安全驗證技術(shù)提供有效的計算和必要的支持。最終，這項工作建立在之前稱為KeYmaera的技術(shù)迭代之上。但是，Platzer表示，為了優(yōu)化工具并使其盡可能簡單，團隊基本上“從頭開始”。

Platzer強調(diào)這些最近的變化有多么引人注目，并指出，在之前的證明中，語句的正確性取決于大約66,000行代碼。值得注意的是，這66,000行中的每一行都對判決的正確性至關(guān)重要。根據(jù)Platzer的說法，這會帶來一個問題，因為確保所有線路都能正確實施非常困難。盡管KeYmaera的最新版本最終與之前的版本一樣大，但在KeYmaera X中，負責(zé)驗證正確性的證明器部分僅為2,000行代碼。

這使得團隊可以比以往更可靠地評估網(wǎng)絡(luò)物理系統(tǒng)的安全性。“我們確定了這個微內(nèi)核，這個系統(tǒng)中真正微不足道的部分負責(zé)答案的正確性，所以現(xiàn)在我們有更好的機會確保我們不會意外地將任何錯誤泄漏到推理引擎中，”Platzer說過。同時，他指出，它使用戶能夠在分析中進行更積極的自動化。Platzer解釋說，“如果你有一小部分系統(tǒng)負責(zé)正確性，那么你可以做更自由的自動化。它可以更加勇敢，因為它下面有一個完整的安全網(wǎng)。“

對于他的研究的下一階段，Platzer將開始整合可能將現(xiàn)實描述為CPS的多種數(shù)學(xué)模型。為了解釋這些接下來的步驟，Platzer再次回歸自動駕駛汽車：“如果你跟隨另一個駕駛員，你不知道駕駛員是否正在尋找停車位，試圖快速到達某個地方，或者即將到來改變車道。因此，原則上，在這種情況下，擁有多個可能的模型并遵守可能是對現(xiàn)實的最佳解釋的模型是個好主意。“

最終，目標是允許CPS通過在這些多個模型之間切換來增加其靈活性和復(fù)雜性，因為它們或多或少可能解釋現(xiàn)實。“世界是一個復(fù)雜的地方，”普拉澤爾解釋說，“所以世界的安全分析也必須是一個復(fù)雜的分析。”