隨著AI技術(shù)的發(fā)展，自主智能體在速度和精確度方面有了很大的提升，變得更加智能和高效，展現(xiàn)出在各種具體任務(wù)上的令人印象深刻的性能，并成功地互相協(xié)作，實現(xiàn)了自己的獨(dú)立目標(biāo)。在本文中，俄羅斯Innopolis大學(xué)機(jī)器人研究所的Konstantin Danilov、Ruslan Rezin、Alexander Kolotov和Ilya Afanasyev教授提出了一種分散式交易市場的概念，可將其稱之為“機(jī)器人經(jīng)濟(jì)學(xué)（robonomics）”。

在這種市場中，自主智能體可以根據(jù)共識協(xié)議消費(fèi)和生產(chǎn)服務(wù)。那么，在這種市場中，客戶如何根據(jù)服務(wù)提供商執(zhí)行責(zé)任的程度獲取對他們的信任程度？又或者如何檢測服務(wù)提供商沒能夠正確執(zhí)行責(zé)任從而中止支付交易呢？ 對此，專家們給出了新的答案。

一般來說，分散式交易市場方法（decentralized trading market approach），即自主的智能體和人員都可以消費(fèi)和生產(chǎn)服務(wù)，以擴(kuò)大自己實現(xiàn)目標(biāo)的機(jī)會，這作為第四次工業(yè)革命的一部分，看起來很有發(fā)展前景。

該方法的關(guān)鍵組成部分是區(qū)塊鏈平臺（blockchain platform），該平臺使得智能體之間通過責(zé)任智能合約（liability smart contract）進(jìn)行交互。服務(wù)提供者的可靠性通常取決于聲譽(yù)模型（reputation model）。然而，這種解決方案只會警醒未來的客戶對服務(wù)提供商的信任程度，以防它無法正確執(zhí)行任何以前的責(zé)任。

另一方面，區(qū)塊鏈共識協(xié)議（blockchain consensus protocol）還可以包含一個驗證程序，用于檢測不正確的責(zé)任執(zhí)行情況，以便暫停向有問題的服務(wù)提供者的支付交易。本文提出了一種對于分散式交易市場中基于智能體的服務(wù)提供者的責(zé)任執(zhí)行驗證方法，該方法使用了基于有限狀態(tài)自動機(jī)（finite state automata）的數(shù)學(xué)模型和有用的時間邏輯屬性（Temporal Logic property）的模型檢測方法（Model Checking method）。

為了說明這個概念，我們在Duckietown應(yīng)用程序中實施了這個方法：移動一個自主的移動機(jī)器人，并使用在一個完整場景結(jié)束時所進(jìn)行的接下來的行為驗證（behavior validation）實現(xiàn)一個任務(wù)目標(biāo)。

圖1：在責(zé)任生命周期中自主智能體之間進(jìn)行交互的通用方案。

在過去的十年中，自主智能體在速度和精確度方面變得更加智能和高效，展現(xiàn)出在各種具體任務(wù)上的令人印象深刻的性能，并成功地互相協(xié)作，實現(xiàn)了自己的獨(dú)立目標(biāo)。這就提出了分散式交易市場的概念，在這種市場中，自主智能體可以根據(jù)共識協(xié)議消費(fèi)和生產(chǎn)服務(wù)。

由于區(qū)塊鏈技術(shù)的出現(xiàn)，特別是解決了雙重支出攻擊問題（double-spending attack problem）的比特幣的實現(xiàn)（Bitcoin），分散式的多智能體系統(tǒng)概念開始變得可行，只要智能體不依賴于單點(diǎn)故障，并且它們的操作對于監(jiān)控而言是透明的。

雖然區(qū)塊鏈最初是作為加密貨幣的解決方案引入的，但它啟發(fā)了以太坊平臺（Ethereum platform）的開發(fā)人員提出了一個新的概念：智能合約——一種協(xié)議的算法執(zhí)行。很快，它成為了分散式應(yīng)用程序的最大平臺，為銷售計算機(jī)的處理能力和分散式計算存儲等市場服務(wù)的研發(fā)提供了新的動力。

基于區(qū)塊鏈的平臺的另一個例子是，以IoT（Internet of Things，物聯(lián)網(wǎng)）市場為導(dǎo)向的自主智能體IOTA的分散式網(wǎng)絡(luò)。盡管我們所討論的項目變得通用了，但它們都集中在特定類型的自主智能體上，這嚴(yán)重限制了可用的服務(wù)。AIRA項目首先引入了分散式交易市場的概念，自主智能體和人員可以消費(fèi)和提供服務(wù)。

