时间：2025年6月18日（周三）10:00
地点：杨咏曼楼606会议室
报告内容：Large Language Models (LLMs) have emerged as a transformative AI paradigm, profoundly influencing broad aspects of daily life. However, despite their remarkable performance, LLMs exhibit a fundamental limitation: hallucination—the tendency to produce misleading outputs that appear plausible. This unreliability poses significant risks, particularly in high-stakes applications where trustworthiness is paramount. On the other hand, Formal Methods (FMs), which share foundations with symbolic AI, provide mathematically rigorous techniques for modeling, specifying, reasoning and verifying the correctness of systems. They have been extensively employed in mission-critical domains such as aerospace, defense, blockchain, and cybersecurity. However, FMs remain limited due to steep learning curves and challenges related to efficiency and adaptability in daily applications. To build trustworthy AI agents, we argue that the integration of LLMs and FMs is necessary to overcome the limitations of both paradigms. While LLMs offer adaptability, creativity and human-like reasoning, they need formal guarantees to ensure correctness and reliability. Conversely, FMs provide rigor but need enhanced accessibility and automation to support broader adoption.
报告人简介：Zhe Hou obtained his PhD from the Australian National University on the topic of automated reasoning for separation logic --- a logic for reasoning about the correctness of computer programs with pointers and other mutable data structures. In 2015, he joined Nanyang Technological University, Singapore, as a postdoc to work on formal verification of information flow security for instruction set architecture and weak memory models. He joined Griffith University, Australia, in 2017 on a project to develop trusted autonomous systems and advanced model checking techniques in collaboration with the Australian Defence Science and Technology. He joined the faculty of Griffith University in 2019. His research interests include logic, automated reasoning, formal methods, AI, sports analytics, blockchain, and quantum computing. More info at //zhehou.github.io/papers/.
