Utilisez les tests basés sur les propriétés pour relier la génération de code par LLM et sa validation.

Use Property-Based Testing to Bridge LLM Code Generation and Validation

June 23, 2025

Auteurs: Lehan He, Zeren Chen, Zhe Zhang, Jing Shao, Xiang Gao, Lu Sheng

cs.AI

Résumé

Les modèles de langage de grande taille (LLMs) excellent dans la génération de code, mais garantir que leurs sorties soient fonctionnellement correctes, en particulier dans des tâches de programmation complexes, reste un défi persistant. Bien que le développement piloté par les tests (Test-Driven Development, TDD) traditionnel offre une voie pour l'affinement du code, son efficacité avec les LLMs est souvent compromise par la rareté de cas de test de haute qualité ou les pièges de la génération automatisée de tests, incluant des tests biaisés ou des prédictions de sortie inexactes qui peuvent détourner le processus de correction. Cet article présente Property-Generated Solver, un cadre novateur qui exploite les tests basés sur les propriétés (Property-Based Testing, PBT) pour valider des propriétés ou invariants de haut niveau des programmes, plutôt que de s'appuyer sur des exemples spécifiques d'entrées-sorties. Ces propriétés sont souvent plus simples à définir et à vérifier que de prédire directement des oracles de test exhaustifs, rompant ainsi le "cycle d'auto-tromperie" où les tests pourraient partager les mêmes défauts que le code qu'ils sont censés valider. Property-Generated Solver emploie deux agents collaboratifs basés sur des LLMs : un Générateur dédié à la génération de code et à son affinement itératif, et un Testeur qui gère le cycle de vie du PBT et formule des retours sémantiquement riches à partir des violations de propriétés. Les retours complets et exploitables qui en résultent guident ensuite le Générateur dans ses efforts d'affinement. En établissant le PBT comme moteur de validation central au sein de ce paradigme itératif en boucle fermée, Property-Generated Solver fournit un mécanisme robuste pour orienter les LLMs vers un code plus correct et généralisable. Les résultats expérimentaux approfondis sur plusieurs benchmarks de génération de code démontrent que Property-Generated Solver réalise des améliorations substantielles en pass@1, avec des gains relatifs allant de 23,1 % à 37,3 % par rapport aux méthodes TDD établies.

English

Large Language Models (LLMs) excel at code generation, but ensuring their outputs to be functionally correct, especially in complex programming tasks, is a persistent challenge. While traditional Test-Driven Development (TDD) offers a path for code refinement, its efficacy with LLMs is often undermined by the scarcity of high-quality test cases or the pitfalls of automated test generation, including biased tests or inaccurate output predictions that can misdirect the correction process. This paper introduces Property-Generated Solver, a novel framework that leverages Property-Based Testing (PBT) to validate high-level program properties or invariants, instead of relying on specific input-output examples. These properties are often simpler to define and verify than directly predicting exhaustive test oracles, breaking the "cycle of self-deception" where tests might share flaws with the code they are meant to validate. Property-Generated Solver employs two collaborative LLM-based agents: a Generator dedicated to code generation and iterative refinement, and a Tester that manages the PBT life-cycle and formulate semantically rich feedback from property violations. The resulting comprehensive and actionable feedback then guides the Generator in its refinement efforts. By establishing PBT as the core validation engine within this iterative, closed-loop paradigm, Property-Generated Solver provides a robust mechanism for steering LLMs towards more correct and generalizable code. Extensive experimental results on multiple code generation benchmarks demonstrate that Property-Generated Solver achieves substantial pass@1 improvements, ranging from 23.1% to 37.3% relative gains over established TDD methods.