作者將這個概念定義為“機(jī)器人經(jīng)濟(jì)學(xué)”（robonomics）。這種AIRA方法建議拒絕集中式機(jī)器人控制的原則，以在機(jī)器人和人類之間提供分散式通信，使用基于區(qū)塊鏈的智能合約作為這些通信的基礎(chǔ)。由于責(zé)任依賴于現(xiàn)實世界的流程，所以不能保證智能體始終能夠正確地執(zhí)行它們。

這可能是由服務(wù)提供者造成的，因為（1）故意欺詐或（2）由于故障而導(dǎo)致的不正確行為。對于第一個問題，AIRA開發(fā)人員認(rèn)為，可以開發(fā)一個聲譽(yù)模型并將其集成到共識協(xié)議中，該協(xié)議將在區(qū)塊鏈信息中反映出對智能體的信任程度。

因此，消費(fèi)者可以進(jìn)一步依賴這些信息來選擇服務(wù)提供者。對于第二個問題，AIRA項目仍然需要技術(shù)和理論的解決方案，這是本文的重點(diǎn)。

圖2：我們在Duckietown環(huán)境中的實驗。Duckiebot執(zhí)行一項任務(wù)，通過遵循責(zé)任智能合約中的標(biāo)簽順序，并將觀察到的標(biāo)簽記錄到日志中，這是由驗證人在任務(wù)結(jié)束后進(jìn)行驗證得到的，從而最終穿過“城市”。

在這項研究中，我們將注意力集中在那些其行為可以用非確定性有限狀態(tài)自動機(jī)進(jìn)行描述的智能體上（（又可以被稱之為基于智能體系統(tǒng)））。對于這些智能體，我們提供了全新的責(zé)任執(zhí)行的驗證方法，使得能夠檢測出由故障的智能體。

它的工作原理是假定出現(xiàn)故障的服務(wù)提供商所產(chǎn)生的結(jié)果與其行為模型相矛盾，并導(dǎo)致自動暫停購買。驗證方法是基于正式的軟件驗證方法，即模型檢查（Model Checking）。由于移動機(jī)器人可以在諸如物流、運(yùn)輸?shù)确矫娴默F(xiàn)實生活中加以使用，所以我們?yōu)镈uckietown環(huán)境提供了簡單的原型實現(xiàn)，其中，一個移動機(jī)器人穿過城鎮(zhèn)，以給定的標(biāo)簽序列為導(dǎo)向，在一個完整場景結(jié)束時通過自身的行為驗證實現(xiàn)任務(wù)目標(biāo)。

我們的驗證方法可以（1）直接實現(xiàn)到一個共識協(xié)議中，或（2）實現(xiàn)作為分散式區(qū)塊鏈應(yīng)用程序的一部分。在前一種情況下，假定責(zé)任執(zhí)行的驗證可以在驗證者節(jié)點(diǎn)（采礦者）和交易上以分散形式進(jìn)行，確認(rèn)服務(wù)是以一種適當(dāng)?shù)姆绞竭M(jìn)行提供的，將被包括在新區(qū)塊中。

例如，它可以通過支持可插拔共識的現(xiàn)有解決方案來實現(xiàn)，如Parity或Hyperledger。而在后一種情況下，它被集成到AIRA的方法中，其中驗證由第三方應(yīng)用程序執(zhí)行，該應(yīng)用程序?qū)Ⅱ炞C結(jié)果提交給以太坊智能合約。

這項研究是全周期責(zé)任執(zhí)行的概念驗證，涵蓋了驗證階段。有了這個證明概念，那么如今評估現(xiàn)有的roboomics基礎(chǔ)設(shè)施并提出相關(guān)改善是非常重要的。這項研究的重要組成部分是現(xiàn)實生活中實際應(yīng)用案例的分析。

在這項研究中，我們考慮簡單的行為模型，它可以被評估為復(fù)雜的出租車服務(wù)原型的第一級，并作為案例研究的起點(diǎn)。通過不斷地添加的新組件便可以順序地增加其復(fù)雜性。每個組件和案例都是進(jìn)一步調(diào)查的主題。尚未解決的問題如下：

