基于大模型的需求描述到形式化规约生成初探 (A Preliminary Study on the Generation of Formal Specifications from Requirements Description Based on Large Language Model）

Abstract

随着形式化方法在软件质量保证过程中的重要性日益凸显，将自然语言描述转化为形式化规约、最终完成形式化验证的自动化过程成为了一个关键的研究课题。本报告初步探讨了基于大语言模型的从自然语言描述到形式化规约生成、最后到验证的自动化转换流程，旨在缩小需求描述与形式化规约之间的鸿沟。我们首先探索了大语言模型如ChatGPT-3.5、通义千问、DeepSeek、StarCoder等在形式化规约生成上的初始能力，并探索提示工程 (prompt engineering) 及上下文学习(in-context learning) 的提升上限。接着通过小样本学习（few-shot learning）及思维链（Chain-of-Thought）等方式进行尝试，识别出更利于规约生成的识别方式。最后，我们构建了1000+高质量的“描述-规约”对，通过对DeepSeek进行监督微调（Supervised Fine-Tuning），使得微调后的模型在两种规约语言生成上达到显著提升。最后，通过一系列案例研究，我们展示了大语言模型在捕捉自然语言描述的语义及生成符合形式化验证标准的规约方面的潜力。此外，报告还讨论了在转换过程中面临的挑战，包括需求描述中的歧义解析、转换准确性的验证等。最后，我们展望了基于大语言模型的需求到规约生成技术的未来挑战及发展方向。

Dr. Jialun, CAO (Bella)

Research Assistant Professor

Jialun’s research interests lie in SE4AI and AI4SE, trustworthy AI, LLM4SE.