pith. sign in

arxiv: 2605.22368 · v1 · pith:EBDAISMPnew · submitted 2026-05-21 · 💻 cs.LG · cs.AI· cs.SE

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
show 2 more authors
Jingwei Liang Tao Luo
This is my paper

Pith reviewed 2026-05-22 08:13 UTC · model grok-4.3

classification 💻 cs.LG cs.AIcs.SE
keywords verifiable code generationadversarial testingtest suite scalingLLM evaluationbenchmark constructionspecification generationcode generation
0
0 comments X

The pith

Adversarially expanded test suites reveal that LLMs are weaker at verifiable code generation than standard benchmarks suggest.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper presents VeriScale, a framework that scales up test suites for evaluating LLMs on generating code with formal specifications. It does this by first expanding the suites using adversarial implementations to create more challenging cases, then reducing them to keep only the most useful ones. Applying it to the Verina benchmark produces a much larger VerinaPlus that causes big drops in model performance scores, showing overestimation in prior tests. A smaller VerinaLite version keeps the same power to tell good models from bad ones but at lower cost. Readers should care because reliable benchmarks are needed to track real progress in AI-assisted software engineering.

Core claim

VeriScale consists of two stages: test-suite expansion to construct diverse and challenging test cases driven by adversarial implementations, and test-suite reduction to distill them into compact yet discriminative suites. Instantiated on Verina, it creates VerinaPlus expanding by over 83 times and VerinaLite as a 14 times variant. Experiments on eight state-of-the-art LLMs show VerinaPlus exposes substantial model weaknesses with sharp score drops on SpecGen and CodeGen tasks, while VerinaLite maintains the discriminative power at a fraction of the evaluation cost.

What carries the argument

The VeriScale framework driven by adversarial implementations for test-suite expansion followed by reduction to create compact discriminative suites.

If this is right

  • Standard benchmarks overestimate LLM capabilities for generating verifiable code.
  • Expanded test suites provide a more accurate measure of model performance on SpecGen and CodeGen tasks.
  • Reduced test suites achieve similar evaluation quality with lower computational cost.
  • Public release of the enhanced benchmarks supports further research on improving LLMs for software engineering.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar adversarial scaling could improve evaluation quality in other code-related benchmarks.
  • LLM training may benefit from incorporating adversarial test cases to build more robust models.
  • Combining this approach with formal verification tools could provide deeper insights into code correctness.

Load-bearing premise

The adversarial implementations used for test-suite expansion generate valid, diverse, and genuinely more challenging test cases that do not introduce artifacts or bias the evaluation.

What would settle it

If evaluations on VerinaPlus do not show sharp score drops for the LLMs or if the new test cases are determined to be invalid or biased.

Figures

Figures reproduced from arXiv: 2605.22368 by Guihong Wang, Jian Yu, Jingwei Liang, Shuhan Xie, Tao Luo, Xiaoyang Liu, Yangyu Zhang, Yantao Li, Yifan Bai, Zihao Mou.

