Utilice Pruebas Basadas en Propiedades para Conectar la Generación y Validación de Código con LLM

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

June 23, 2025

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

cs.AI

Resumen

Los Modelos de Lenguaje de Gran Escala (LLMs, por sus siglas en inglés) destacan en la generación de código, pero garantizar que sus resultados sean funcionalmente correctos, especialmente en tareas de programación complejas, sigue siendo un desafío persistente. Aunque el Desarrollo Guiado por Pruebas (TDD, por sus siglas en inglés) tradicional ofrece un camino para el refinamiento del código, su eficacia con los LLMs a menudo se ve socavada por la escasez de casos de prueba de alta calidad o los inconvenientes de la generación automatizada de pruebas, como pruebas sesgadas o predicciones de salida inexactas que pueden desviar el proceso de corrección. Este artículo presenta Property-Generated Solver, un marco novedoso que aprovecha las Pruebas Basadas en Propiedades (PBT, por sus siglas en inglés) para validar propiedades o invariantes de alto nivel del programa, en lugar de depender de ejemplos específicos de entrada-salida. Estas propiedades suelen ser más sencillas de definir y verificar que predecir directamente oráculos de prueba exhaustivos, rompiendo el "ciclo de autoengaño" en el que las pruebas podrían compartir defectos con el código que están destinadas a validar. Property-Generated Solver emplea dos agentes colaborativos basados en LLM: un Generador dedicado a la generación de código y refinamiento iterativo, y un Probador que gestiona el ciclo de vida de las PBT y formula retroalimentación semánticamente rica a partir de violaciones de propiedades. La retroalimentación integral y accionable resultante guía entonces al Generador en sus esfuerzos de refinamiento. Al establecer las PBT como el motor central de validación dentro de este paradigma iterativo y de bucle cerrado, Property-Generated Solver proporciona un mecanismo robusto para dirigir a los LLMs hacia un código más correcto y generalizable. Los resultados experimentales exhaustivos en múltiples benchmarks de generación de código demuestran que Property-Generated Solver logra mejoras sustanciales en pass@1, con ganancias relativas que oscilan entre el 23.1% y el 37.3% en comparación con los métodos TDD establecidos.

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.