# SpecGen: Automated Generation of Formal Program Specifications via Large Language Models

**Authors:** Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, Lei Bu  
**arXiv:** [2401.08807](https://arxiv.org/abs/2401.08807)  
**Date:** 2024-01-16  
**Summary page:** https://www.summarizepaper.com/en/arxiv-id/2401.08807v1/

## Key points

- Formal program specifications are essential in software development to guide various stages of the development process.
- Manual creation of these specifications is challenging and labor-intensive, especially for complex programs.
- Automated methods like SpecGen leverage Large Language Models (LLMs) to generate formal program specifications efficiently.
- SpecGen uses a conversational approach in the first phase and mutation operators with a heuristic selection strategy in the second phase to enhance the quality and reliability of generated specifications.
- Experimental results show that SpecGen successfully generates verifiable specifications for a high percentage of test cases, surpassing existing approaches.

## Summary

, , , , 

In the realm of software development, formal program specifications are essential components that guide various stages of the development process. However, manual creation of these specifications is a challenging and labor-intensive task, particularly for complex programs requiring accurate and comprehensive descriptions of their semantics. To address this issue and alleviate the burden on software developers, automated methods for generating program specifications have emerged. One such innovative approach is SpecGen, which leverages Large Language Models (LLMs) to automate the generation of formal program specifications. Unlike existing methods that often struggle to accurately capture real-world program behavior and functionality due to reliance on predefined templates or grammars, SpecGen stands out by harnessing the code comprehension capabilities of LLMs. The process of SpecGen unfolds in two distinct phases. The first phase adopts a conversational approach to guide the LLM in generating appropriate specifications for a given program. This interactive method ensures that generated specifications align closely with the intended semantics and functionalities of the program under consideration. In instances where the LLM encounters challenges in producing correct specifications, the second phase comes into play. During this phase, four mutation operators are applied to manipulate model-generated specifications. A novel heuristic selection strategy is then employed to sift through these mutated versions and identify verifiable specifications by assigning varying weights based on their accuracy and relevance. Through this meticulous process, SpecGen aims to enhance the quality and reliability of generated formal program specifications. To evaluate its efficacy, a dataset comprising 120 test cases was manually constructed for testing SpecGen's performance. The experimental results showcase impressive outcomes, with SpecGen successfully generating verifiable specifications for 100 out of 120 programs. This success rate surpasses that achieved by existing purely LLM-based approaches and conventional specification generation tools. Furthermore, detailed investigations into the quality of generated specifications reveal that SpecGen excels in articulating the intricate behaviors exhibited by input programs comprehensively. Authored by Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu, "SpecGen: Automated Generation of Formal Program Specifications via Large Language Models" represents a significant advancement in automating formal program specification generation processes within software development contexts.