Source-linked AI summary
Can Large Language Models Write Good Property-Based Tests?
Vasudev Vikram, Caroline Lemieux, Joshua Sunshine, Rohan Padhye
TL;DR
Property-based testing remains relatively underused, and writing its input generators and meaningful assertions is challenging. This paper uses API documentation to prompt LLMs to generate and evaluate property-based tests, finding that GPT-4 with two-stage prompting achieves valid, sound tests in 2.4 samples on average and covers 21% of documented properties.
Problem
Property-based testing is relatively underused, and developers report difficulty writing random input generators and meaningful properties.
Source: §1 · p. 1Method
The authors prompt LLMs with API documentation to synthesize property-based tests and evaluate validity, soundness, and property coverage.
Source: §1 · p. 2, §3.2.3 · p. 6Results
GPT-4 with two-stage prompting produces valid and sound PBTs in 2.4 samples on average and covers 21% of documented properties.
Source: §8 · p. 11Takeaways & Limitations
LLM-based PBT generation is suitable for automating some of the tedious work of writing property-based tests.
Source: §1 · p. 3The authors do not know whether their conclusions generalize beyond Python or to other property-based testing libraries.
Source: §5.3 · p. 10
Abstract
from arXiv · showhide
Property-based testing (PBT), while an established technique in the software testing research community, is still relatively underused in real-world software. Pain points in writing property-based tests include implementing diverse random input generators and thinking of meaningful properties to test. Developers, however, are more amenable to writing documentation; plenty of library API documentation is available and can be used as natural language specifications for PBTs. As large language models (LLMs) have recently shown promise in a variety of coding tasks, we investigate using modern LLMs to automatically synthesize PBTs using two prompting techniques. A key challenge is to rigorously evaluate the LLM-synthesized PBTs. We propose a methodology to do so considering several properties of the generated tests: (1) validity, (2) soundness, and (3) property coverage, a novel metric that measures the ability of the PBT to detect property violations through generation of property mutants. In our evaluation on 40 Python library API methods across three models (GPT-4, Gemini-1.5-Pro, Claude-3-Opus), we find that with the best model and prompting approach, a valid and sound PBT can be synthesized in 2.4 samples on average. We additionally find that our metric for determining soundness of a PBT is aligned with human judgment of property assertions, achieving a precision of 100% and recall of 97%. Finally, we evaluate the property coverage of LLMs across all API methods and find that the best model (GPT-4) is able to automatically synthesize correct PBTs for 21% of properties extractable from API documentation.
1 INTRODUCTION
The introduction frames API documentation as a resource for automating property-based test generation, then presents LLM prompting and an evaluation framework for judging generated tests. Its reported results show that the best approach can produce valid, sound tests and cover over 20% of documented properties.
1 INTRODUCTION
- Developers report difficulty creating random input generators and meaningful properties, while PBT remains relatively underused despite its testing impact.The introduction notes that only 222 of 180,000 PyPI packages list Hypothesis as a dependency.Source: §1 · p. 1
- Their example translates numpy.cumsum documentation into random input generation and assertions about result size, shape, and the last element.The last-element assertion uses the documentation’s note that the result’s final value equals the sum of the input when the array is not floating-point.Source: §1 · p. 2, Figure 1 · p. 2, Figure 2 · p. 2
- The authors investigate prompting GPT-4, Claude-3-Opus, and Gemini-1.5-Pro with API documentation to synthesize property-based tests.They explore single-stage and two-stage prompting strategies.Source: §1 · pp. 1–2
- With the best-performing approach, valid and sound PBTs were synthesized in over 2.4 samples on average, and correct PBTs covered over 20% of documented properties.The introduction describes the evaluation across 40 API methods and two prompting strategies.Source: §1 · pp. 2–3
- The proposed evaluation considers validity, soundness, and completeness, introducing property coverage to assess detection of documented-property violations.The contributions also report manual comparison of the soundness metric with human judgment.Source: §1 · pp. 2–3
2 BACKGROUND
Section 2.1 frames property-based testing as checking program properties on generated inputs and illustrates how Hypothesis generators feed parametrized assertions. Section 2.2 describes pre-trained LLMs and their use through prompt engineering.
2.1 Property-based Testing
- Property-based testing checks whether program outputs satisfy desired properties across randomly generated inputs, rather than enumerating all possible inputs.The test combines a generator with a parametrized check; a property violation causes failure, but passing tests do not prove the absence of violations.Source: §2.1 · p. 3
- A Hypothesis test generates integer lists, invokes sorted, and asserts that the returned list is monotonically increasing.The generator can be separate from the parametrized test, with @given connecting them.Source: §2.1 · p. 3
- Combining generation and test logic lets Hypothesis generate dependent arguments sequentially when a method has multiple interdependent inputs.The example also notes that a generator constrained to lists of minimum size one omits empty-list behavior, and that the assertions do not check whether input and output contain the same elements.Source: §2.1 · pp. 3–4
2.2 Large Language Models
- Pre-trained LLMs predict the next token and can perform tasks from examples or textual instructions supplied in a prompt.The paper uses pre-trained language models, adapting them to the task through prompt engineering alone.Source: §2.2 · p. 4
- LLMs trained extensively on code, as well as general-purpose LLMs, have been applied to software engineering tasks through prompt engineering.The listed tasks include program synthesis, repair, code explanation, and test generation.Source: §2.2 · p. 4
3 THE PROPTEST-AI APPROACH
Proptest-AI prompts LLMs with API documentation to synthesize Hypothesis property-based tests, then evaluates the tests for validity, soundness, and property coverage.
3.1 Prompt Design
- Two-stage prompting first extracts up to five API properties, then generates an individual Hypothesis test function for each.Single-stage prompting instead asks for a generation strategy, properties to test, and one complete test.Source: §3.1 · p. 4
3.2 Evaluation Methodology
- The evaluation methodology assesses whether tests are valid, sound, and cover documented properties.The paper motivates these metrics with examples of inaccurate tests and discusses mitigation strategies.Source: §3.2 · p. 4
3.2.1 Validity.
- A test is valid only if all invocations avoid runtime errors other than property-assertion failures.For example, a timedelta generator can produce days with magnitude above 1,000,000, triggering OverflowError.Source: §3.2.1 · p. 5, Figure 5 · p. 5
3.2.2 Soundness.
- Soundness requires zero assertion errors across test invocations; the approach treats frequent assertion failures as evidence of an unsound property.The paper notes that interpreting an assertion failure as more likely an unsound property than an API bug is a weak assumption.Source: §3.2.2 · p. 5
3.2.3 Property Coverage.
- Property coverage measures whether sound tests kill mutants designed to violate documented properties.A property mutant preserves the API method signature, runs the original method, and mutates its output; a property is covered if a corresponding mutant is killed.Source: §3.2.3 · p. 6
4 EVALUATION
Across 40 Python API methods, two-stage GPT-4 achieved the strongest end-to-end property coverage. The evaluation also found that the execution-based soundness metric aligned closely with human labels.
4.1 Experimental Setup
- The study evaluated three models across 40 deterministic API methods from 10 Python libraries using single- and two-stage prompting.The models were GPT-4, Claude-3-Opus, and Gemini-1.5-Pro; each approach was sampled five times.Source: §4.1 · p. 6
4.2 RQ1: Validity and Soundness
- 2.4 samples on average yielded a valid, sound GPT-4 test with two-stage prompting, which outperformed single-stage prompting on validity and soundness across models.GPT-4 achieved the highest validity and soundness for both prompting approaches.Source: §4.2 · p. 7
4.3 RQ2: Soundness Metric Alignment
- The execution-based soundness metric achieved 100% precision and 97.14% recall against human labels.Its single false negative came from an unsound assertion that was not triggered by an edge-case input during 1,000 invocations.Source: §4.3 · p. 8
4.4 RQ3: Property Coverage
- Valid, sound samples killed 40–80% of property mutants, with higher coverage in native Python libraries and stronger assertions needed for networkx.The paper attributes networkx's difficulty to the complexity of graph properties.Source: §4.4 · pp. 8–9, Figure 11 · p. 9
- 20.5% of documented properties were covered by valid, sound PBTs from two-stage GPT-4 across 40 API methods.The evaluation included 200 properties in total.Source: Table 5 · p. 9, §4.4 · p. 9
5 THREATS TO VALIDITY
The evaluation uses repeated sampling and execution, but its validity claims have construct, internal, and external boundaries. The authors flag possible soundness misclassification, equivalent mutants, and limited evidence about generalization.
5.1 Construct Validity
- Five samples per LLM and 1,000 test executions mitigate nondeterminism, with 1,000 executions following Hypothesis's standard.Validity and soundness measurements depend on executing tests that include random-input generation.Source: §5.1 · p. 9
5.2 Internal Validity
- Assertion failures may reflect actual program bugs rather than unsound properties, so manual labeling provides a stronger soundness judgment.Output-level property mutations mitigate source-level equivalent mutants, but some mutated outputs may still be equivalent.Source: §5.2 · p. 9
5.3 External Validity
- The study covers Python and established libraries whose documentation and source may be in model training data, so generalization to other languages, libraries, and new APIs is uncertain.The authors also cannot confirm whether existing PBTs for selected methods appeared in model training data, although they found none in the selected repositories.Source: §5.2 · pp. 9–10, §5.3 · p. 10
6 RELATED WORK
Related work addresses automated unit-test and oracle generation, fuzzing, and retrieval-augmented code generation. The paper distinguishes its focus on synthesizing property-based tests whose assertions must be sound and cover documented properties.
Related work
- Prior LLM testing work generated unit tests, while TiCoder uses proposed tests to concretize natural-language specifications for function implementations.TestPilot automatically refines prompts after test errors, using documentation, signatures, or error information.Source: §6 · p. 10
- Regression assertions capture possibly buggy behavior, while mutation-based assertion selection addresses completeness but leaves soundness unresolved.Randoop generates regression assertions; μTest, EvoSuite, and Pynguin use mutation testing to retain assertions that kill mutants.Source: §6 · p. 10
- Natural-language oracle extraction targets exceptions, metamorphic relations, or temporal properties, but imprecise documentation can yield unsound assertions.These tools can detect implementation bugs unlike regression oracles, and traditional NLP poses fewer validity concerns than hallucination-prone LLMs.Source: §6 · p. 10
- Deep-learning oracle generators avoid some validity problems through token prediction or assertion grammars, while soundness and strength remain concerns.ATLAS predicts oracle token sequences; TOGA has a model select from a defined assertion grammar.Source: §6 · p. 10
- PBTs test properties over generator-produced inputs, while effective input-space search is orthogonal; retrieval approaches may supply additional knowledge for synthesis.Coverage guidance, validity-biased guidance, reinforcement-learning guidance, and behavioral-diversity guidance are possible pairings; DocPrompting [51] and ARKS [52] retrieve knowledge for code generation.Source: §6 · p. 10
- Fuzz-driver work is related, but crash-focused fuzzing does not address property soundness or coverage in the same way as PBT.UTopia notes that assertions such as null-pointer checks may need preservation for property validity; LLM fuzz-driver generation includes [20] and OSS-Fuzz.Source: §6 · p. 10
7 DATA AVAILABILITY
Evaluation materials and supporting artifacts are available in an anonymized repository. The repository also includes the API documentation and prompt templates.
7 DATA AVAILABILITY
- The anonymized repository contains evaluation data for Proptest-AI, including synthesized tests, property mutants, and measurements.The measurements cover validity, soundness, and property coverage.Source: §7 · pp. 10–11
- API method documentation and prompt templates are also included in the repository.Source: §7 · p. 11
8 CONCLUSION
The paper characterizes validity, soundness, and documented-property coverage as qualities of good PBTs and evaluates LLM synthesis. In 40 Python API methods, two-stage prompting with GPT-4 produced valid and sound tests in 2.4 samples on average and covered 21% of documented properties.
8 CONCLUSION
- 21% of documented properties were covered by PBTs synthesized with two-stage prompting and GPT-4 across 40 Python API methods.The evaluation methodology assesses validity, soundness, and coverage of properties documented for the API methods.Source: §8 · p. 11
- 2.4 samples on average produced valid and sound PBTs with two-stage prompting and GPT-4 across 40 Python API methods.Source: §8 · p. 11