LLM-generated specifications can mislead software verification results
Are LLM-Generated Formal Specifications Faithful to Their Requirements? A Study on Bimodal Formal Specification Generation
Software EngineeringProgramming Languages
Summary
Checking if software matches its requirements is very important but hard. This paper looks at how large language models (LLMs) create formal software rules from both the code and the written requirements. The authors found that when code is correct, adding requirements doesn't help generate better rules. But if the code is wrong, these AI-generated rules might wrongly say everything is fine. This means current AI methods might not reliably ensure software really meets its requirements.
What this means in practice
- •For software verification teams: Identify limitations in AI-generated formal specifications that could cause false positives during software correctness checking.
- •For software testing teams: Use findings to improve specification generation practices when checking software against requirements to avoid being misled by weak AI outputs.
Authors
Wenhan Wang, Shiming Chen, Zeyu Sun, Shenghua Feng
Abstract
Formal specification generation is a critical step towards formal verification and correctness assurance of software. Recently, large language models have been widely adopted in automatic generation of formal specifications. However, existing LLM-based specification generation approaches often assume that the input program is correct, which deviates from the real purpose of formal verification---to figure out whether the program meets its requirements when its correctness is unknown. Therefore, we conduct an empirical study of LLM-based specification generation under the bimodal setting: given both the natural language requirement and its corresponding code implementation, whose correctness is unknown. We construct a benchmark of 1,403 C programs and evaluate ACSL specification generation with Frama-C verification. Our study reaches several interesting findings: first, when the code implementation is correct, providing the natural language requirement does not further improve the pass rate of generated specifications. Second, when the code implementation is incorrect, LLM-based specification generation may erroneously pass verification by producing weak or implementation-misled specifications, and this cannot be fully alleviated by advanced prompting approaches. Compared with the non-formal HoarePrompt approach, LLM-generated formal specifications are less effective in predicting requirement-code consistency. Our study takes a first look at applying LLM-based formal specification generation to verifying program correctness against requirements, and points to requirement-faithful specification generation as a new direction for future LLM-based formal specification research.