Rédiger un PREreview

Large language models are increasingly used not only to generate code, but also to generate tests and other evidence intended to verify that code. This creates a methodological problem: a verifier may appear stronger when it explores behaviors beyond the public examples, while some of that apparent coverage may consist of requirements the verifier has invented rather than requirements supported by the specification. We study this problem in a controlled pilot in which an LLM generates executable verification challenges from a software requirement and public interface without observing the candidate implementation. We vary the generator's access to, and dependence on, public examples and separately measure challenge validity and semantic coverage. Challenges are labeled before condition identities are revealed, and validity is evaluated against a known-good implementation under a frozen requirement contract. Across two semantically distinct software bug families, we observe the same broad pattern: conditions that encourage greater exploration produce broader semantic coverage but lower challenge-level validity. In one replication case, the baseline condition achieved 75% validity and covered two useful semantic signatures, while the strongest exploration condition achieved 30% validity but covered nine useful signatures, including five not observed under the other conditions. Conversely, a structured condition achieved 100% validity while collapsing to a single semantic signature. A secondary validity-label audit on a frozen sample achieved 81.25% agreement (Cohen's kappa = 0.684) under evidence parity; annotator independence could not be verified retrospectively. These results are preliminary and do not establish a universal property of LLM verification. They instead identify a measurable evaluation problem: semantic novelty alone can overstate verification quality when the generated checks are not grounded in the requirement they are intended to verify.