PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, Lei Bu

arXiv:2401.08807v5cs.SE

TL;DR

Template-based tools struggle to capture complex program behavior, while manually writing comprehensive formal specifications is difficult. SpecGen combines LLM conversation with mutation and heuristic selection, and generates verifiable specifications for 279 of 385 programs while outperforming the compared baselines. Its evaluation datasets may carry data-leakage risk.

Abstract

from arXiv · show

Formal program specifications play a crucial role in various stages of software development. However, manually crafting formal program specifications is rather difficult, making the job time-consuming and labor-intensive. It is even more challenging to write specifications that correctly and comprehensively describe the semantics of complex programs. To reduce the burden on software developers, automated specification generation methods have emerged. However, existing methods usually rely on predefined templates or grammar, making them struggle to accurately describe the behavior and functionality of complex real-world programs. To tackle this challenge, we introduce SpecGen, a novel technique for formal program specification generation based on Large Language Models. Our key insight is to overcome the limitations of existing methods by leveraging the code comprehension capability of LLMs. The process of SpecGen consists of two phases. The first phase employs a conversational approach that guides the LLM to generate appropriate specifications for a given program. The second phase, designed for where the LLM fails to generate correct specifications, applies four mutation operators to the model-generated specifications and selects verifiable specifications from the mutated ones through a novel heuristic selection strategy. We evaluate SpecGen on two datasets, including the SV-COMP Java category benchmark and a manually constructed dataset. Experimental results demonstrate that SpecGen succeeds in generating verifiable specifications for 279 out of 385 programs, outperforming the existing purely LLM-based approaches and conventional specification generation tools like Houdini and Daikon. Further investigations on the quality of generated specifications indicate that SpecGen can comprehensively articulate the behaviors of the input program.

I. INTRODUCTION

SpecGen uses LLM code comprehension to address the difficulty of generating comprehensive formal specifications for complex programs. It combines conversational generation with mutation and heuristic selection, and its evaluation reports more verifiable specifications than the compared baselines.

I. INTRODUCTION

  • SpecGen first uses conversation to generate specifications, then applies mutation-based generation when the LLM fails to produce verifiable results.The conversation begins with few-shot examples and uses verifier failures as feedback; the mutation phase applies four operators and heuristically selects variants for verification.Source: §I · pp. 1–2
  • 279 of 385 programs received verifiable specifications, compared with 247 for AutoSpec and 98 for Houdini.The evaluation also reports that SpecGen significantly outperformed the baseline methods.Source: §I · p. 2
  • The mutation-based approach enriches LLM output with mutation operators and heuristic selection intended to improve verification efficiency.The heuristic repeatedly selects promising mutated variants until verification succeeds.Source: §I · p. 2
  • SpecGenBench adds programs with expert-written specifications to complement the established SV-COMP benchmark.The manually constructed dataset contains 120 Java programs.Source: §I · p. 2

II. BACKGROUND AND MOTIVATION

The section introduces formal specifications and template-based generation, illustrates the limits of those tools on a nested-loop example, and outlines SpecGen’s two-part workflow.

A. Specification Generation and Verification

  • Formal specifications express intended or actual program behavior; Java examples include JML preconditions, postconditions, and loop invariants.Houdini and Daikon generate candidate specifications from expert-defined templates, which a verifier or runtime checking filters.Source: A. Specification Generation and… · p. 2

B. Motivation

  • For TwoSum, Houdini and Daikon produce trivial constraints that do not capture the nested-loop program’s functionality, while SpecGen generates comprehensive, verifiable specifications.The example includes method-level properties and loop invariants.Source: B. Motivation · p. 3

A. Overview

  • SpecGen pairs conversation-driven generation with mutation-based generation to handle programs for which the LLM does not produce verifiable specifications.The workflow uses verifier feedback during conversation, then mutates failed specifications and uses a heuristic selector to choose variants for verification.Source: A. Overview · p. 3

B. Conversation-Driven Specification Generation

SpecGen constructs an initial prompt from a system role, few-shot examples, and the queried program, then iteratively uses verifier feedback to refine generated specifications.

B. Conversation-Driven Specification Generation

  • The conversational approach is designed to help the LLM correct syntax errors and use verifier failure information to generate more accurate specifications.The process repeats until specifications pass verification or a maximum iteration limit is reached.Source: B. Conversation-Driven Specification… · pp. 3–4

1) Initial Prompt Construction:

  • The initial prompt combines a system role describing JML generation, few-shot program-specification examples, and the queried program.Examples are randomly selected from the collected dataset and are intended to support accurate outputs and the desired format.Source: 1) Initial Prompt Construction · p. 4

2) Conversational Specification Generation:

  • After a failed verification, the verifier’s error message becomes the next prompt, with matching natural-language guidance for recognized failure types.The verifier is configured to report one failure message per attempt; iterations continue until success or the maximum is reached.Source: 2) Conversational Specification… · p. 4

C. Mutation-based Specification Generation

SpecGen mutates unverifiable LLM-generated specifications to produce variants, then uses verification-guided selection to retain verifiable specifications. Its mutation operators target fine-grained relationships between variables, where LLMs can make mistakes.

