Title:   From Informal to Formal – Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs

Speaker:曹嘉伦（研究助理教授, 香港科技大学） 

Time: 2025年4月27日（周日），上午10:00  

Venue:中国科学院软件研究所5号楼3层334报告厅

Abstract:  As the role of formal methods in ensuring software quality becomes more critical, the automated transformation of natural language descriptions into formal specifications, followed by formal verification, has emerged as a vital area of research. This report delves into the process of automating this process using large language models (LLMs), with the goal of bridging the gap between requirement descriptions and formal specifications. Initially, we assessed the basic capabilities of LLMs in generating formal specifications. We investigated the limits of prompt engineering and in-context learning with these models. Subsequently, we explored more effective framework for specification generation employing in-context learning. We then created over 1,000 high-quality "description-specification" pairs and conducted supervised fine-tuning three open-sourced models, which notably enhanced its ability to generate formal specification languages. Through a series of case studies, we demonstrated the capacity of LLMs to comprehend the semantics of natural language descriptions and produce specifications that align with formal verification standards. Finally, the report addresses the challenges encountered in this conversion process, including the resolution of ambiguities in requirement. Looking forward, we anticipate further challenges and directions in the development of requirement-to-specification generation and modeling using LLMs.

 Bio: Dr. Jialun Cao is a Research Assistant Professor at the Hong Kong University of Science and Technology. Her main research areas include AI testing, AI4SE, and formal verification, etc. She received her Ph.D. from the Hong Kong University of Science and Technology under the supervision of Professor Shing-Chi Cheung. She received her master's degree from the State Key Laboratory of the Institute of Software, Chinese Academy of Sciences. She has published more than 20 papers in top conferences in the field such as ICSE, ESEC/FSE, CAV, ASE, USENIX Security and top journals such as TOSEM. She also serves as a reviewer for many top journals such as TSE and TOSEM and is also a program committee member of ICSE and FSE. She received an ACM Distinguished Paper Award, and was a receiver of Huawei Fellowship. She served as a member of the 2025 award committees for the three most prestigious awards in the field of international software engineering: the ACM SIGSOFT Outstanding Research Award, the ACM SIGSOFT Outstanding Service Award, and the ACM SIGSOFT Influential Educator Award. And she was the only shortlisted participant from the Hong Kong University of Science and Technology in the "Engineering Rising Stars Women" seminar at the 2024 Asian Deans' Forum.