上科大江智浩團隊研究成果讓智能輔助軟件更“懂”你

隨著計算機科學的進步，智能軟件擁有了在復雜環(huán)境中自主做出決策的能力，可在減輕人類專家負擔的同時提升工作效率。但在醫(yī)療、交通等領域，由于問題的復雜性以及對安全的重視，智能軟件還無法完全取代人類專家。在上述領域中的智能軟件應保證人-機-物的三元融合，即領域?qū)＜遥ㄈ耍┰谥悄苘浖�（機）的輔助下解決復雜問題（物）。智能軟件如何利用其嚴謹性以及高算力承擔人類專家不擅長的工作，并為領域?qū)＜姨峁┚哂锌山忉屝缘妮o助是人-機-物三元融合系統(tǒng)的核心問題。上科大信息學院江智浩團隊利用形式化方法保證智能軟件的正確性，并使用數(shù)字孿生技術(shù)集成領域知識，保證輔助的可解釋性，在智慧醫(yī)療、軟件工程等應用領域取得多項成果。

形式化工具降低交叉領域軟件驗證門檻

嵌入式軟件的開發(fā)屬于計算機領域與應用領域的交叉領域，如何讓應用領域?qū)＜以谌狈τ嬎銠C專業(yè)知識的情況下參與嵌入式軟件開發(fā)是一項重大的難題。模型驗證方法可在軟件開發(fā)早期對系統(tǒng)在不同環(huán)境狀況下的正確性進行形式化驗證，并通過提供反例的方式為軟件改進提供依據(jù)。在模型驗證中，系統(tǒng)所處的環(huán)境狀況由環(huán)境模型表示，該模型需要覆蓋所有可能的環(huán)境狀況，并在存在反例時保證反例的可解釋性。開發(fā)滿足以上條件的環(huán)境模型需要同時具備應用領域以及形式化方法兩個領域的知識，極大地限制了模型驗證方法在軟件開發(fā)中的應用。

江智浩團隊提出了一種領域無關(guān)的環(huán)境建模范式，并基于此范式開發(fā)抽象樹工具，將環(huán)境模型的形式化抽象與細化過程對用戶隱藏，使得應用領域?qū)＜遥ㄈ耍┛稍谌狈τ嬎銠C專業(yè)知識的情況下利用抽象樹工具（機）進行軟件驗證（物），在保證環(huán)境模型覆蓋度的同時得到具有可解釋性的反例。該成果極大地降低了模型驗證方法在嵌入式軟件開發(fā)過程中的應用門檻，可盡早為嵌入式軟件提供正確性保障。該成果以“Environment Modeling During Model Checking of Cyber-Physical Systems”為題在IEEE Computer作為封面文章發(fā)表。

上�？萍即髮W是論文唯一完成單位，信息學院2020級碩士研究生陳光耀為第一作者，信息學院助理教授江智浩為通訊作者。

圖 |（1）應用領域的專家提供常見環(huán)境狀況模型；（2）利用領域無關(guān)的抽象規(guī)則提升環(huán)境模型覆蓋度，建立抽象樹；（3）如有反例產(chǎn)生，則沿抽象樹對環(huán)境模型進行細化，為反例提供可解釋性；（4）領域?qū)＜铱筛鶕?jù)反例補充環(huán)境模型。

數(shù)字孿生技術(shù)提升診斷效率

在醫(yī)療領域，對病人狀況的診斷與評估主要依賴醫(yī)生的經(jīng)驗，在面對不確定性很高的復雜狀況時無法保證診斷的嚴謹性與準確性。如何開發(fā)智能輔助系統(tǒng)，在保證診斷過程嚴謹性的同時為醫(yī)生提供具有可解釋的診斷輔助成為一大難題。在傳統(tǒng)心臟射頻消融手術(shù)中，醫(yī)生通過放置于心臟內(nèi)的導管電極觀測心臟內(nèi)電信號的產(chǎn)生與傳導，并對病人的心臟狀況進行診斷。由于觀測有限，在診斷過程中可能存在多種可解釋歷史觀測的疑似心臟狀況。醫(yī)生需要“腦補”所有疑似心臟狀況，并通過對病人心臟進行電刺激來排除部分疑似心臟狀況，最終得到準確的診斷。診斷過程的準確性與耗時取決于醫(yī)生的經(jīng)驗，不利于射頻消融手術(shù)的普及。

江智浩團隊開發(fā)出基于模型的心臟射頻消融手術(shù)輔助系統(tǒng)，使用心臟電生理模型建立病人數(shù)字孿生，枚舉診斷過程中的疑似心臟狀況，為診斷結(jié)果提供可解釋性，并利用形式化方法保證診斷過程的嚴謹性。該輔助系統(tǒng)在手術(shù)過程中承擔計算機更擅長的枚舉與推理任務，并將推理結(jié)果以符合醫(yī)生專業(yè)知識的形式進行呈現(xiàn)，使醫(yī)生（人）在該輔助系統(tǒng)（機）的幫助下對病人的心臟狀況進行準確診斷（物），可有效地減輕醫(yī)生的推理負擔，推動射頻消融手術(shù)的普及。該成果以“Model-based Clinical Assist System for Cardiac Ablation”為題發(fā)表于Proceedings of the ACM/IEEE 12th International Conference on Cyber-Physical Systems (ICCPS '21)并獲最佳論文提名；同時以“基于模型的射頻消融手術(shù)輔助系統(tǒng)”為題獲得中國發(fā)明專利。

此項論文由上�？萍即髮W與美國卡內(nèi)基梅隆大學合作完成，上海科技大學作為第一完成單位，信息學院2018級碩士研究生吳雨桐為第一作者，信息學院助理教授江智浩為通訊作者。

圖 | 臨床輔助系統(tǒng)通過觀測病人心內(nèi)電信號建立多個病人數(shù)字孿生，代表所有可解釋歷史觀測的心臟狀況，并將診斷結(jié)果以電信號傳導路徑的方式進行可視化。在得到新觀測時利用新信息對數(shù)字孿生進行更新和排除，并通過對疑似心臟狀況的分析為醫(yī)生提供程序電刺激建議，以進一步區(qū)分心臟狀況。

論文鏈接：

https://網(wǎng)址未加載/10.1109/MC.2021.3087631

https://網(wǎng)址未加載/10.1145/3450267.3450539

圖 文 江智浩

排 版 朱珮瑄

編 輯 高 瑄

今天“分享”“點贊”“在看”了嗎？