C. Mutation-based Specification Generation

  • SpecGen applies mutation to specifications that fail verification after multi-round conversation, generating diverse candidate variants.The authors motivate this phase by observing that LLM outputs can be close to the oracle despite failing verification.Source: C. Mutation-based Specification… · pp. 4–5
  • MutationBasedGen takes failed template specifications Et and mutation operators M, and produces candidate specifications through SpecMutation.Each operator is applied to a template specification to obtain a set of mutated candidates Emutated.Source: C. Mutation-based Specification… · p. 5
  • The selector iteratively replaces refuted specifications with mutated variants from the same template family until all selected candidates verify or the set becomes empty.If every candidate is refuted, the process terminates with an empty selected set.Source: C. Mutation-based Specification… · p. 5

1) Template Specification Mutation:

  • Four mutation families—predicative, logical, comparative, and arithmetic—replace operators with alternatives of the same type.The design targets operator mistakes in fine-grained relationships between variables; combinations of mutation types can be applied together.Source: 1) Template Specification Mutation · p. 5
  • The mutation process can exhaust combinations of operator changes, such as changing a comparison and arithmetic expression together.For example, x < n + 1 can become x <= n - 1 through combined comparative and arithmetic mutations.Source: 1) Template Specification Mutation · p. 5

2) Mutated Specification Selection:

The selection heuristic prioritizes mutated specifications by a weighted score of the operators used to create them. It addresses the verification burden of checking the large candidate sets produced by exhaustive mutation.

2) Mutated Specification Selection:

  • The heuristic is intended to improve verification stability and efficiency because exhaustive mutation creates large candidate sets that burden the verifier.The paper contrasts this burden with Houdini’s practice of verifying generated specifications together.Source: 2) Mutated Specification Selection · p. 5
  • The heuristic selects the candidate with the highest score within a family of mutations derived from one template specification.The family is denoted Ef, the originating template et, and the mutation set M.Source: 2) Mutated Specification Selection · pp. 5–6
  • Each candidate’s score sums the number of times each mutation was applied, multiplied by that mutation’s weight.The score prioritizes candidates according to the mutation types and counts used to derive them.Source: 2) Mutated Specification Selection · pp. 5–6

IV. EXPERIMENTAL SETUP

The evaluation is organized around four questions: baseline performance, mutation effectiveness, candidate-selection efficiency, and the semantic content of generated specifications.

IV. EXPERIMENTAL SETUP

  • RQ1 asks how SpecGen compares with the baseline approaches.This frames the evaluation’s overall comparison question.Source: §IV · p. 6
  • RQ2 asks how each mutation type contributes to SpecGen’s effectiveness.This isolates the contribution of mutation types.Source: §IV · p. 6
  • RQ3 asks how candidate-selection strategies affect SpecGen’s efficiency.This focuses on selection strategy and efficiency.Source: §IV · p. 6
  • RQ4 asks how much semantic information about the input program appears in generated specifications.This examines specification content relative to program semantics.Source: §IV · p. 6

A. Implementation

The implementation uses GPT-3.5 Turbo with iterative prompting and OpenJML verification, alongside fixed mutation weights and a bounded verification timeout.

A. Implementation

  • GPT-3.5-turbo-1106 runs at temperature 0.4 with four few-shot examples and up to 10 conversation rounds.The temperature is set to balance output diversity and rigorousness.Source: A. Implementation · p. 6
  • OpenJML verifies specifications, with each verification limited to 30 minutes because of implementation incompleteness.The timeout is intended to avoid unexpected situations such as a non-responding verifier.Source: A. Implementation · p. 6
  • Comparative, logical, arithmetic, and predicative mutation weights are set to -1, -2, -4, and -4, respectively.The negative weights prioritize candidates with fewer mutations; experiments ran on an 8-core workstation with 32GB RAM.Source: A. Implementation · p. 6

B. Dataset

The evaluation uses a modified SV-COMP Java dataset and a complementary benchmark spanning varied control-flow structures; it compares SpecGen with conventional and LLM-based approaches.

B. Dataset

  • SV-COMP includes 265 Java classes, but 88.7% are loop-free, limiting coverage of more complex program structures.Programs were minimally modified for compilation and execution while preserving semantics; their average size is 22.51 LoC and cyclomatic complexity is 6.18.Source: B. Dataset · p. 6
  • SpecGenBench adds 120 programs across five control-flow categories, including branches, single-path loops, multi-path loops, and nested loops.The five categories contain 26, 23, 24, 26, and 21 programs, respectively; the benchmark averages 20.77 LoC and cyclomatic complexity 6.60.Source: B. Dataset · p. 6
  • For 100 LeetCode programs, three formal-verification experts wrote verifiable specifications, with another expert selecting the ground truth when multiple versions were available.The dataset also includes 20 programs and specifications from Nilizadeh et al..Source: B. Dataset · pp. 6–7

C. Baselines

  • The baselines include Houdini and Daikon, plus few-shot, conversational, and AutoSpec LLM-based approaches.Few-shot settings use 0, 2, or 4 examples; conversational generation iteratively refines results using verifier-error feedback, while AutoSpec decomposes programs and validates combined specifications.Source: C. Baselines · p. 7