Figure 1
Figure 1. Figure 1: Overview of the VeriScale framework for adversarial test-suite scaling. Driven by the adversarial implementations, the framework scales verifiable code generation benchmarks through two core stages: test-suite expansion to ensure rigorous boundary coverage, and test-suite reduction to optimize evaluation efficiency without sacrificing discriminative power. capturing the program intent, allowing incorrect i… view at source ↗
Figure 2
Figure 2. Figure 2: illustrates this bidirectional pipeline in practice. For the isolated expected inputs, we execute the reference implementation to compute their corresponding outputs. This completes the expected input-output pairs, establishing a ground truth for evaluating functional correctness. EXAMPLE OF CANDIDATE INPUT CLASSIFICATION Problem Description: (VERINA #advanced_7) This task requires writing a Lean 4 functio… view at source ↗
Figure 3
Figure 3. Figure 3: Case study of a flawed specification on VERINA #advanced_3. The generated postcondition success￾fully rejects unexpected outputs from the original dataset, but erroneously accepts our adversarially synthesized unexpected outputs. often rely on LLMs to directly hallucinate incor￾rect outputs or employ naive random sampling to deviate from the ground truth. However, these triv￾ially incorrect outputs are usu… view at source ↗
Figure 4
Figure 4. Figure 4: An example of adversary-killing reduction. Given an expected input, an adversarial implementation is considered "killed" if its output differs from the ex￾pected output. The illustrated case kills six out of seven adversarial implementations, making it a high-quality case. For simplicity, we ignore any preconditions in these adversarial implementations. 6 [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Performance comparison of eight models on VERINA, VERINAPLUS, and VERINALITE. The top panel shows the Code Score, while the bottom panel displays the Spec Sound&Complete Score. For the specification evaluation, we include error bars indicating the lower bound (treating unknown cases as not holding) and upper bound (treating unknown cases as holding). All experiments are implemented using Lean v4.24.0. The … view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper proposes VeriScale, a two-stage framework using adversarial implementations to expand test suites for verifiable code generation benchmarks and then reduce them. Instantiated on the Verina benchmark, it produces VerinaPlus (83× expansion) and VerinaLite (14× variant). Experiments across eight LLMs report sharp performance drops on SpecGen and CodeGen tasks with VerinaPlus, indicating that prior benchmarks overestimate model capabilities, while VerinaLite preserves discriminative power at lower cost. Enhanced benchmarks and code are publicly released.

Significance. If the adversarial test cases prove valid, diverse, and unbiased, the work would meaningfully advance evaluation practices for LLMs in code generation and formal specification by exposing limitations hidden in existing benchmarks. The public artifact release supports reproducibility and community follow-up.

major comments (2)
  1. The description of the test-suite expansion stage (abstract and §3) provides no details on how adversarial implementations are generated, what checks ensure new tests are spec-consistent (i.e., pass for correct code and fail only for incorrect code per the original specification), or any diversity/validity metrics. This is load-bearing for the central claim that observed score drops on SpecGen and CodeGen reflect genuine model weaknesses rather than test artifacts or biases.
  2. Experimental results section: the reported sharp score drops across eight LLMs lack any mention of statistical tests, confidence intervals, or controls for confounds such as unintended correlations between adversarial tests and model training data. Without these, the evidence that VerinaPlus exposes hidden weaknesses remains weakly supported.
minor comments (1)
  1. The abstract refers to 'SpecGen and CodeGen tasks' without a brief definition or pointer to the Verina benchmark paper; adding one sentence would improve accessibility.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive feedback, which helps strengthen the presentation and evidence in our work on VeriScale. We address each major comment below and commit to revisions that enhance clarity without altering the core contributions.

read point-by-point responses

  1. Referee: The description of the test-suite expansion stage (abstract and §3) provides no details on how adversarial implementations are generated, what checks ensure new tests are spec-consistent (i.e., pass for correct code and fail only for incorrect code per the original specification), or any diversity/validity metrics. This is load-bearing for the central claim that observed score drops on SpecGen and CodeGen reflect genuine model weaknesses rather than test artifacts or biases.

    Authors: We agree that additional detail is required to substantiate the validity of the expanded test suites. In the revised manuscript, we will expand §3 with a new subsection describing the adversarial implementation generation process (including the two-stage framework mechanics), explicit spec-consistency verification procedures (e.g., ensuring reference implementations pass all tests while known buggy variants fail), and quantitative metrics for diversity (such as branch coverage and edge-case distribution) and validity (such as agreement rates with the original specification). These additions will directly support that performance drops reflect model limitations rather than artifacts. revision: yes

  2. Referee: Experimental results section: the reported sharp score drops across eight LLMs lack any mention of statistical tests, confidence intervals, or controls for confounds such as unintended correlations between adversarial tests and model training data. Without these, the evidence that VerinaPlus exposes hidden weaknesses remains weakly supported.

    Authors: We acknowledge this limitation in the current experimental reporting. The revised version will incorporate statistical significance testing (e.g., paired Wilcoxon signed-rank tests across models), 95% confidence intervals on all reported scores, and an analysis of potential confounds including checks for overlap with common pre-training corpora where feasible. We will also add a limitations paragraph noting any remaining constraints on full confound control. These changes will provide stronger empirical grounding for the observed weaknesses. revision: yes

Circularity Check

0 steps flagged

No significant circularity in framework or empirical results

full rationale

The paper introduces an empirical two-stage framework (adversarial test-suite expansion followed by reduction) and reports direct experimental outcomes on eight LLMs, including observed score drops on SpecGen and CodeGen tasks for VerinaPlus versus the original benchmark. No mathematical derivation chain, equations, fitted parameters, or predictions are present that could reduce to the inputs by construction. The central claims rest on observable performance differences using independent models and publicly released artifacts rather than self-definitional loops, load-bearing self-citations, or renamed known results. This is a standard non-circular empirical contribution in benchmark construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The framework rests on the domain assumption that adversarial implementations produce useful test cases; no free parameters or invented entities are mentioned in the abstract.

axioms (1)
  • domain assumption Adversarial implementations can be used to construct diverse and challenging test cases that reveal model weaknesses in specification and code generation.
    This premise underpins the test-suite expansion stage described in the abstract.

pith-pipeline@v0.9.0 · 5781 in / 1166 out tokens · 47009 ms · 2026-05-22T08:13:28.547369+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

28 extracted references · 28 canonical work pages · 1 internal anchor

  1. [1]

    Evaluating Large Language Models Trained on Code

    Evaluating large language models trained on code.Preprint, arXiv:2107.03374. Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient smt solver. InTools and Algorithms for the Construction and Analysis of Systems, pages 337– 340, Berlin, Heidelberg. Springer Berlin Heidelberg. Quinn Dougherty and Ronak Mehta. 2025. Proving the coding interview: A be...

    work page internal anchor Pith review Pith/arXiv arXiv 2008

  2. [2]

    InThe Thirty-ninth An- nual Conference on Neural Information Processing Systems Datasets and Benchmarks Track

    CLEVER: A curated benchmark for formally verified code generation. InThe Thirty-ninth An- nual Conference on Neural Information Processing Systems Datasets and Benchmarks Track. Ruijie Xu, Zengzhi Wang, Run-Ze Fan, and Pengfei Liu

    work page

  3. [3]

    input": {

    Benchmarking benchmark leakage in large language models.Preprint, arXiv:2404.18824. Kaichun Yao, Hao Wang, Chuan Qin, Hengshu Zhu, Yanjun Wu, and Libo Zhang. 2024. Carl: Unsu- pervised code-based adversarial attacks for program- ming language models via reinforcement learning. ACM Trans. Softw. Eng. Methodol., 34(1). He Ye, Aidan Z.H. Yang, Chang Hu, Yanl...

    work page arXiv 2024

  4. [4]

    Do not output markdown, prose, comments, or code fences

    work page

  5. [5]

    Keys in each`input`object must exactly match the function parameter names: no missing keys, no extra keys

    work page

  6. [6]

    Values must be JSON−serializable and type−compatible with the declared Lean parameter types

    work page

  7. [7]

    Treat the ground−truth precondition as the valid−input boundary: generate both valid and invalid inputs, especially boundary cases

    work page

  8. [8]

    Treat likely−invalid as semantically violating the precondition, not malformed JSON

    Include both likely−valid and likely−invalid inputs. Treat likely−invalid as semantically violating the precondition, not malformed JSON

    work page

  9. [9]

    likely−invalid

    Generate diverse and challenging edge−case candidates. Return exactly the number of candidates requested by the user. Generate candidate inputs for this Lean4 programming verification task. Task description: {description} Ground−truth precondition: {precond} Use of precondition: − It defines the semantic boundary of valid inputs. − Generate both inputs th...

    work page

  10. [10]

    contents (decleration of the input variables) b

    Identify the Input information: a. contents (decleration of the input variables) b. constraints of the input − type/data structure of the input variables − properties of the input variables must satisfy, mark each property with one of the following two keywords (E: Explicit, properties that are stated explicitly in the problem descripition) (H: Hypothesis...

    work page

  11. [11]

    contents (decleration of the output variables, you can declare them as`res1, res2, ...`) b

    Identify the Output information: a. contents (decleration of the output variables, you can declare them as`res1, res2, ...`) b. constraints of the output − type/data structure of the output variables − properties of the output variables must satisfy, the relationship between the input and the output (eg. elements/ ordering preserving, elements inclusion, etc.)

    work page

  12. [12]

    − Consider the type of the variables, for example, real numbers, integers, string and etc

    A detailed description of the type of input and output: − Figure out the data struture, consider list/tuples and etc. − Consider the type of the variables, for example, real numbers, integers, string and etc

    work page

  13. [13]

    A detailed description of the relationship between the input and the output. You may think through: − Does every element of the output originate from the input? − Does the output preserve any ordering from the input? − Does the output contain all elements from the input that meet some conditions?

    work page

  14. [14]

    Unless explicitly stated, do NOT mark non−empty, integer−only, positivity, uniqueness, sortedness and etc. with`E`

    work page

  15. [15]

    ### Output Format You MUST structure your response strictly as follows: Input: a

    Do not add any explanations of the constraints. ### Output Format You MUST structure your response strictly as follows: Input: a. {contents} b. {constraints} − {constraints1} − {constraints2} − ... Output: a. {contents} b. {constraints} − {constraints1} − {constraints2} − ... ### Now perform the following task: − **Problem Description**: {problem_descript...

    work page

  16. [16]

    Both the Input and Output have two parts: contents and constraints

    Generate the Lean4 code for the precondition and postcondition according to the Input and Output information. Both the Input and Output have two parts: contents and constraints. Note that you should include all the information provided for you

    work page

  17. [17]

    You should carefully analyze the problem description to help you identify gaps and omissions, thereby capturing any missing details within the Input and Output

    work page

  18. [18]

    Define the Lean4 precondition and postcondition by using the provided function signature

    work page

  19. [19]

    Neglect the constraints marked with 'H'

    Only translate the constraints of the precondition marked with 'E'. Neglect the constraints marked with 'H'

    work page

  20. [20]

    lazy" code hacker. Your objective is to perform

    If auxiliary functions are needed, put them directly before the precondition and postcondition. ### Output Format You MUST structure your response strictly as follows: ```lean −− Precondition Implementation {precondition auxiliary functions, if any. precondition implementation} −− Postcondition Implementation {postcondition auxiliary functions, if any. po...

    work page

  21. [21]

    You MUST NOT write a genuine algorithmic solution to the`Problem Description`. **If your code actually solves the true problem perfectly, you have FAILED your mission.** Your code MUST produce fundamentally WRONG outputs according to the natural language problem, BUT these wrong outputs must magically trick the`post−condition` into evaluating to`True`(or ...

    work page

  22. [22]

    Carefully analyze the`post−condition`. What crucial constraints from the`Problem Description`did it forget to check? You may consider − Did it check`List.length`but forget to check elements? − Did it check`List.Sorted`but forget to ensure elements belong to the original list? − Did it use`∃`without bounding the witness? − Did it use`∀x∈xs`but forget the e...

    work page

  23. [23]

    no duplicates

    Here are some adversarial strategies you may consider: − *Constant Return*: Return meaningless constants (`0`,`#[]`,`[]`,`""`,`#[0, 0]`,`false`,`none`) if the post− condition fails to bind the output to the input. − *Input Echoing*: Return the input parameters directly unmodified (e.g.,`fun xs => xs`). − *Trivial Synthesis*: Return`List.replicate n 0`,`Li...

    work page

  24. [24]

    Your adversarial functions MUST be pure and total Lean4 functions. You MUST NOT: − declare new`axiom`s, use`sorry`, or introduce`opaque`definitions to bypass verification − use`unsafe`,`partial`, or non−terminating recursion to avoid producing a real value − use`@[implemented_by ...]`,`@[extern ...]`, or any attribute that replaces the compiled behavior o...

    work page

  25. [25]

    You MUST NOT use type−level / typeclass / coercion tricks to fake post−condition satisfaction. In particular, DO NOT: − define custom`structure`s /`inductive`types as outputs purely so that a custom`DecidableEq`,`LE`,`LT`, or` BEq`instance makes the post−condition trivially true − override or re−declare instances such as`BEq`,`DecidableEq`,`LE`,`LT`,`Ord`...

    work page

  26. [26]

    Try to use a *different* adversarial strategy from the list above for each one to probe different potential loopholes

    You must generate exactly**5** different adversarial implementations. Try to use a *different* adversarial strategy from the list above for each one to probe different potential loopholes

    work page

  27. [27]

    Distinguish each adversarial function by appending the suffix`i`to its name, where i denotes the index of the i−th adversarial implementation

    The function signatures of your adversarial implementations MUST match the implementation signature provided. Distinguish each adversarial function by appending the suffix`i`to its name, where i denotes the index of the i−th adversarial implementation

    work page

  28. [28]

    ### Output Format You MUST structure your response strictly as follows

    DO NOT add any explanations. ### Output Format You MUST structure your response strictly as follows. Do not include any explanations, and you must provide**5** adversarial implementations. ```lean −− Adversarial Implementation 1 {adversatial function 1} 18 −− Adversarial Implementation 2 {adversatial function 2} −− Adversarial Implementation 3 {adversatia...

    work page