Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SpecEval: Evaluating Code Comprehension in Large Language Models via Program Specifications

Lezhi Ma, Shangqing Liu, Lei Bu, Shangru Li, Yida Wang, Yang Liu

TL;DR

SpecEval introduces a black-box framework that evaluates code comprehension in large language models by representing program semantics with formal specifications, specifically using Java Modeling Language (JML). It defines four specification-focused tasks—Judgement, Selection, Infilling, and Generation—and incorporates counterfactual analysis with semantic-preserving perturbations to probe robustness across 204 Java programs and six LLMs. The results show that current LLMs have limited ability to articulate full program semantics via formal specs, with Judgement performing best and Infilling worst, and reveal notable sensitivity to identifier-related perturbations. The work demonstrates that few-shot prompting can improve performance and underscores the need for robust specification-based evaluation and tooling to enhance reliability in software engineering tasks guided by LLMs.

Abstract

Large Language models have achieved impressive performance in automated software engineering. Extensive efforts have been made to evaluate the abilities of code LLMs in various aspects, with an increasing number of benchmarks and evaluation frameworks proposed. Apart from the most sought-after capability of code generation, the capability of code comprehension is being granted growing attention. Nevertheless, existing works assessing the code comprehension capability of LLMs exhibit varied limitations. Evaluation frameworks like CRUXEval and REval usually focus on code reasoning tasks over a certain input case, leading to a limited range of execution traces covered, resulting in a loss in code semantics examined and the inability to assess the comprehensive understanding of LLMs concerning the target program. To tackle these challenges, we propose SpecEval, a novel black-box evaluation framework to evaluate code comprehension in LLMs via program specifications. Inspired by the idea that specifications can act as a comprehensive articulation of program behaviors concerning all possible execution traces, we employ formalized program specifications to represent program semantics and perform comprehensive evaluations. In particular, four specification-related tasks are designed meticulously to assess the capability of LLMs from basic to advanced levels. Counterfactual analysis is further conducted to study the performance variance of LLMs under semantics-preserving perturbations. Systematic experiments are conducted on six state-of-the-art LLMs. Extensive experimental results present a below-satisfactory performance of LLMs on specification-related tasks, revealing the limitations of existing LLMs in terms of articulating program semantics with formal specifications. Counterfactual analysis also reveals the sensitivity of LLMs towards semantic-preserving perturbations.

SpecEval: Evaluating Code Comprehension in Large Language Models via Program Specifications

TL;DR

SpecEval introduces a black-box framework that evaluates code comprehension in large language models by representing program semantics with formal specifications, specifically using Java Modeling Language (JML). It defines four specification-focused tasks—Judgement, Selection, Infilling, and Generation—and incorporates counterfactual analysis with semantic-preserving perturbations to probe robustness across 204 Java programs and six LLMs. The results show that current LLMs have limited ability to articulate full program semantics via formal specs, with Judgement performing best and Infilling worst, and reveal notable sensitivity to identifier-related perturbations. The work demonstrates that few-shot prompting can improve performance and underscores the need for robust specification-based evaluation and tooling to enhance reliability in software engineering tasks guided by LLMs.

Abstract

Large Language models have achieved impressive performance in automated software engineering. Extensive efforts have been made to evaluate the abilities of code LLMs in various aspects, with an increasing number of benchmarks and evaluation frameworks proposed. Apart from the most sought-after capability of code generation, the capability of code comprehension is being granted growing attention. Nevertheless, existing works assessing the code comprehension capability of LLMs exhibit varied limitations. Evaluation frameworks like CRUXEval and REval usually focus on code reasoning tasks over a certain input case, leading to a limited range of execution traces covered, resulting in a loss in code semantics examined and the inability to assess the comprehensive understanding of LLMs concerning the target program. To tackle these challenges, we propose SpecEval, a novel black-box evaluation framework to evaluate code comprehension in LLMs via program specifications. Inspired by the idea that specifications can act as a comprehensive articulation of program behaviors concerning all possible execution traces, we employ formalized program specifications to represent program semantics and perform comprehensive evaluations. In particular, four specification-related tasks are designed meticulously to assess the capability of LLMs from basic to advanced levels. Counterfactual analysis is further conducted to study the performance variance of LLMs under semantics-preserving perturbations. Systematic experiments are conducted on six state-of-the-art LLMs. Extensive experimental results present a below-satisfactory performance of LLMs on specification-related tasks, revealing the limitations of existing LLMs in terms of articulating program semantics with formal specifications. Counterfactual analysis also reveals the sensitivity of LLMs towards semantic-preserving perturbations.
Paper Structure (29 sections, 1 equation, 4 figures, 3 tables)

This paper contains 29 sections, 1 equation, 4 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Background and Motivation
  3. Program Specification
  4. Motivation
  5. Methodology
  6. Evaluation Tasks and Metrics
  7. Specification Correctness Judgement
  8. Specification Candidates Selection
  9. Specification Infilling
  10. Specification Generation
  11. Counterfactual Analysis
  12. Semantic-preserving Perturbations
  13. Evaluation Metrics
  14. experimental setup
  15. Benchmark Construction
  16. ...and 14 more sections

Figures (4)

  • Figure 1: An example program and corresponding ground-truth JML specification (highlighted in blue).
  • Figure 2: Illustrations for the semantic-preserving perturbations, including the original program, corresponding specifications, and all perturbed programs. The code and specifications modified by the perturbations are highlighted in blue.
  • Figure 3: The selection task for program FizzBuzz, the correct answer, and the options chosen by each model.
  • Figure 4: The infilling task for program IntSquare (both the Original and the Name Random category), along with the answers provided by GPT-3.5 and CodeLlama.