1）通常情況下，用戶會要求出租車服務(wù)從A點(diǎn)到B點(diǎn)去接他們。這應(yīng)該被定義為，完整循環(huán)（移到A然后移到B）的目標(biāo)是什么？以及我們應(yīng)該為這種情況創(chuàng)建多少智能合同。

2）在我們簡單的案例中，用戶直接與robocar進(jìn)行交易，這意味著用戶應(yīng)提前知道汽車的位置和地址。但是，通常情況并非如此。某些中間服務(wù)需要連接到用戶和服務(wù)提供商。

3）隨著物聯(lián)網(wǎng)設(shè)備數(shù)量的不斷增加以及道路基礎(chǔ)設(shè)施的不斷完善，我們有可能將其轉(zhuǎn)變?yōu)閞obeconomic的一部分。例如，汽車可以與基礎(chǔ)設(shè)施進(jìn)行交互，以建立最佳路線，甚至還可以從基礎(chǔ)設(shè)施那里獲得有力支持。

4）AIRA責(zé)任驗證模型假定機(jī)器人不會故意偽造目標(biāo)執(zhí)行日志（objective execution intentionally）。這意味著，服務(wù)提供者可以選擇接受報酬，盡管其尚未提供相應(yīng)服務(wù)。目前，有可能解決這一問題的方案是引入“記錄器”（recorders），例如，它可以將智能體在特定時間內(nèi)，于特定地點(diǎn)出現(xiàn)的事實，記錄在區(qū)塊鏈中。在日志檢驗過程中可以考慮這些信息。我們應(yīng)該建立完整的過程描述以及經(jīng)濟(jì)模型：有人應(yīng)該為這些數(shù)據(jù)支付費(fèi)用。

顯然，復(fù)雜的智能體行為需要通過建模和檢驗框架進(jìn)行改進(jìn)：

?模型校驗方法的主要缺點(diǎn)是，對于基于基于智能體的系統(tǒng)而言，其狀態(tài)數(shù)量會隨變量數(shù)量的增加，而呈現(xiàn)出增長態(tài)勢。這意味著并非所有模型都可以進(jìn)行物理處理，因此需要一種機(jī)制來限制模型的復(fù)雜性。

?當(dāng)概率模型比非確定性模型更適用時，就必須開展更多的工作來擴(kuò)展這一方法。在這種情況下，可以采用概率模型檢驗（Probabilistic Model Checking）。

?檢驗框架也可以得到增強(qiáng)。特別是這樣一種工具的實現(xiàn)，即該工具使得能夠從模型檢驗?zāi)Ｐ停∕odel Checking model）中自動生成高級代碼，并將其集成到服務(wù)開發(fā)項目中。

?使用新的屬性類型可以使屬性生成工具得到增強(qiáng)。此外，我們還可以將工具的使用權(quán)限擴(kuò)展至客戶，允許他們構(gòu)建自己的屬性，例如，允許服務(wù)提供者在履行責(zé)任之前，檢驗所提交的模型是否滿足他們的需求。

在本文中，我們提出了一種針對自主智能體（autonomous agents）分散交易市場模型的概念，并將其命名為robonomics。針對基于智能體的特殊系統(tǒng)，我們還引入了一種基于模型檢驗的正式軟件驗證技術(shù)的新方法，以解決責(zé)任執(zhí)行的驗證問題，這有助于中止對發(fā)生故障的服務(wù)提供者的支付行為，并可與聲譽(yù)模型一起集成于區(qū)塊鏈共識協(xié)議中。

驗證過程試圖證明服務(wù)提供者在執(zhí)行操作后所提交的結(jié)果與其事先提交的行為模型相對應(yīng)。然而，要將屬性作為輸入傳遞給模型檢驗器（Model Checker），就必須將其轉(zhuǎn)換為時態(tài)邏輯公式（Temporal Logic formula）。

此外，復(fù)雜系統(tǒng)模型的構(gòu)建也是一項復(fù)雜的任務(wù)，該模型適合于模型檢驗器的執(zhí)行。因此，我們建立了有助于解決這兩項問題的框架。驗證方法作為復(fù)雜AIRA robonomics原型的一部分受到了評估，該原型是使用Duckietown項目實現(xiàn)的。

該原型實現(xiàn)了一個簡單的真實案例，即一個機(jī)器人根據(jù)給定路線行駛，并進(jìn)行了后續(xù)責(zé)任驗證。最后，我們討論了所提解決方案對于未來的影響。