Use Testes Baseados em Propriedades para Conectar Geração e Validação de Código com LLMs

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

Resumo

Os Modelos de Linguagem de Grande Escala (LLMs) se destacam na geração de código, mas garantir que suas saídas sejam funcionalmente corretas, especialmente em tarefas de programação complexas, é um desafio persistente. Embora o Desenvolvimento Orientado a Testes (TDD) tradicional ofereça um caminho para o refinamento de código, sua eficácia com LLMs é frequentemente prejudicada pela escassez de casos de teste de alta qualidade ou pelas armadilhas da geração automatizada de testes, incluindo testes tendenciosos ou previsões de saída imprecisas que podem desviar o processo de correção. Este artigo apresenta o Property-Generated Solver, uma nova estrutura que aproveita o Teste Baseado em Propriedades (PBT) para validar propriedades ou invariantes de alto nível do programa, em vez de depender de exemplos específicos de entrada-saída. Essas propriedades são frequentemente mais simples de definir e verificar do que prever diretamente oráculos de teste exaustivos, rompendo o "ciclo de autoengano" onde os testes podem compartilhar falhas com o código que devem validar. O Property-Generated Solver emprega dois agentes colaborativos baseados em LLM: um Gerador dedicado à geração de código e refinamento iterativo, e um Testador que gerencia o ciclo de vida do PBT e formula feedback semanticamente rico a partir de violações de propriedades. O feedback abrangente e acionável resultante então orienta o Gerador em seus esforços de refinamento. Ao estabelecer o PBT como o mecanismo central de validação dentro desse paradigma iterativo e de ciclo fechado, o Property-Generated Solver fornece um mecanismo robusto para direcionar LLMs em direção a códigos mais corretos e generalizáveis. Resultados experimentais extensivos em vários benchmarks de geração de código demonstram que o Property-Generated Solver alcança melhorias substanciais no pass@1, com ganhos relativos variando de 23,1% a 37,3% em relação aos métodos TDD estabelecidos.

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.