Pith. sign in

REVIEW 7 cited by

Can Large Language Models Write Good Property-Based Tests?

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2307.04346 v2 pith:WQSUBE3M submitted 2023-07-10 cs.SE

classification cs.SE
keywords propertypbtsdocumentationfindlanguagellmsmodelsproperties
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

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.

Discussion (0). Sign in to comment.

Forward citations

Cited by 7 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. ELFuzz: Efficient Input Generation via LLM-driven Synthesis Over Fuzzer Space

    cs.CR 2025-06 conditional novelty 7.0 of 10

    ELFuzz automatically evolves LLM-written input generators for large programs, outperforming grammar-based fuzzers in coverage and bug finding on seven benchmarks.

  2. Teaching Code LLMs to Reason with Intermediate Formal Specifications

    cs.SE 2026-07 conditional novelty 6.0 of 10

    Verification-guided fine-tuning with mutants and refinement traces teaches CodeLLMs to emit intermediate executable assertions that improve checking and repair on HumanExec.

  3. PBFuzz: Agentic Directed Fuzzing for PoV Generation

    cs.CR 2025-12 conditional novelty 6.0 of 10

    An agentic fuzzing system lets LLM agents infer vulnerability constraints, encode them as parameter generators, and solve them with property-based testing; it triggered 57 Magma CVEs, 17 missed by other fuzzers.

  4. Hamster: A Large-Scale Study and Characterization of Developer-Written Tests

    cs.SE 2025-09 conditional novelty 6.0 of 10

    A large-scale study of 1.7M developer-written Java tests shows they commonly use fixtures, mocking, structured inputs, and multi-class scope, features largely missing from automated test generation tools.

  5. DisFaceRep: Representation Disentanglement for Co-occurring Facial Components in Weakly Supervised Face Parsing

    cs.CV 2025-08 unverdicted novelty 5.0 of 10

    DisFaceRep reports a weakly supervised face parsing framework that disentangles co-occurring facial components and outperforms existing weakly supervised segmentation methods on CelebAMask-HQ, LaPa, and Helen.

  6. LLM-based Property-based Test Generation for Guardrailing Cyber-Physical Systems

    cs.SE 2025-05 conditional novelty 5.0 of 10

    An LLM-based tool, ChekProp, extracts safety properties from CPS code and documentation and generates property-based tests that can serve as design-time checks and proposed runtime guardrails.

  7. Towards LLM-assisted High-Quality Property Generation for Solidity Smart Contracts

    cs.SE 2026-07 conditional novelty 4.0 of 10

    LLM-generated Solidity test properties catch most of the mutants that human-written properties catch on average, and match human quality on the LibBit contract.

Pith tools