Utilizza il Testing Basato su Proprietà per Colmare la Generazione e la Validazione del Codice con LLM

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

June 23, 2025

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

cs.AI

Abstract

I Large Language Model (LLM) eccellono nella generazione di codice, ma garantire che i loro output siano funzionalmente corretti, specialmente in compiti di programmazione complessi, rimane una sfida persistente. Sebbene lo sviluppo guidato dai test (Test-Driven Development, TDD) tradizionale offra un percorso per il perfezionamento del codice, la sua efficacia con gli LLM è spesso compromessa dalla scarsità di casi di test di alta qualità o dalle insidie della generazione automatica di test, inclusi test distorti o previsioni di output inaccurati che possono deviare il processo di correzione. Questo articolo introduce Property-Generated Solver, un nuovo framework che sfrutta il testing basato su proprietà (Property-Based Testing, PBT) per validare proprietà o invarianti di alto livello del programma, invece di affidarsi a specifici esempi di input-output. Queste proprietà sono spesso più semplici da definire e verificare rispetto alla previsione diretta di oracoli di test esaustivi, rompendo il "ciclo di autoinganno" in cui i test potrebbero condividere difetti con il codice che dovrebbero validare. Property-Generated Solver impiega due agenti basati su LLM che collaborano: un Generatore dedicato alla generazione di codice e al perfezionamento iterativo, e un Tester che gestisce il ciclo di vita del PBT e formula feedback semanticamente ricchi dalle violazioni delle proprietà. Il feedback completo e azionabile risultante guida quindi il Generatore nei suoi sforzi di perfezionamento. Stabilendo il PBT come motore di validazione centrale all'interno di questo paradigma iterativo a ciclo chiuso, Property-Generated Solver fornisce un meccanismo robusto per indirizzare gli LLM verso codice più corretto e generalizzabile. I risultati sperimentali estesi su molteplici benchmark di generazione di codice dimostrano che Property-Generated Solver raggiunge miglioramenti sostanziali in termini di pass@1, con guadagni relativi che vanno dal 23,1% al 37,3% rispetto ai metodi TDD consolidati.

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.