清華學(xué)子面對(duì)面對(duì)話學(xué)術(shù)大師之
圖靈獲得者愛(ài)德蒙·克拉克做客“巔峰對(duì)話”
清華新聞網(wǎng)4月28日電（研通社記者 方 文 彭智軒 杜林霏） 4月25日下午，清華大學(xué)“巔峰對(duì)話”活動(dòng)第二場(chǎng)在信息科學(xué)技術(shù)大樓舉辦,， 2007年度圖靈獎(jiǎng)獲得者愛(ài)德蒙·克拉克教授“巔峰對(duì)話”,。
圖為愛(ài)德蒙·克拉克演講。研通社記者 王皓冉 攝
愛(ài)德蒙·克拉克簡(jiǎn)單介紹了自己的學(xué)術(shù)歷程和主要學(xué)術(shù)成果,。愛(ài)德蒙·克拉克本科期間從事數(shù)學(xué)科學(xué)專業(yè),，1967年從弗吉尼亞大學(xué)獲得數(shù)學(xué)學(xué)士學(xué)位。出于對(duì)計(jì)算機(jī)的酷愛(ài),，博士研究期間他選擇了另一個(gè)專業(yè)——計(jì)算機(jī)專業(yè),。本科期間的學(xué)習(xí)為后來(lái)的研究打下了堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)，從自己感興趣的領(lǐng)域——推理和可計(jì)算實(shí)數(shù)出發(fā),，他首先著手于實(shí)數(shù)的非線性問(wèn)題,。1981年，愛(ài)德蒙·克拉克與自己的博士生首次提出模型檢測(cè)的想法,，并用在自動(dòng)機(jī)并發(fā)系統(tǒng)的驗(yàn)證研究上,，主要使用SAT驗(yàn)證完成模型檢測(cè)，主要針對(duì)于有界模型,。然而從理論推導(dǎo)到實(shí)際工程應(yīng)用是有距離的,，因?yàn)閷?shí)際系統(tǒng)大多都是混合系統(tǒng)，尤其是數(shù)值方法直接的使用會(huì)出現(xiàn)許多錯(cuò)誤。為此,，愛(ài)德蒙教授的團(tuán)隊(duì)針對(duì)他們的思想開(kāi)發(fā)出了dReal實(shí)用工具,，該工具主要利用DPLL、間隔算法,、限制性算法等思想研究實(shí)際問(wèn)題,。實(shí)際中，信息物理系統(tǒng)是一個(gè)龐大的系統(tǒng),，對(duì)于系統(tǒng)安全性問(wèn)題的研究至關(guān)重要,。針對(duì)這一研究目標(biāo)，愛(ài)德蒙團(tuán)隊(duì)驗(yàn)證了卡普了猜想,，無(wú)人駕駛汽車,，心臟模擬仿真等問(wèn)題。
圖為同學(xué)們與愛(ài)德蒙·克拉克交流,。研通社記者 王皓冉 攝
學(xué)術(shù)報(bào)告結(jié)束后,，現(xiàn)場(chǎng)學(xué)生與愛(ài)德蒙·克拉克開(kāi)始“對(duì)話”環(huán)節(jié),。同學(xué)針對(duì)專業(yè)問(wèn)題,、科研心得等與愛(ài)德蒙·克拉克進(jìn)行了交流。
有同學(xué)對(duì)愛(ài)德蒙·克拉克提到的“空間爆炸”問(wèn)題非常感興趣,，愛(ài)德蒙·克拉克對(duì)此作了進(jìn)一步解釋,。他指出，“空間爆炸”可以理解成并行運(yùn)行過(guò)程中進(jìn)程突然被阻斷的過(guò)程,，這一過(guò)程在計(jì)算機(jī)應(yīng)用方面有廣泛應(yīng)用,，例如微軟設(shè)備驅(qū)動(dòng)就是一個(gè)例子。也有同學(xué)大膽質(zhì)疑,，愛(ài)德蒙·克拉克的模型檢測(cè)思想怎樣證明自身的正確性,，以及為什么應(yīng)用于軟件系統(tǒng)會(huì)比較困難。愛(ài)德蒙·克拉克解釋到,，自身正確性的檢驗(yàn)需要一定的抽象程度,，一般通過(guò)一些編譯器來(lái)自檢；而相比于硬件系統(tǒng),，軟件系統(tǒng)有較為復(fù)雜的數(shù)據(jù)結(jié)構(gòu),，因此會(huì)使得工作量較大。
與純學(xué)術(shù)的交流相比,，很多同學(xué)對(duì)于愛(ài)德蒙·克拉克的科研經(jīng)驗(yàn)非常感興趣,。關(guān)于如何保持對(duì)科研的積極心態(tài)，愛(ài)德蒙·克拉克說(shuō),，自己的性格里對(duì)于喜歡的東西有一種著了魔的熱情,，喜歡拼盡全力解決問(wèn)題；時(shí)間安排上會(huì)給科研工作留出充足的余量，避免自己過(guò)度陷入行政工作中,。對(duì)于如何訓(xùn)練自己的學(xué)生,，愛(ài)德蒙·克拉克強(qiáng)調(diào)了兩個(gè)詞：多自由度和適時(shí)引導(dǎo)。他會(huì)給自己的學(xué)生充足的自由環(huán)境,，在此基礎(chǔ)之上加以適度的引導(dǎo),，并著力培養(yǎng)他們專注于探索問(wèn)題的品質(zhì)。有同學(xué)問(wèn)到教授如何看待數(shù)學(xué)基礎(chǔ)訓(xùn)練的意義,，愛(ài)德蒙·克拉克給出這樣的回答：計(jì)算本身是一件令人興奮的事情,，數(shù)學(xué)則是做好計(jì)算機(jī)科學(xué)的關(guān)鍵，數(shù)學(xué)的各種算法本質(zhì)上是培養(yǎng)一種思維方式,，這對(duì)于本科生無(wú)疑是很好的一個(gè)專業(yè),。
圖為校研究生會(huì)主席劉博涵代表清華學(xué)子向愛(ài)德蒙·克拉克贈(zèng)送禮物。 研通社記者 王皓冉 攝
活動(dòng)結(jié)束前,，清華大學(xué)研究生會(huì)主席劉博涵代表同學(xué)向愛(ài)德蒙·克拉克贈(zèng)送了禮物,，愛(ài)德蒙·克拉克表示非常高興來(lái)到清華大學(xué)，有機(jī)會(huì)跟同學(xué)們近距離地交流,，他對(duì)清華的學(xué)生給予了高度評(píng)價(jià),，認(rèn)為清華人非常聰明和出色，合作意識(shí)也很好,，他希望還有機(jī)會(huì)與清華學(xué)生做更進(jìn)一步的交流,。
圖為活動(dòng)現(xiàn)場(chǎng)。 研通社記者 王皓冉 攝
活動(dòng)結(jié)束之后,，來(lái)自電子系的博士生毛洪亮表示,，愛(ài)德蒙·克拉克自身不論是為人還是學(xué)術(shù)都非常嚴(yán)謹(jǐn)，今天有幸聽(tīng)到教授的科研經(jīng)驗(yàn),，受益頗豐,；也有同學(xué)對(duì)愛(ài)德蒙·克拉克的坦承和寬容做出了高度評(píng)價(jià)，“當(dāng)我問(wèn)愛(ài)德蒙教授 ‘模型檢測(cè)’的局限性時(shí),，他說(shuō)這個(gè)思想不是萬(wàn)能的,，有很多領(lǐng)域的問(wèn)題還沒(méi)辦法以此解決；同時(shí)針對(duì)同行其他專家研究成果,，他的評(píng)述總是報(bào)以包容和支持的態(tài)度,。”也有同學(xué)表示在這一場(chǎng)論壇中收獲了很多前沿的知識(shí)，論壇氛圍非常自由,，通過(guò)大師的鼓勵(lì)獲得了很多正能量,，并表示學(xué)生學(xué)習(xí)要崇尚自主學(xué)習(xí)。
相關(guān)鏈接：
愛(ài)德蒙·克拉克（Edmund Clarke）生于1945年,，1967年從弗吉尼亞大學(xué)獲得數(shù)學(xué)學(xué)士學(xué)位,。1976年,，康奈爾大學(xué)計(jì)算機(jī)系獲得其博士學(xué)位。1981年,，他與自己的博士生Allen Emerson首次提出模型檢測(cè)（model checking）的想法并用在 自動(dòng)及并發(fā)系統(tǒng)的驗(yàn)證研究上,。2007年度圖靈獎(jiǎng)授予Edmund M.Clarke、E Allen Emerson和Joseph Sifakis三位科學(xué)家,，表彰他們開(kāi)發(fā)模型檢測(cè)技術(shù),，并使之成為一個(gè)廣泛應(yīng)用在硬件和軟件工業(yè)中非常有效的算法驗(yàn)證技術(shù)所做的奠基性貢獻(xiàn)。
編輯：范 麗
