Towards Trustworthy AI Agents: Integrating Large Language Models with Formal Methods

报告摘要: Large Language Models (LLMs) have emerged as a transformative AI paradigm, profoundly influencing broad aspects of daily life. Despite their remarkable performance, LLMs exhibit a fundamental limitation: hallucination—the tendency to produce misleading outputs that appear plausible. This inherent unreliability poses significant risks, particularly in high-stakes domains where trustworthiness is essential. 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. These methods have been widely employed in mission-critical domains such as aerospace, defense, and cybersecurity. However, the broader adoption of FMs remains constrained by significant challenges, including steep learning curves, limited scalability, and difficulties in adapting to the dynamic requirements of 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. LLMs offer adaptability and human-like reasoning but lack formal guarantees of correctness and reliability. FMs provide rigor but need enhanced accessibility and automation to support broader adoption from LLMs.

报告人简介: Yedi Zhang obtained her Ph.D. in 2023 from ShanghaiTech Univeristy, where her research focused on the formal verification of neural networks and received the CCF outstanding doctoral dissertation award in formal methods. After that, she joined National University of Singapore, Singapore, as a postdoc to continue on verification and validation of AI systems. Her current research explores the integration of formal methods with large language methods to advance the development of trustworhty AI agents. She serves and has served as a program committee member or reviewer for various conferences/journals (e.g., CAV, FAC, ATVA, TASE, ICSE, TOSEM, APSEC, ICLR, NeurIPS, ACM MM) in the fields of formal methods, software engineering, and artificial intelligence. More infomration at: https://zhangyedi.github.io/.