Verwenden Sie Property-Based Testing, um die Code-Generierung und Validierung von LLMs zu verbinden.

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

June 23, 2025

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

cs.AI

Zusammenfassung

Große Sprachmodelle (LLMs) zeichnen sich durch ihre Fähigkeit zur Code-Generierung aus, doch die Sicherstellung, dass ihre Ausgaben funktional korrekt sind, insbesondere bei komplexen Programmieraufgaben, bleibt eine anhaltende Herausforderung. Während traditionelle Testgetriebene Entwicklung (TDD) einen Weg zur Code-Verfeinerung bietet, wird ihre Wirksamkeit bei LLMs oft durch den Mangel an hochwertigen Testfällen oder die Fallstricke der automatisierten Testgenerierung untergraben, einschließlich verzerrter Tests oder ungenauer Ausgabevorhersagen, die den Korrekturprozess fehlleiten können. Dieses Papier stellt den Property-Generated Solver vor, ein neuartiges Framework, das Property-Based Testing (PBT) nutzt, um hochrangige Programmeigenschaften oder Invarianten zu validieren, anstatt sich auf spezifische Eingabe-Ausgabe-Beispiele zu verlassen. Diese Eigenschaften sind oft einfacher zu definieren und zu überprüfen als die direkte Vorhersage umfassender Testorakel, wodurch der „Zyklus der Selbsttäuschung“ durchbrochen wird, bei dem Tests möglicherweise die gleichen Fehler wie der Code aufweisen, den sie validieren sollen. Der Property-Generated Solver setzt zwei kollaborative, LLM-basierte Agenten ein: einen Generator, der sich der Code-Generierung und iterativen Verfeinerung widmet, und einen Tester, der den PBT-Lebenszyklus verwaltet und semantisch reichhaltiges Feedback aus Eigenschaftsverletzungen formuliert. Das daraus resultierende umfassende und handlungsorientierte Feedback leitet dann den Generator bei seinen Verfeinerungsbemühungen an. Indem PBT als zentrale Validierungsmaschine innerhalb dieses iterativen, geschlossenen Regelkreises etabliert wird, bietet der Property-Generated Solver einen robusten Mechanismus, um LLMs in Richtung korrekterer und generalisierbarer Codes zu steuern. Umfangreiche experimentelle Ergebnisse auf mehreren Code-Generierungs-Benchmarks zeigen, dass der Property-Generated Solver erhebliche Verbesserungen bei pass@1 erzielt, mit relativen Gewinnen zwischen 23,1 % und 37,3 % gegenüber etablierten TDD-Methoden.

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.