11月13日，2013年圖靈獎獲得者、美國國家工程院院士、分布式系統(tǒng)與形式化方法奠基人萊斯利·蘭伯特（Leslie Lamport）博士應邀訪問學校，圍繞“分布式計算、形式化方法與人工智能的未來”主題，與學校師生及桂林地區(qū)高校、企業(yè)代表開展高水平學術交流。本次活動由學校主辦，吸引了來自桂林電子科技大學、廣西師范大學、桂林理工大學等高校的專家學者，以及桂林市貿促會、桂林國際商會和多家本地科技企業(yè)的技術骨干共同參與。座談會由副校長楊慶慶主持。

交流座談會現(xiàn)場

校長吳郭泉為此次座談會致辭。他指出，蘭伯特博士提出的邏輯時鐘、Paxos共識算法等成果，是現(xiàn)代互聯(lián)網(wǎng)、云計算和分布式系統(tǒng)的技術基石，其開發(fā)的LaTeX排版系統(tǒng)更是全球科研工作者廣泛使用的標準工具。吳郭泉表示，蘭伯特博士強調嚴謹邏輯與系統(tǒng)思維的研究理念，與學校培養(yǎng)“理論扎實、實踐能力強、具備系統(tǒng)工程素養(yǎng)”的高素質應用型人才目標高度契合。此次交流將為學校信息技術類專業(yè)建設、課程改革與科研方向凝練注入重要動力。

吳郭泉在座談會上講話

蘭伯特博士做主題分享

座談交流中，蘭伯特博士回顧了自己進入計算機科學領域的歷程，并重點介紹了其創(chuàng)立的TLA+形式化規(guī)約語言。他強調，在構建復雜系統(tǒng)（包括人工智能系統(tǒng)）之前，應通過數(shù)學化的形式化方法進行精確建模與驗證，以從源頭保障系統(tǒng)的正確性與可靠性。蘭伯特博士將抽象理論轉化為清晰的工程哲學，引導聽眾深入理解“用數(shù)學思維指導軟件設計”的核心價值?，F(xiàn)場師生踴躍提問，圍繞大語言模型能否輔助形式化驗證、AI系統(tǒng)的可解釋性與安全性、應用型高校如何融入形式化方法教學、復雜問題的分解策略等議題展開深入探討。蘭伯特博士一一耐心解答，其睿智、謙和且富有啟發(fā)性的回應贏得陣陣掌聲。

與會師生與蘭伯特博士進行交流

本次學術交流活動是學校拓展國際學術視野、營造濃厚科研育人氛圍的重要舉措。作為地方應用型本科高校，學校將持續(xù)推動前沿學術成果融入教育教學全過程，深化產教融合與科教融匯，不斷提升高素質應用型人才培養(yǎng)質量，為服務區(qū)域數(shù)字經濟與高質量發(fā)展貢獻力量。