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

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

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

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

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

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

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

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

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

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

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

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

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

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

答案是一個(gè)自動(dòng)定理證明器，它是一個(gè)計(jì)算機(jī)程序，可以幫助開發(fā)嚴(yán)格的數(shù)學(xué)正確性證明。

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

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

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

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

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

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

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

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

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

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

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

最終，目標(biāo)是允許CPS通過(guò)在這些多個(gè)模型之間切換來(lái)增加其靈活性和復(fù)雜性，因?yàn)樗鼈兓蚨嗷蛏倏赡芙忉尙F(xiàn)實(shí)。“世界是一個(gè)復(fù)雜的地方，”普拉澤爾解釋說(shuō)，“所以世界的安全分析也必須是一個(gè)復(fù)雜的分析。”