Improving Dynamic Specification Inference with LLM-Generated Counterexamples

TL;DR

This paper leverages large language models to generate counterexamples that improve the accuracy of dynamically inferred software specifications, reducing false positives and increasing precision.

Contribution

It introduces a novel approach using LLM-generated counterexamples to enhance dynamic specification inference, addressing test suite limitations.

Findings

LLMs can generate effective counterexamples that discard up to 11.68% of invalid assertions.

Incorporating LLM-generated counterexamples improves inference precision by up to 7%.

The approach maintains recall while reducing false positives.

Abstract

Contract assertions, such as preconditions, postconditions, and invariants, play a crucial role in software development, enabling applications such as program verification, test generation, and debugging. Despite their benefits, the adoption of contract assertions is limited, due to the difficulty of manually producing such assertions. Dynamic analysis-based approaches, such as Daikon, can aid in this task by inferring expressive assertions from execution traces. However, a fundamental weakness of these methods is their reliance on the thoroughness of the test suites used for dynamic analysis. When these test suites do not contain sufficiently diverse tests, the inferred assertions are often not generalizable, leading to a high rate of invalid candidates (false positives) that must be manually filtered out. In this paper, we explore the use of large language models (LLMs) to automatically generate tests that attempt to invalidate generated assertions. Our results show that state-of-the-art LLMs can generate effective counterexamples that help to discard up to 11.68\% of invalid assertions inferred by SpecFuzzer. Moreover, when incorporating these LLM-generated counterexamples into the dynamic analysis process, we observe an improvement of up to 7\% in precision of the inferred specifications, with respect to the ground-truths gathered from the evaluation benchmarks, without affecting recall.