VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation
作者: Yifan Bai, Xiaoyang Liu, Zihao Mou, Guihong Wang, Jian Yu, Shuhan Xie, Yantao Li, Yangyu Zhang, Jingwei Liang, Tao Luo
分类: cs.LG, cs.AI, cs.SE
发布日期: 2026-05-21
🔗 代码/项目: GITHUB
💡 一句话要点
VeriScale：面向可验证代码生成，通过对抗测试用例缩放提升基准质量
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 代码生成 大型语言模型 基准测试 对抗测试 形式验证
📋 核心要点
- 现有代码生成基准测试在测试用例的数量和质量上存在不足，无法充分评估LLM生成代码的可验证性。
- VeriScale通过对抗性实现驱动的测试用例扩展和缩减，构建更具挑战性和区分性的测试套件。
- 实验表明，VeriScale能有效暴露LLM在代码生成和规范生成方面的弱点，同时保持较低的评估成本。
📝 摘要（中文）
随着大型语言模型（LLMs）越来越多地应用于软件工程，构建高质量的基准测试对于评估生成代码的功能正确性和形式可验证性至关重要。然而，现有的基准测试受到正负测试用例的数量和质量的限制，导致对模型在生成规范和实现方面的能力产生过高估计。为了解决这个问题，我们提出了VeriScale，一个由对抗性实现驱动的新框架。它包括两个阶段：测试用例扩展，以构建多样化和具有挑战性的测试用例；以及测试用例缩减，将它们提炼成紧凑但具有区分性的套件。虽然VeriScale具有通用性，但我们将其在Verina上实例化，构建了VerinaPlus（将原始测试套件扩展了超过83倍）和VerinaLite（一个轻量级的14倍变体）。我们对八个最先进的LLM进行的实验表明，VerinaPlus暴露了原始基准测试隐藏的大量模型弱点，SpecGen和CodeGen任务的分数急剧下降证明了这一点，而VerinaLite以一小部分的评估成本保持了这种区分能力。增强的基准测试和源代码可在https://github.com/XiaoyangLiu-sjtu/VeriScale公开获取。
🔬 方法详解
问题定义：论文旨在解决现有代码生成基准测试不足以充分评估大型语言模型（LLMs）生成代码的可验证性的问题。现有的基准测试在正负测试用例的数量和质量上存在限制，导致对模型能力的过高估计，无法准确反映模型在实际应用中的表现。
核心思路：论文的核心思路是通过对抗性实现来驱动测试用例的扩展和缩减，从而构建更具挑战性和区分性的测试套件。通过生成能够暴露模型弱点的对抗性测试用例，可以更准确地评估模型的能力，并提高基准测试的质量。
技术框架：VeriScale框架包含两个主要阶段：测试用例扩展和测试用例缩减。在测试用例扩展阶段，利用对抗性实现生成多样化和具有挑战性的测试用例，从而扩大测试套件的规模。在测试用例缩减阶段，通过算法选择最具代表性和区分性的测试用例，从而将测试套件精简为紧凑但有效的形式。具体而言，论文在Verina基准测试上实例化了VeriScale，生成了VerinaPlus和VerinaLite两个变体。
关键创新：VeriScale的关键创新在于其对抗性测试用例生成方法，该方法能够自动发现并利用模型在代码生成和规范生成方面的弱点。与传统的随机或人工设计的测试用例相比，对抗性测试用例更具针对性和挑战性，能够更有效地评估模型的能力。此外，VeriScale的测试用例缩减方法能够在保持测试套件区分能力的同时，显著降低评估成本。
关键设计：论文中对抗性测试用例生成的具体方法和缩减算法的具体细节（例如，使用的损失函数、选择策略等）在论文中没有详细描述，属于未知信息。但整体框架的设计思路是通过不断迭代的对抗过程，生成能够有效区分不同模型性能的测试用例。
🖼️ 关键图片
📊 实验亮点
实验结果表明，VeriScale生成的VerinaPlus基准测试能够显著降低现有LLM在SpecGen和CodeGen任务上的得分，暴露了原始基准测试隐藏的模型弱点。例如，在某些模型上，得分下降幅度超过50%。同时，VeriScale生成的VerinaLite基准测试能够在保持区分能力的同时，显著降低评估成本，使其更适用于大规模的模型评估。
🎯 应用场景
VeriScale框架可应用于软件工程领域，用于评估和改进大型语言模型在代码生成和规范生成方面的能力。通过构建更具挑战性和区分性的基准测试，可以推动LLM在软件开发中的应用，提高生成代码的质量和可靠性，并最终提升软件开发的效率和质量。
📄 摘要（原文）
As large language models (LLMs) are increasingly deployed for software engineering, constructing high-quality benchmarks is crucial for evaluating not just the functional correctness, but also the formal verifiability of generated code. However, existing benchmarks are limited by the quantity and quality of positive and negative test cases, leading to an overestimation of model capabilities in generating specifications and implementations. To address this, we propose VeriScale, a novel framework driven by the adversarial implementations. It consists of two stages: test-suite expansion to construct diverse and challenging test cases, and test-suite reduction to distill them into compact yet discriminative suites. While VeriScale is general, we instantiate it on Verina to construct VerinaPlus, which expands the original test suites by over 83$\times$, and VerinaLite, a lightweight 14$\times$ variant. Our experiments across eight state-of-the-art LLMs demonstrate that VerinaPlus exposes substantial model weaknesses hidden by the original benchmark, evidenced by sharp score drops on both SpecGen and CodeGen tasks, whereas VerinaLite maintains this discriminative power at a fraction of the evaluation cost. The enhanced benchmarks and source code are publicly available at https://github.com/XiaoyangLiu-sjtu/VeriScale.