D. Evaluation Metrics

The section defines evaluation metrics and reports SpecGen's benchmark performance, reliability, and verifier-call trade-offs. Across both datasets, it handles the most programs among the compared approaches.

D. Evaluation Metrics

  • Number of Passes counts programs whose generated specifications pass verification; other metrics measure LLM success probability, verifier calls, and semantic quality ratings.The user-rating measure uses a one-to-five Likert scale.Source: D. Evaluation Metrics · p. 7

A. RQ1: Comparison with Baselines

  • On SV-COMP, SpecGen handled 179 programs, compared with 146 for conversational generation and 94 for 4-shot LLM; AutoSpec handled 10 more than the conversational approach.Houdini handled 56 programs, while even 0-shot LLM handled 81.Source: A. RQ1: Comparison with Baselines · pp. 7–8, Table II · p. 8
  • 279 of 385 programs had verifiable specifications from SpecGen, more than Daikon (72), Houdini (98), conversational generation (218), or AutoSpec (247).SpecGen also had the highest success probability among LLM-based approaches.Source: Table II · p. 8, A. RQ1: Comparison with Baselines · p. 8
  • SpecGen's overall success probability was 59.97%, versus 35.95% for conversational generation and 46.13% for AutoSpec.Each LLM-based approach was tested 10 times per program.Source: A. RQ1: Comparison with Baselines · p. 8
  • SpecGen uniquely produced verifiable specifications for seven SpecGenBench programs, including five nested-loop and two single-path-loop programs.The paper describes these programs as relatively complicated and challenging to handle.Source: Figure 5 · p. 8, A. RQ1: Comparison with Baselines · p. 8
  • The conversational approach averaged 7.07 verifier calls per execution, compared with 16.19 for AutoSpec and 15.51 for SpecGen.Under the study's settings, the authors report that AutoSpec and SpecGen used more calls to filter results and produce more reliable results.Source: A. RQ1: Comparison with Baselines · p. 8

B. RQ2: Ablation Study on Mutation Types

SpecGen generated verifiable specifications for 279 of 385 programs, with comparative mutations contributing most to performance. Heuristic selection reduced verifier calls, particularly on SpecGenBench and programs with loops.

B. RQ2: Ablation Study on Mutation Types

  • 279/385 programs were verifiable with SpecGen; disabling comparative mutations reduced this to 223, the largest ablation drop, followed by logical mutations at 235.Disabling predicative and arithmetic mutations yielded 259 and 262 programs, respectively.Source: B. RQ2: Ablation Study on Mutation Types · p. 9
  • Comparative mutations matter especially for loop scope bounds, while predicative mutations help with nested-loop specifications involving complex quantifiers.Comparative ablation reduced coverage most in single-path, multi-path, and nested-loop programs; predicative ablation also hurt nested-loop coverage.Source: B. RQ2: Ablation Study on Mutation Types · p. 9

C. RQ3: Effectiveness of Selection Strategy

  • For programs that successfully generated verifiable specifications, five-run averages show heuristic selection used 8.91 versus random’s 9.41 calls on SV-COMP (5.30% improvement) and 28.51 versus 36.20 on SpecGenBench (21.23%).Source: C. RQ3: Effectiveness of Selection… · p. 9
  • Heuristic selection shows larger gains for loop programs, where generating verifiable specifications typically requires more iterations.The authors report smaller improvements for sequential and branched programs, where conversational generation is more efficient.Source: C. RQ3: Effectiveness of Selection… · p. 9

D. RQ4: User Study on the Quality of Specifications

In a 15-program user study, SpecGen’s specifications received ratings close to the oracle and above Houdini and Daikon. On Defects4J programs, SpecGen generated verifiable specifications for 38 of 50 files.

D. RQ4: User Study on the Quality of Specifications

A. Performance on Real-world Programs

  • 38/50 Defects4J files were handled by SpecGen, with an average success probability of 55.20%.The 50 files came from 9 repositories; ground-truth specifications were not prepared for this verifiability evaluation.Source: A. Performance on Real-world Programs · p. 10

B. Threats to Validity

The authors identify prompt sensitivity, possible data leakage, verifier flaws, and potential bias in expert-written specifications as validity threats. They position SpecGen among prior specification-generation work and conclude that it outperforms baselines on two datasets.

B. Threats to Validity

  • Prompt choices may affect results; possible data leakage applies to SV-COMP and 20 borrowed programs, while OpenJML flaws may reject correct specifications.The authors also identify potential bias in hand-written expert specifications.Source: B. Threats to Validity · pp. 10–11

VII. RELATED WORK

  • Prior LLM specification work combines static analysis [21], fine-tuning, or invariant ranking [69]; SpecGen pairs conversational generation with mutation enhancement.The authors note that some prior artifacts or specification grammars could not be included in their comparisons.Source: §VII · p. 11

VIII. CONCLUSION

  • Across SV-COMP Java and a manually constructed 120-program dataset, the authors report that SpecGen outperforms baseline approaches and articulates program behaviors.Source: §VIII · p. 11
Loading 2401.08807v5…