5月20日，圖靈獎(jiǎng)得主Joseph Sifakis應(yīng)邀做客師大，在中山北路校區(qū)科學(xué)會(huì)堂為師生們帶來(lái)了題為“Autonomous Systems-A Rigorous Architectural Characterization（自主系統(tǒng)——嚴(yán)謹(jǐn)?shù)募軜?gòu)描述）”的學(xué)術(shù)報(bào)告，與師生及業(yè)界人士暢談如何理解“自主系統(tǒng)”?；顒?dòng)由計(jì)算機(jī)科學(xué)與軟件工程學(xué)院院長(zhǎng)何積豐院士主持。
圖靈獎(jiǎng)得主Joseph Sifakis作“自主系統(tǒng)——嚴(yán)謹(jǐn)?shù)募軜?gòu)描述”學(xué)術(shù)報(bào)告
計(jì)算機(jī)科學(xué)與軟件工程學(xué)院院長(zhǎng)何積豐院士主持
2007年，Joseph Sifakis被美國(guó)計(jì)算機(jī)協(xié)會(huì)（ACM）授予有“計(jì)算機(jī)界的諾貝爾獎(jiǎng)”之稱(chēng)的圖靈獎(jiǎng)，以表彰其在模型檢查理論和應(yīng)用方面做出的卓越貢獻(xiàn)。Joseph Sifakis是法國(guó)國(guó)家科研中心榮譽(yù)研究員、格勒諾布爾市Verimag實(shí)驗(yàn)室創(chuàng)始人，法國(guó)科學(xué)院院士、法國(guó)國(guó)家工程院院士、歐洲科學(xué)院院士、美國(guó)藝術(shù)與科學(xué)學(xué)院院士及美國(guó)國(guó)家工程院院士。研究領(lǐng)域主要包括系統(tǒng)設(shè)計(jì)的基本概念和應(yīng)用，主要專(zhuān)注于系統(tǒng)設(shè)計(jì)的形式化，即根據(jù)特定的要求實(shí)現(xiàn)可信賴(lài)、最優(yōu)化且構(gòu)造正確的系統(tǒng)。
講座開(kāi)始，Joseph Sifakis首先介紹了自主系統(tǒng)的概念和基本組成（“智能體” Agent ，“對(duì)象” Object，“環(huán)境”Environment），提出“自主”是實(shí)現(xiàn)物聯(lián)網(wǎng)愿景的關(guān)鍵所在。所謂“自主”，即在將智能服務(wù)更好地集成于系統(tǒng)的同時(shí)，最大限度地減少人為干預(yù)。通過(guò)使用溫控系統(tǒng)、自動(dòng)控制列車(chē)、象棋機(jī)器人等常見(jiàn)的應(yīng)用實(shí)例，Joseph Sifakis解釋了自主系統(tǒng)如何“自主”實(shí)現(xiàn)既定目標(biāo)，并基于自主系統(tǒng)的發(fā)展現(xiàn)狀，提出了下一代自主系統(tǒng)的主要特征以及面臨的制約與挑戰(zhàn)。
自助系統(tǒng)應(yīng)用實(shí)例
Joseph Sifakis著重講述了他提出的一種結(jié)合系統(tǒng)構(gòu)架模型和智能體模型的通用計(jì)算模型，該模型可以調(diào)理自主系統(tǒng)中“智能體” (Agent) 和“對(duì)象” (Object) 的關(guān)系，使得系統(tǒng)在不同的突發(fā)環(huán)境條件下，能夠獨(dú)立實(shí)現(xiàn)動(dòng)態(tài)、可重構(gòu)的多模式協(xié)調(diào)，從而自主完成任務(wù)。Joseph Sifakis提出的通用模型結(jié)合了五個(gè)維度，分別是感知、知識(shí)庫(kù)、目標(biāo)管理、規(guī)劃和自適應(yīng)，這五個(gè)維度構(gòu)成了“自主復(fù)雜性”的概念。隨后，他以美國(guó)汽車(chē)工程師學(xué)會(huì)（SAE）對(duì)自動(dòng)駕駛的6個(gè)不同程度的自動(dòng)化分級(jí)為例，形象對(duì)比了機(jī)器自主和人類(lèi)輔助機(jī)器自主之間的差距，說(shuō)明了構(gòu)建自主系統(tǒng)的難度。
自動(dòng)駕駛的6個(gè)不同程度的自動(dòng)化分級(jí)
隨后，Joseph Sifakis 從自主復(fù)雜性、設(shè)計(jì)復(fù)雜性、反應(yīng)復(fù)雜性和架構(gòu)復(fù)雜性等方面，討論了自主系統(tǒng)面臨的復(fù)雜性問(wèn)題。在他看來(lái)，嚴(yán)格的自主系統(tǒng)設(shè)計(jì)應(yīng)該重視準(zhǔn)確性并嚴(yán)格遵循開(kāi)發(fā)流程，以達(dá)到“可信賴(lài)”(Trustworthiness) 的目標(biāo)。在自主系統(tǒng)的構(gòu)建中，不論是人工智能還是機(jī)器學(xué)習(xí)技術(shù)，都是不可或缺的，但現(xiàn)有的機(jī)器學(xué)習(xí)技術(shù)在模型的正確性證明方面仍有局限性。
講座現(xiàn)場(chǎng)
在總結(jié)階段，Joseph Sifakis 對(duì)其研究成果進(jìn)行了概述：“自主”作為一種廣泛的智能，不應(yīng)只局限于特定的實(shí)現(xiàn)技術(shù)，而應(yīng)強(qiáng)調(diào)系統(tǒng)的功能設(shè)計(jì)；“可信賴(lài)”的自主系統(tǒng)構(gòu)建遠(yuǎn)遠(yuǎn)超過(guò)目前人工智能系統(tǒng)所面臨的挑戰(zhàn)，并發(fā)起了對(duì)下一代自主系統(tǒng)標(biāo)準(zhǔn)的討論。
演講結(jié)束后，現(xiàn)場(chǎng)師生進(jìn)行了踴躍提問(wèn)，如如何看待最近的波音737-MAX自動(dòng)駕駛功能異常；智能化算法愈加復(fù)雜的情況下，如何保證機(jī)器學(xué)習(xí)的安全性；采用何種模型來(lái)規(guī)約“知識(shí)”，以及未來(lái)實(shí)現(xiàn)實(shí)時(shí)自動(dòng)系統(tǒng)的關(guān)鍵是什么等問(wèn)題，Joseph Sifakis都給予了耐心細(xì)致的回答。
大師與師生的對(duì)話(huà)：
計(jì)算機(jī)科學(xué)與軟件工程學(xué)院客座教授Jean Raymond Abrial院士提問(wèn)
計(jì)算機(jī)科學(xué)與軟件工程學(xué)院客座教授Jean Raymond Abrial院士（2016年國(guó)家國(guó)際科技合作獎(jiǎng)和2018年政府友誼獎(jiǎng)獲得者）：最近關(guān)于波音737-MAX自動(dòng)駕駛功能異常，使用您的通用計(jì)算模型是否可以解決或者處理這個(gè)問(wèn)題？如何從科學(xué)和經(jīng)濟(jì)學(xué)的角度來(lái)考量這個(gè)問(wèn)題？
Joseph Sifakis：這是個(gè)非常好的問(wèn)題。從已有先例來(lái)看，如今工程師在設(shè)計(jì)系統(tǒng)時(shí)較少考慮人和系統(tǒng)的交互，這是個(gè)非常重要的問(wèn)題。在自動(dòng)系統(tǒng)中，要通過(guò)人和系統(tǒng)的合作共同完成同一個(gè)任務(wù)。系統(tǒng)可以整合復(fù)雜的場(chǎng)景信息，然后將控制權(quán)交給人。有些人認(rèn)為與其關(guān)注人和系統(tǒng)共同控制的自動(dòng)駕駛（自動(dòng)化級(jí)別較低的駕駛），還不如全自動(dòng)駕駛。在未來(lái)，如果人們都擁有全自動(dòng)車(chē)輛，處理起來(lái)更簡(jiǎn)單，我也認(rèn)為的確如此。
計(jì)算機(jī)科學(xué)與軟件工程學(xué)院馬利莊教授提問(wèn)
計(jì)算機(jī)科學(xué)與軟件工程學(xué)院馬利莊教授（國(guó)家杰出青年科學(xué)基金獲得者）：我們正在做關(guān)于智能機(jī)器的研究，也和自動(dòng)駕駛緊密相關(guān)。自動(dòng)駕駛很復(fù)雜，需要越來(lái)越智能的算法，并且要求它可以自修改，而算法也越來(lái)越復(fù)雜，怎么保證它的安全性？
Joseph Sifakis：這也是我講座中最原始的問(wèn)題，正是因?yàn)橄到y(tǒng)有越來(lái)越多危險(xiǎn)因素，所以要把大型的問(wèn)題分解成子問(wèn)題來(lái)解決，就像智能體架構(gòu)圖所展示的認(rèn)知模塊，反映模塊等模塊，系統(tǒng)輸入通過(guò)多個(gè)模塊得到輸出。我的看法是，我們需要機(jī)器學(xué)習(xí)方法，去探測(cè)和分類(lèi)信息，以在決策中保證安全。
計(jì)算機(jī)科學(xué)與軟件工程學(xué)院黨委副書(shū)記兼副院長(zhǎng)曹桂濤：我想代表學(xué)生問(wèn)您一些問(wèn)題，要如何找到自己感興趣的領(lǐng)域？以何種態(tài)度對(duì)待科研才能提升我們的科研能力，甚至像您這樣獲得圖靈獎(jiǎng)呢？
Joseph Sifakis：實(shí)際與理論脫節(jié)是有一定的危險(xiǎn)的，尤其在高校當(dāng)中更存在危險(xiǎn)。有人認(rèn)為軟件工程與計(jì)算機(jī)科學(xué)之間關(guān)系不大，但其實(shí)不是這樣。如果你和如今的軟件工程師交流，你就會(huì)發(fā)現(xiàn)他們對(duì)程序間的差異并不十分了解。在企業(yè)界，開(kāi)發(fā)系統(tǒng)往往十分迅速，較為倉(cāng)促。而對(duì)我來(lái)說(shuō)，系統(tǒng)工程及軟件工程中一個(gè)極其重要的觀(guān)念就是要能確認(rèn)，任何好的系統(tǒng)都需要建立在一個(gè)好的架構(gòu)之上。學(xué)生應(yīng)該要學(xué)會(huì)如何設(shè)計(jì)好的結(jié)構(gòu)，當(dāng)然這需要大量的、持續(xù)的練習(xí)。我認(rèn)為對(duì)當(dāng)今學(xué)生們而言，他們所面臨的挑戰(zhàn)不是如何成為一個(gè)好的程序設(shè)計(jì)員，而是如何成為一個(gè)好的系統(tǒng)工程師。
計(jì)算機(jī)科學(xué)與軟件工程學(xué)院李欽副教授提問(wèn)
計(jì)算機(jī)科學(xué)與軟件工程學(xué)院李欽副教授：您采用哪種模型來(lái)規(guī)約知識(shí)（knowledge）？
Joseph Sifakis：首先要清楚什么是知識(shí)，知識(shí)有哪些類(lèi)型。典型的知識(shí)是一些假設(shè)，用來(lái)解釋知識(shí)；而數(shù)學(xué)意義上的知識(shí)是更高層次的知識(shí)，對(duì)于知識(shí)的認(rèn)知，類(lèi)似于“我知道一個(gè)事實(shí)”。機(jī)器學(xué)習(xí)的知識(shí)是介于典型知識(shí)和認(rèn)證過(guò)的知識(shí)之間。它的問(wèn)題在于，AI系統(tǒng)可以預(yù)估一些可能現(xiàn)象，但是難以解釋它是如何得出結(jié)論的，這是個(gè)黑盒（Black Box）問(wèn)題。
計(jì)算機(jī)科學(xué)與軟件工程學(xué)院張民副教授：您以為形式化方法在自治系統(tǒng)的開(kāi)發(fā)中應(yīng)起到什么樣的作用，自治系統(tǒng)的可靠性需要什么樣的新的形式化方法？
Joseph Sifakis：首先我們應(yīng)該回答什么是形式化方法。形式化方法是驗(yàn)證模型是否滿(mǎn)足某種特性，而自治系統(tǒng)或者智能系統(tǒng)的特點(diǎn)是沒(méi)有模型，沒(méi)有模型，我們能驗(yàn)證什么呢，基本是沒(méi)有希望的。我們需要找到目標(biāo)系統(tǒng)的一些基本規(guī)律，才能理解這個(gè)黑盒的行為，在一定程度上可以提高其可解釋性。
計(jì)算機(jī)科學(xué)與軟件工程學(xué)院博士一年級(jí)學(xué)生許巾一提問(wèn)
許巾一（計(jì)算機(jī)科學(xué)與軟件工程學(xué)院博士一年級(jí)學(xué)生）：您認(rèn)為異構(gòu)計(jì)算，算法優(yōu)化，和將來(lái)可能到來(lái)的計(jì)算機(jī)體系結(jié)構(gòu)革命，三者中哪一種會(huì)成為未來(lái)實(shí)現(xiàn)實(shí)時(shí)自主系統(tǒng)的關(guān)鍵？
Joseph Sifakis：要設(shè)計(jì)控制目標(biāo)與時(shí)間的自動(dòng)控制器，問(wèn)題有兩個(gè)，第一個(gè)是如何管理目標(biāo)以找到最佳可行目標(biāo)，需要選擇目標(biāo)并制定方案，來(lái)確定如何解決問(wèn)題。第二個(gè)是對(duì)于優(yōu)化問(wèn)題，要有經(jīng)過(guò)計(jì)算的方案。如果有了方法，那么對(duì)于GPU就需要一個(gè)媒介來(lái)告訴你可以使用快速計(jì)算設(shè)備進(jìn)行加速，例如FPGA。但這樣的實(shí)時(shí)操作會(huì)造成一些問(wèn)題，谷歌的技術(shù)員們也一直在進(jìn)行研究，尋求最佳解決方案。這往往需要長(zhǎng)時(shí)間的訓(xùn)練，但一旦對(duì)系統(tǒng)進(jìn)行訓(xùn)練，實(shí)時(shí)響應(yīng)就沒(méi)有問(wèn)題了。
王宏澤（計(jì)算機(jī)科學(xué)與軟件工程學(xué)院學(xué)生）：關(guān)于自動(dòng)駕駛系統(tǒng)，目前主流的方法是基于深度學(xué)習(xí)的。然而也有一些團(tuán)隊(duì)致力于使用形式化方法來(lái)實(shí)現(xiàn)自動(dòng)駕駛系統(tǒng)。請(qǐng)問(wèn)您如何看待這種基于形式化的方法？您認(rèn)為他們能夠成功嗎？
Joseph Sifakis：基于形式化方法實(shí)現(xiàn)自動(dòng)駕駛系統(tǒng)的努力是值得肯定的，有價(jià)值的。但是我們應(yīng)該結(jié)合深度學(xué)習(xí)和形式化方法。如果能夠擁抱AI，我覺(jué)得他們會(huì)成功的。
圖｜陳勵(lì) 文｜計(jì)算機(jī)科學(xué)與軟件工程學(xué)院 郭文君 來(lái)源｜計(jì)算機(jī)科學(xué)與軟件工程學(xué)院
編輯｜彭佳 編審｜郭文君
