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