Используйте тестирование на основе свойств для объединения генерации и проверки кода с помощью языковых моделей.

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

June 23, 2025

Авторы: Lehan He, Zeren Chen, Zhe Zhang, Jing Shao, Xiang Gao, Lu Sheng

cs.AI

Аннотация

Крупные языковые модели (LLM) превосходно справляются с генерацией кода, но обеспечение функциональной корректности их выводов, особенно в сложных задачах программирования, остается постоянной проблемой. Хотя традиционная разработка через тестирование (TDD) предлагает путь для улучшения кода, ее эффективность при работе с LLM часто снижается из-за недостатка высококачественных тестовых случаев или недостатков автоматической генерации тестов, включая предвзятые тесты или неточные прогнозы выходных данных, которые могут направить процесс исправления в неправильное русло. В данной статье представлен Property-Generated Solver — новый фреймворк, который использует тестирование на основе свойств (PBT) для проверки высокоуровневых свойств программы или инвариантов, вместо того чтобы полагаться на конкретные примеры входных и выходных данных. Эти свойства зачастую проще определить и проверить, чем напрямую предсказывать исчерпывающие тестовые оракулы, что позволяет разорвать "цикл самообмана", в котором тесты могут разделять недостатки с кодом, который они призваны проверять. Property-Generated Solver использует двух совместно работающих агентов на основе LLM: Генератор, отвечающий за генерацию кода и его итеративное улучшение, и Тестер, который управляет жизненным циклом PBT и формулирует семантически насыщенную обратную связь на основе нарушений свойств. Полученная всесторонняя и полезная обратная связь затем направляет Генератор в его усилиях по улучшению. Устанавливая PBT в качестве основного механизма проверки в рамках этой итеративной, замкнутой парадигмы, Property-Generated Solver предоставляет надежный механизм для направления LLM к более корректному и обобщаемому коду. Результаты обширных экспериментов на нескольких бенчмарках генерации кода демонстрируют, что Property-Generated Solver достигает значительных улучшений в показателе pass@1, с относительным приростом от 23,1% до 37,3% по сравнению с устоявшимися методами TDD.

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.