VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation Yifan Bai1 * , Xiaoyang Liu1 * , Zihao Mou2 , Guihong Wang1 , Jian Yu3 , Shuhan Xie4 , Yantao Li5 , Yangyu Zhang6 , Jingwei Liang1,7† , Tao Luo1,7,8† 1 School of Mathematical Sciences, Shanghai Jiao Tong University 2 School of Science and Engineering, The Chinese University of Hong Kong, Shenzhen 3 School of Mathematics, Jilin University 4 School of Mathematical Sciences, Tongji University 5 Zhiyuan College, Shanghai Jiao Tong University 6 School of Future Technology, South China University of Technology 7 Institute of Natural Sciences, Shanghai Jiao Tong University 8 MOE-LSC, CMA-Shanghai, Shanghai Jiao Tong University address this reliability challenge, verifiable code Abstract
generation has emerged as a principled paradigm in which models are required to jointly synthesize formal specifications, code implementations, and machine-checkable proofs to establish their consistency (Sun et al., 2024; Ye et al., 2026). By integrating machine-checkable correctness guarantees into the generation process, this paradigm offers a promising path toward more trustworthy LLM-based software development. To rigorously evaluate this emerging paradigm, recent benchmarks such as C LEVER (Thakur et al., 2026) and V ERINA (Ye et al., 2026) have adopted Lean (Moura and Ullrich, 2021) as their core verification backend. Unlike verification frameworks such as Dafny (Leino, 2010) and Verus (Lattuada et al., 2023), which heavily leverage SMT solvers (de Moura and Bjørner, 2008) for automated theorem proving with less explicit proof steps, Lean operates as an interactive theorem prover (ITP). This distinction enables the construction of proofs with explicit intermediate steps, thereby facilitating the direct assessment of model capabilities in proof generation (ProofGen). For specification generation (SpecGen) and code generation (CodeGen), these benchmarks primarily rely on test cases as the empirical evaluation mechanism (Chen et al., 2021; Ye et al., 2026). However, this reliance on test-suite evaluation exposes a central limitation: the reliability of the assessment depends heavily on the quantity and quality of the underlying test cases. In current verifiable code generation benchmarks, each problem is typically accompanied by only a limited number of positive test cases, i.e., expected input-output pairs. More importantly, high-quality negative test cases are even more limited, including unexpected inputs and unexpected outputs that are essential for testing whether generated specifications correctly reject invalid behaviors. As a result, models may satisfy the sparse test cases without
arXiv:2605.22368v1 [cs.LG] 21 May 2026
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 V ERINA to construct V ERINA P LUS, which expands the original test suites by over 83×, and V ERINA L ITE, a lightweight 14× variant. Our experiments across eight state-of-the-art LLMs demonstrate that V ERINA P LUS exposes substantial model weaknesses hidden by the original benchmark, evidenced by sharp score drops on both SpecGen and CodeGen tasks, whereas V ERINA L ITE 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.
1
Introduction
The rapid advancement of large language models (LLMs) has reshaped software engineering, particularly in program synthesis and code generation (Chen et al., 2021; OpenAI et al., 2024). However, LLM-generated programs remain prone to subtle logical errors (Pearce et al., 2025), limiting their deployment in high-stakes settings. To * Equal contribution †
Corresponding author: [email protected], [email protected]
1
Test-Suite Expansion
Adversarial Synthesis
Seed
Type-aware
Problem
Generation
Mutation
Decomposition
GT Precondition
Classification
Reduced Reduced
Unexpected
Expected Input
Input
Reduced
Pass?
Unexpected
SpecGen
Test-Suite Reduction
Adversarial Implementation
Expected Output
Boundary-
Reduced
Preserving
Unexpected Output
Reduction
Expected Input
Input Expected Output
GT Impl
Adversary-Killing Reduction
Unexpected Output
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 implementations or unsound and incomplete specifications to achieve inflated pass rates and leading to an overestimate of model capabilities. To bridge this gap, we propose VeriScale, an adversarial framework that systematically scales test-suite evaluation for verifiable code generation. VeriScale first combines LLM-based seed generation with type-aware mutation to construct a large pool of candidate inputs. These inputs are then classified as either expected or unexpected according to the ground-truth preconditions. For the former, VeriScale executes the reference implementation to derive the corresponding outputs, thereby forming robust expected input-output pairs. The core innovation of VeriScale lies in constructing adversarial implementations to drive both the construction of unexpected outputs and the reduction of expected test cases. Instead of directly prompting LLMs to generate arbitrary unexpected outputs, VeriScale synthesizes adversarial implementations designed to exploit weaknesses in LLM-generated specifications, executing them on expected inputs. Outputs are retained only when they differ from the reference outputs while being falsely accepted by the generated postconditions, ensuring they are genuinely informative for exposing specification flaws. Finally, VeriScale repurposes these implementations in a reduction stage, distilling the expanded cases into compact yet discriminative test suites through boundary-preserving and adversary-killing reduction. To evaluate our approach, we apply VeriScale to
V ERINA, resulting in the V ERINA P LUS and V ERI NA L ITE benchmarks. The empirical results underscore the necessity of adversarial test scaling. Notably, GPT-5.5 experiences a severe performance degradation on V ERINA P LUS, plummeting from 68.78% to 44.44% on SpecGen and from 96.83% to 86.24% on CodeGen. This stark contrast highlights how the original benchmark significantly overestimates true model capabilities. Furthermore, model performance on V ERINA L ITE closely mirrors that on V ERINA P LUS, confirming that our reduction strategy successfully eliminates redundant test cases while preserving discriminative rigor. Our main contributions are as follows: 1. We propose VeriScale, a framework that leverages adversarial implementations to drive both the systematic expansion and the reduction of test suites for verifiable code generation. 2. We instantiate VeriScale on V ERINA to construct V ERINA P LUS, expanding the original test suites by over 83×, alongside V ERI NA L ITE , a lightweight 14× variant. 3. We show that V ERINA P LUS reveals substantial weaknesses overlooked by the original benchmark in both SpecGen and CodeGen, while V ERINA L ITE retains the discriminative power at a fraction of the evaluation cost.
2
Related Work
Benchmarks for Verifiable Code Generation. The evaluation of LLM-generated programs has evolved from functional correctness toward formal verifiability. Early benchmarks such as Hu2
manEval (Chen et al., 2021), MBPP (Austin et al., 2021), APPS (Hendrycks et al., 2021), and LiveCodeBench (Jain et al., 2025) primarily assess code generation through unit tests, but do not evaluate formal specifications or proofs. Recent verification-oriented benchmarks, including Dafny-Synthesis (Misu et al., 2024), Clover (Sun et al., 2024), DafnyBench (Loughridge et al., 2025), miniCodeProps (Lohn and Welleck, 2024), FVAPPS (Dougherty and Mehta, 2025), and V E RINA (Ye et al., 2026), incorporate formal reasoning tasks in languages such as Dafny and Lean. Among these benchmarks, V ERINA provides a comprehensive benchmark for verifiable code generation, supporting the evaluation of SpecGen, CodeGen, and ProofGen. VeriScale is complementary to these efforts: instead of introducing new tasks, it strengthens existing benchmarks by scaling expected input-output pairs, unexpected inputs, and high-quality unexpected outputs for more discriminative test-suite evaluation.
framework comprises two primary stages, test-suite expansion and test-suite reduction, both fundamentally driven by adversarial implementations. 3.1
Formally, each benchmark task is equipped with a problem description, a ground-truth precondition, a reference implementation, and existing base inputs. From these components, VeriScale constructs a comprehensive test suite encompassing three types of cases: expected input-output pairs, unexpected inputs, and unexpected outputs. Expected input-output pairs support both CodeGen and SpecGen evaluation by checking intended behaviors, while unexpected inputs and unexpected outputs test whether generated specifications reject invalid inputs and incorrect outputs, respectively. Seed Generation and Type-aware Mutation. Drawing inspiration from EvalPlus (Liu et al., 2023), VeriScale employs LLMs to synthesize a diverse set of initial seed inputs. To construct the generation prompt for each task, we aggregate the problem description, the ground-truth precondition, input parameter signatures (names and types), and any pre-existing expected and unexpected inputs. The LLM is then queried to output a specified volume of distinct candidate inputs, establishing a seed pool for the subsequent type-aware mutation phase. The detailed prompt is shown in Appendix C. To systematically expand the initial seed pool, VeriScale employs an iterative, type-aware mutation strategy (Park et al., 2021). To preserve taskspecific semantics during structural perturbation, we extract an ingredient pool from existing candidates, allowing target parameters to stochastically reuse these contextual values (Martinez and Monperrus, 2019). When reuse is not triggered, the framework falls back on type-specific heuristic perturbations. To construct complex edge cases, the mutation engine performs a sequence of modifications by randomly targeting a single parameter per step under a bounded generation budget. To mathematically capture how a specific value is perturbed during any given step, we formalize our type-aware mutation procedure as a five-tuple M = (T , D, O, p, q).
Scaling Test-Suite Evaluation. Test-suite quality is crucial for reliable code generation evaluation, as limited unit tests may allow incorrect programs to pass by missing corner cases. EvalPlus (Liu et al., 2023) is a representative effort that augments HumanEval (Chen et al., 2021) with large-scale test cases by combining seed generation and typeaware mutation. Mutation-based generation can mitigate benchmark leakage, since newly generated tests are less likely to have been memorized during training (Xu et al., 2024; Satvaty et al., 2026). Adversarial tests have also proven effective in exposing weaknesses in code generation and program repair systems (Yao et al., 2024; Ye et al., 2025). VeriScale is inspired by these methods but targets verifiable code generation, where evaluation requires richer signals than expected input-output pairs alone. In particular, SpecGen evaluation needs unexpected inputs and unexpected outputs to test whether generated specifications correctly reject invalid behaviors. Therefore, VeriScale extends test-suite scaling with precondition-guided classification and adversarial implementation synthesis, producing more informative negative cases to strictly evaluate the SpecGen task.
3
Test-Suite Expansion
Methodology
• T is the set of input types. • D maps each type τ ∈ T to its domain Dτ . • O maps each type τ ∈ T to a finite set of mutation schemas Oτ = {sτ,1 , . . . , sτ,kτ }. Each
In this section, we detail VeriScale, a framework designed to scale test-suite evaluation for verifiable code generation, as illustrated in Figure 1. The 3
schema sτ,i : Dτ × Θτ,i → Dτ is parameterized by a parameter space Θτ,i . • p maps each type τ ∈ T to a probability distribution pτ over Oτ , specifying how a mutation schema is selected. • q maps each pair (τ, i) to a probability distribution qτ,i over the parameter space Θτ,i , specifying how the parameters of schema sτ,i are sampled. In general, this distribution may depend on the input value x ∈ Dτ .
to timeouts or search exhaustion are permanently excluded from the final test suite. 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. E XAMPLE OF C ANDIDATE I NPUT C LASSIFICATION Problem Description: (V ERINA #advanced_7) This task requires writing a Lean 4 function that converts a binary number represented as a list of digits (0 or 1) into its corresponding decimal value. The list is ordered in big-endian format, meaning the most significant digit comes first. The function should interpret the list as a binary number and return its decimal representation as a natural number. Ground-Truth Precondition: def binaryToDecimal_precond (digits : List Nat) : Prop := digits.all (fun d => d = 0 ∨ d = 1)
Given an input value x ∈ Dτ , the mutator first samples a mutation schema I ∼ pτ , and then samples its parameters according to θ ∼ qτ,I (· | x). The mutated value is then defined as Mτ (x) = sτ,I (x; θ). Since each schema is type-preserving, for any x ∈ Dτ , i ∈ {1, . . . , kτ }, θ ∈ Θτ,i , we have sτ,i (x; θ) ∈ Dτ .
Candidate Input: [1, 2, 1] Syntax Filter: #check binaryToDecimal_precond ([1, 2, 1]) Ë Passed Stage 1: Bidirectional decide • #guard decide (binaryToDecimal_precond ([1, 2, 1])) → Failed (Expression did not evaluate to ‘true’) • #guard decide (¬ binaryToDecimal_precond ([1, 2, 1])) Ë Passed Stage 2: Bidirectional plausible
Therefore, the mutation procedure preserves the input type by construction: Mτ (x) ∈ Dτ . See Appendix A for more details of these schemas. Precondition-Guided Input Classification. To classify the candidate inputs, VeriScale operates in alignment with Verina (Ye et al., 2026), evaluating them against the ground-truth precondition using a two-stage verification pipeline. Prior to logical evaluation, we enforce a strict syntax filter. Each candidate is rendered as a Lean precondition application, denoted as <expr>, and validated via the #check <expr> command. Candidates failing this step due to missing arguments, type mismatches, or syntax errors are immediately discarded. In the first stage, we apply a bidirectional procedure, evaluating both #guard decide <expr> and #guard decide (¬ <expr>). An input is classified as expected if the positive expression evaluates to true (or the negation to false), and unexpected if the inverse holds. For these unresolved inputs, we construct an example, unfold the precondition, aggressively simplify the goal context via simp_all!, and execute plausible bidirectionally. Discovering a counterexample for the negated expression confirms the input as expected, whereas finding one for the positive expression marks it as unexpected. Candidates that still lack a definitive verdict due
• example: binaryToDecimal_precond ([1, 2, 1]) := by unfold binaryToDecimal_precond simp_all! plausible → Found a counter-example! • example: ¬ binaryToDecimal_precond ([1, 2, 1]) := by unfold binaryToDecimal_precond simp_all! Ë Passed Final Verdict: Unexpected Input.
Figure 2: A full trajectory of candidate input classification. The input [1,2,1] will be classified as unexpected because #guard descide fails at Stage 1. According to our judging process, this example does not proceed to Stage 2; it is shown here for illustration only.
Adversarial Synthesis of Unexpected Outputs. Beyond verifying basic functionality, evaluating the soundness and completeness of formal specifications requires high-quality unexpected outputs to serve as negative test cases. Existing approaches 4
Problem description: rotate a list of integers to the right by a specified number of positions. Specification generated by GPT-5.1:
l := [1, 2, 3, 4, 5] n := 7 Expected Input
[5,1,2,3,4] [3,4,5,1,2]
[4,5,1,2,3] Expected Output
Unexpected Output (
[] )
Unexpected Output (
)
Figure 3: Case study of a flawed specification on V ERINA #advanced_3. The generated postcondition successfully rejects unexpected outputs from the original dataset, but erroneously accepts our adversarially synthesized unexpected outputs.
often rely on LLMs to directly hallucinate incorrect outputs or employ naive random sampling to deviate from the ground truth. However, these trivially incorrect outputs are usually easily rejected by even highly flawed specifications, failing to provide meaningful diagnostic feedback for underspecification. As illustrated in Figure 3, a concrete case study demonstrates this limitation. To synthesize highly discriminative unexpected outputs, VeriScale introduces an adversarial execution paradigm. We first prompt language models to perform problem decomposition to reduce task complexity and clarify structural logic (Liu et al., 2026). Next, we leverage advanced models to generate high-quality formal specifications. Crucially, a more capable model acts as a red team (Perez et al., 2022), crafting adversarial implementations to exploit vulnerabilities within these specifications. As a fallback, if the model fails to generate an adversarial implementation, we systematically drop constraints from the ground-truth specification to expose an attack target, thereby facilitating the successful synthesis of an adversarial implementation. These adversarial implementations are subsequently executed on the expected inputs generated during the previous stage. If an adversarial implementation produces an output that diverges from the ground truth but is still successfully accepted by the generated postconditions, this mismatched value is formally retained. Because these unexpected outputs stem from systematic specification gaming rather than arbitrary hallucination, they closely mimic realistic logical errors, making them significantly more effective at exposing specification unsoundness and incompleteness. 3.2
tion and eliminate redundant expected input-output pairs through adversary-killing reduction. Unexpected outputs are implicitly filtered alongside their corresponding inputs. Boundary-Preserving Reduction. For unexpected inputs, we adopt a boundary-preserving reduction strategy rather than relying solely on random sampling or feature diversity. We extract lightweight structural signatures (e.g., empty containers, zero or negative values, mismatched lengths, and ordering patterns) to approximate failure modes. We then prioritize inputs that correspond to common boundary violations. For each task, we first retain representative examples from these critical boundary buckets, ensuring that frequent and semantically meaningful unexpected inputs are preserved. If the budget is not exhausted, we further fill the remaining slots with representative inputs from diverse structural buckets, and finally use a deterministic priority order as a fallback. This approach keeps the unexpected input set compact while maintaining coverage of typical precondition violations and edge-case behaviors. Adversary-Killing Reduction. We further use adversary-killing to reduce the set of expected input-output pairs. Specifically, we repurpose the adversarial implementations synthesized in the previous stage, treating each as a distinct mutant. We associate each expected pair with the set of adversarial implementations it can kill, formulating test reduction as a set-cover problem. We first select expected pairs that cover the largest number of previously unkilled mutants using a greedy procedure, ensuring that every implementation detectable by the expanded test suite remains covered by at least one retained pair. Then, under a fixed per-task budget, we add additional pairs that kill the highest number of implementations. This strategy avoids
Test-Suite Reduction
To reduce computational overhead, we filter unexpected inputs via boundary-preserving reduc5
Table 1: Comparison of test suite volumes. Data is formatted as Mean (Min–Max), accompanied by the relative growth multiplier compared to the baseline V ERINA. Dataset
Expected Input-Output
Unexpected Output
Unexpected Input
V ERINA V ERINA P LUS V ERINA L ITE
5.89 (2–13) 370.07 (5–705) (×62.83) 52.34 (5–61) (×8.89)
12.69 (2–34) 1114.01 (15–2973) (×87.79) 202.35 (15–467) (×15.95)
0.65 (0–7) 119.00 (0–684) (×183.08) 15.80 (0–50) (×24.31)
the coverage loss caused by purely diversity-based or random reduction, allowing the lightweight test suite to substantially reduce its size while preserving its ability to distinguish flawed specifications.
4
Experiments
4.1
The Augmented Benchmarks
E XAMPLE OF A DVERSARY-K ILLING R EDUCTION Problem Description: (V ERINA #advanced_16) Implement the insertion sort algorithm in Lean 4. The function takes a single list of integers as input and returns a new list that contains the same integers in ascending order. Candidate Expected Input: [0, -1, -2, -3, -4] Expected Output: [-4, -3, -2, -1, 0] Adversary-Killing Count
We instantiate VeriScale on the V ERINA dataset (Ye et al., 2026) to construct the augmented benchmarks V ERINA P LUS and V ERINA L ITE. During the expansion stage, we employ GPT-5.3-Codex for seed generation, problem decomposition, and adversarial implementation synthesis. To obtain highly diverse candidate specifications, we utilize an array of widely adopted prior models: ClaudeHaiku-4.5, Claude-Sonnet-4.5, GPT-5.1, GPT-4.1, Qwen3-Max, and DeepSeek-V3.2. Detailed hyperparameter configurations of the expansion and reduction stages are provided in Appendix B. In total, the API cost incurred during the benchmark expansion phase was $58.89. As demonstrated in Table 1, V ERINA P LUS significantly scales up the test volume by over 83× compared to the original baseline to ensure rigorous boundary coverage, whereas V ERINA L ITE optimizes computational overhead via the aforementioned reduction strategies to provide a lightweight 14× variant. Notably, the augmented benchmarks also consistently maintain 100% code coverage. 4.2
• def insertionSort (xs : List Int) : List Int := xs.reverse Output: [-4, -3, -2, -1, 0] → Same as expected • def insertionSort (xs : List Int) : List Int := match xs with | [] => [] | x :: _ => List.replicate xs.length x Output: [0, 0, 0, 0, 0] Ë Different • def insertionSort (xs : List Int) : List Int := List.replicate xs.length 0 Output: [0, 0, 0, 0, 0] Ë Different • def insertionSort (xs : List Int) : List Int := (List.range xs.length).map (fun n => Int.ofNat n) Output: [0, 1, 2, 3, 4] Ë Different • def insertionSort (xs : List Int) : List Int := [] Output: [] Ë Different • def insertionSort (xs : List Int) : List Int := xs Output: [0, -1, -2, -3, -4] Ë Different • def insertionSort (xs : List Int) : List Int := match xs with | [] => [] | x :: _ => [x]
Evaluation Setup
Output: [0] Ë Different
We evaluate eight state-of-the-art LLMs, including Claude-Sonnet-4.6, Claude-Opus-4.7, GPT-5.3Codex, GPT-5.5, Gemini-3.1-Flash-Lite-Preview, Gemini-3.1-Pro-Preview, Qwen3.6-Max-Preview, and DeepSeek-V4-Pro. These models are assessed across the V ERINA, V ERINA P LUS, and V ERI NA L ITE benchmarks, focusing on the SpecGen and CodeGen tasks. To ensure a rigorous assessment, we employ the official evaluation harness provided by V ERINA (Ye et al., 2026) to compute and report the pass@1 scores. However, we intentionally remove the original 2-shot setting to facilitate the evaluation of the entire dataset.
Adversary-Killing Count: 6 / 7.
Figure 4: An example of adversary-killing reduction. Given an expected input, an adversarial implementation is considered "killed" if its output differs from the expected 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
Claude-Sonnet-4.6 Gemini-3.1-Flash-Lite-Preview
Claude-Opus-4.7 Gemini-3.1-Pro-Preview
GPT-5.3-Codex Qwen3.6-Max-Preview
GPT-5.5 Deepseek-V4-Pro
Code Score 100
86.77 80
Verina VerinaPlus VerinaLite
89.42
86.24 88.36
79.37 82.01
75.13 77.78
73.02
96.83
91.01
79.37 81.48 67.72
63.49 65.08
56.61
60
60.32 61.38
64.02
49.74 50.79
56.61 58.20
40
20
0
Spec Sound&Complete Score 100
71.16
80
66.40
60.32 60
44.97
50.00
47.88
53.97
Verina VerinaPlus VerinaLite
69.05
68.78
60.32 47.09
50.00
44.44
47.88
44.71
42.33 31.75 33.07
40
48.41
Error bar 41.27
44.97
47.62 34.92
37.83
20
0
Figure 5: Performance comparison of eight models on V ERINA, V ERINA P LUS, and V ERINA L ITE. 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 evaluation was conducted on a server equipped with dual Intel Xeon Platinum 8380 CPUs, providing a total of 80 physical cores. 4.3
vulnerabilities, providing a much more rigorous evaluation of the SpecGen and CodeGen tasks. Furthermore, a closer examination of the SpecGen evaluation reveals a striking reduction in evaluation uncertainty, as evidenced by the significantly narrowed error bars on the augmented benchmarks. In the original V ERINA baseline, the scarcity of test cases frequently leads to indeterminate verification outcomes, resulting in wide margins between the upper and lower bounds. For example, Claude-Opus-4.7 exhibits a substantial gap of 13.23% (77.78% vs. 64.55%) on the baseline. However, under the rigorous scrutiny of V ERINA P LUS, this ambiguity is effectively resolved, drastically shrinking the gap for the same model to merely 4.76% (50.26% vs. 45.50%). This consistent compression of error margins across all evaluated models demonstrates that our adversarial scaling not only exposes model flaws, but also transforms a previously ambiguous evaluation into a highly definitive and statistically reliable assessment.
Evaluation Results
To systematically interpret our findings, we organize the evaluation results across three critical dimensions: the effectiveness of the augmented benchmarks in exposing hidden model vulnerabilities, the profound robustness gap between SpecGen and CodeGen, and the computational efficiency of our test-suite reduction strategy. Effectiveness of the Augmented Benchmarks. As illustrated in Figure 5, all models exhibit significant performance degradation across both SpecGen and CodeGen tasks on V ERINA P LUS and V ERINA L ITE compared to the V ERINA baseline. For instance, the top-performing model, GPT-5.5, achieves a code score of 96.83 and a specification soundness and completeness score of 68.78 on the baseline, which drop sharply to 86.24 and 44.44 on V ERINA P LUS, respectively. This consistent decline across all models demonstrates that the original benchmark overestimates model capabilities due to underspecified test cases. By addressing this critical limitation, our adversarial expansions successfully systematically expose previously hidden
Robustness Gap between SpecGen and CodeGen. While the augmented benchmarks universally depress scores, this degradation is far from uniform: the decline in CodeGen is drastically outpaced by a precipitous drop in SpecGen. Taking the top-performing GPT-5.5 as a representative example again, the model experiences a moderate 7
Table 2: Evaluation time on V ERINA, V ERINA P LUS, and V ERINA L ITE. We report wall-clock time in seconds, with the average row additionally highlighting the relative time multipliers compared to the V ERINA baseline. Model
SpecGen
CodeGen
V ERINA V ERINA P LUS V ERINA L ITE V ERINA V ERINA P LUS V ERINA L ITE
Claude-Sonnet-4.6 Claude-Opus-4.7 GPT-5.3-Codex GPT-5.5 Gemini-3.1-Flash-Lite-Preview Gemini-3.1-Pro-Preview Qwen3.6-Max-Preview DeepSeek-V4-Pro
996 1324 1018 1191 790 1214 962 757
1772 2758 1839 2100 1333 2081 1732 1261
1280 2102 1395 1669 1053 1645 1333 935
268 250 252 264 190 254 212 260
356 394 413 413 305 396 329 311
241 269 327 284 205 267 227 217
Average
1032
1860 (×1.80)
1427 (×1.38)
244
365 (×1.50)
255 (×1.05)
relative decline of roughly 10.59% in CodeGen when moving from the V ERINA baseline to V ERI NA P LUS , yet suffers a staggering 24.34% relative reduction in its specification soundness and completeness score. This consistent disparity, observed across all evaluated LLMs, strongly indicates that synthesizing sound and complete specifications is fundamentally more challenging than generating functional code. This stark contrast highlights a fundamental limitation in the current state-of-the-art models. Thanks to vast exposure to standard software repositories during pre-training, advanced LLMs have developed a remarkable proficiency for synthesizing functional programming logic. However, this empirical success is heavily reliant on statistical pattern matching and does not seamlessly transfer to the rigorous domain of formal verification. Synthesizing sound and complete specifications demands strict mathematical reasoning and a global awareness of constraints. Consequently, when tasked with formalizing properties that defend against adversarial edge cases, the reasoning capabilities of these models remain highly fragile.
sue without sacrificing evaluative rigor. It drastically reduces the time overhead to merely 1.38 and 1.05 times the original baseline. More importantly, while achieving this efficiency, V ERINA L ITE simultaneously maintains a performance degradation profile highly similar to the full V ERINA P LUS suite (as evidenced in Figure 5). This optimal balance proves that our reduction strategies successfully prune redundant cases while fully retaining the essential diagnostic power, thereby establishing V ERINA L ITE as a highly practical benchmark for evaluations of verifiable code generation.
5
Conclusion and Future Work
In this paper, we proposed VeriScale, an adversarial framework that systematically expands and reduces test suites to rigorously evaluate verifiable code generation. We instantiated VeriScale on the original V ERINA benchmark to construct V ERINA P LUS (expanded by over 83×) and V ERINA L ITE (a 14× variant). Our evaluations demonstrate that V ERI NA P LUS uncovers substantial weaknesses in stateof-the-art LLMs across both SpecGen and CodeGen tasks that original benchmarks fail to detect, while V ERINA L ITE achieves the same discriminative power with significantly reduced evaluation cost. Together, these augmented benchmarks provide a crucial, highly reliable standard for advancing LLM-based verifiable code generation. Future work will evolve VeriScale into a closedloop repair system, using the discovered counterexamples to guide models in iteratively patching flawed specifications. Furthermore, recognizing that SpecGen is fundamentally an autoformalization task severely bottlenecked by data scarcity, we plan to leverage VeriScale as an adversarial data engine. By synthesizing large-scale, high-quality training corpora, we aim to train a dedicated model
Efficiency of Test-Suite Reduction Strategy. Beyond evaluation rigor, the practical utility of a benchmark heavily depends on its computational overhead. As detailed in Table 2, exhaustively evaluating models on the expanded V ERINA P LUS incurs a substantial computational penalty due to the sheer volume of test cases. Specifically, this exhaustive approach multiplies the average time overhead to 1.80 and 1.50 times the baseline for the SpecGen and CodeGen tasks, respectively. Such pronounced time constraints can significantly hinder the widespread utilization of the benchmark. Crucially, our minimized benchmark, V ERI NA L ITE , effectively resolves this scalability is8
capable of robust autoformalization. Finally, generalizing VeriScale to other formal verification frameworks, such as Dafny, remains a critical step toward verifiable code generation.
Quinn Dougherty and Ronak Mehta. 2025. Proving the coding interview: A benchmark for formally verified code generation. Preprint, arXiv:2502.05714. Dan Hendrycks, Steven Basart, Saurav Kadavath, Mantas Mazeika, Akul Arora, Ethan Guo, Collin Burns, Samir Puranik, Horace He, Dawn Song, and Jacob Steinhardt. 2021. Measuring coding challenge competence with APPS. In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 2).
Limitations While VeriScale significantly advances the rigorous evaluation of verifiable code generation, it has several limitations. First, the pipeline relies fundamentally on the availability of ground-truth preconditions and the reference implementations. Second, the quality of the generated unexpected outputs is inherently bounded by the reasoning and formalization capabilities of the LLM acting as the red team. If the model struggles with the strict typing constraints of Lean 4, it may fail to synthesize sophisticated adversarial implementations. Third, the construction phase of the expanded test suites remains highly compute-intensive, requiring massive LLM sampling and Lean executions.
Naman Jain, King Han, Alex Gu, Wen-Ding Li, Fanjia Yan, Tianjun Zhang, Sida Wang, Armando SolarLezama, Koushik Sen, and Ion Stoica. 2025. Livecodebench: Holistic and contamination free evaluation of large language models for code. In The Thirteenth International Conference on Learning Representations. Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying rust programs using linear ghost types. Proc. ACM Program. Lang., 7(OOPSLA1). K. Rustan M. Leino. 2010. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, pages 348–370, Berlin, Heidelberg. Springer Berlin Heidelberg.
Acknowledgments This work is sponsored by the National Key R&D Program of China Grant No. 2022YFA1008200 (T. L.). We also thank Shanghai Institute for Mathematics and Interdisciplinary Sciences (SIMIS) for their financial support. This research was funded by SIMIS under grant number SIMIS-ID-2025-ST. The authors are grateful for the resources and facilities provided by SIMIS, which were essential for the completion of this work.
Jiawei Liu, Chunqiu Steven Xia, Yuyao Wang, and Lingming Zhang. 2023. Is your code generated by chatGPT really correct? rigorous evaluation of large language models for code generation. In Thirty-seventh Conference on Neural Information Processing Systems. Xiaoyang Liu, Zineng Dong, Yifan Bai, Yantao Li, Yuntian Liu, and Tao Luo. 2026. Decompose, structure, and repair: A neuro-symbolic framework for autoformalization via operator trees. Preprint, arXiv:2604.19000.
References
Evan Lohn and Sean Welleck. 2024. minicodeprops: a minimal benchmark for proving code properties. In Neurips Safe Generative AI Workshop 2024.
Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, and Charles Sutton. 2021. Program synthesis with large language models. Preprint, arXiv:2108.07732.
Chloe R Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, and Max Tegmark. 2025. Dafnybench: A benchmark for formal software verification. Transactions on Machine Learning Research.
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, and 39 others. 2021. Evaluating large language models trained on code. Preprint, arXiv:2107.03374.
Matias Martinez and Martin Monperrus. 2019. Astor: Exploring the design space of generate-and-validate program repair beyond genprog. J. Syst. Softw., 151(C):65–80.
Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient smt solver. In Tools and Algorithms for the Construction and Analysis of Systems, pages 337– 340, Berlin, Heidelberg. Springer Berlin Heidelberg.
Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. 2024. Towards ai-assisted synthesis of verified dafny methods. Proc. ACM Softw. Eng., 1(FSE).
9
Leonardo de Moura and Sebastian Ullrich. 2021. The lean 4 theorem prover and programming language. In Automated Deduction – CADE 28, pages 625–635, Cham. Springer International Publishing.
inferred program intent. Proc. ACM Softw. Eng., 2(ISSTA). Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, and Dawn Song. 2026. VERINA: Benchmarking verifiable code generation. In The Fourteenth International Conference on Learning Representations.
OpenAI, Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, Red Avila, Igor Babuschkin, Suchir Balaji, Valerie Balcom, Paul Baltescu, Haiming Bao, Mohammad Bavarian, Jeff Belgum, and 262 others. 2024. Gpt-4 technical report. Preprint, arXiv:2303.08774. Jiwon Park, Dominik Winterer, Chengyu Zhang, and Zhendong Su. 2021. Generative type-aware mutation for testing smt solvers. Proc. ACM Program. Lang., 5(OOPSLA). Hammond Pearce, Baleegh Ahmad, Benjamin Tan, Brendan Dolan-Gavitt, and Ramesh Karri. 2025. Asleep at the keyboard? assessing the security of github copilot’s code contributions. Commun. ACM, 68(2):96–105. Ethan Perez, Saffron Huang, Francis Song, Trevor Cai, Roman Ring, John Aslanides, Amelia Glaese, Nat McAleese, and Geoffrey Irving. 2022. Red teaming language models with language models. In Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, pages 3419–3448, Abu Dhabi, United Arab Emirates. Association for Computational Linguistics. Ali Satvaty, Suzan Verberne, and Fatih Turkmen. 2026. Undesirable memorization in large language models: A survey. Preprint, arXiv:2410.02650. Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. 2024. Clover: Closed-loop verifiable code generation. In AI Verification: First International Symposium, SAIV 2024, Montreal, QC, Canada, July 22–23, 2024, Proceedings, page 134–155, Berlin, Heidelberg. Springer-Verlag. Amitayush Thakur, Jasper Lee, George Tsoukalas, Meghana Sistla, Matthew Zhao, Stefan Zetzsche, Greg Durrett, Yisong Yue, and Swarat Chaudhuri. 2026. CLEVER: A curated benchmark for formally verified code generation. In The Thirty-ninth Annual Conference on Neural Information Processing Systems Datasets and Benchmarks Track. Ruijie Xu, Zengzhi Wang, Run-Ze Fan, and Pengfei Liu. 2024. 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: Unsupervised code-based adversarial attacks for programming language models via reinforcement learning. ACM Trans. Softw. Eng. Methodol., 34(1). He Ye, Aidan Z.H. Yang, Chang Hu, Yanlin Wang, Tao Zhang, and Claire Le Goues. 2025. Adverintentagent: Adversarial reasoning for repair based on
10
A
Detailed Type-aware Mutation Rules
When ingredient pool reuse is not triggered, we apply type-specific mutations for the following Lean input types: Int, Nat, List Int, Array Int, List Nat, Array Nat, and List Char, String. Integers.
When τ = Int, the domain is Dτ = Z. We define mutation-schema set as Oτ ≜ {sτ,1 , sτ,2 }
where sτ,1 (x, δ) = x + δ,
Θτ,1 = {−2, −1, 0, 1, 2} ,
sτ,2 (x, δ) = δx,
Θτ,2 = {−2, −1, 0, 1, 2} .
When ingredient pool reuse is disabled, both the mutation schema and its parameters are sampled uniformly. Therefore, 1 pτ (i) = , i ∈ {1, 2} , 2 1 qτ,i (δ) = , i ∈ {1, 2} , δ ∈ {−2, −1, 0, 1, 2} . 5 Natural numbers. When τ = Nat, the domain is Dτ = N. We obtain the mutation schemas by applying the integer schemas and clipping the result to the natural-number domain. Formally, let clip(z) = max(0, z), we define Oτ ≜ {sτ,1 , sτ,2 } , where sτ,1 (x; δ) = clip(x + δ),
Θτ,1 = {−2, −1, 0, 1, 2},
sτ,2 (x; δ) = clip(δx),
Θτ,2 = {−2, −1, 0, 1, 2}.
The clipping operation ensures that every mutated value remains in Dτ = N. When ingredient pool reuse is disabled, both the mutation schema and its parameters are sampled uniformly: 1 pτ (i) = , i ∈ {1, 2}, 2 1 qτ,i (δ) = , i ∈ {1, 2}, δ ∈ {−2, −1, 0, 1, 2}. 5 Integer lists and arrays. When τ ∈ {List Int, Array Int}, we model both lists and arrays as finite sequences. Thus, ! [ Dτ = Z∗ ≜ Zn . n∈N
We define the mutation-schema set as Oτ ≜ {sτ,1 , sτ,2 , sτ,3 , sτ,4 } , corresponding to element modification, appending, deletion, and reversal. For a sequence x, let |x| denote its length, xj its j-th element, replace(x, j, v) the sequence obtained by replacing xj with v, and del(x, j) the sequence obtained by deleting xj . The schemas are defined as ( replace(x, j, sInt,i (xj ; δ)) , |x| > 0, sτ,1 (x; j, i, δ) = x, |x| = 0, sτ,2 (x; v) = x ++ [v], ( del(x, j), |x| > 0, sτ,3 (x; j) = x, |x| = 0, sτ,4 (x) = rev(x). 11
The corresponding parameter spaces are Θτ,1 (x) = {0, . . . , |x| − 1} × {1, 2} × {−2, −1, 0, 1, 2}, Θτ,2 = {−5, −4, . . . , 5}, Θτ,3 (x) = {0, . . . , |x| − 1}, Θτ,4 = ∅. When |x| = 0, the index-dependent schemas are interpreted as the identity function, so the mutation remains well-defined. When ingredient pool reuse is disabled, the schema distribution is uniform: 1 pτ (i) = , 4
i ∈ {1, 2, 3, 4}.
The parameter distributions are uniform over their corresponding finite parameter spaces. In particular, 1 1 1 · · , |x| 2 5 1 qτ,2 (v) = , 11 1 qτ,3 (j | x) = , |x| qτ,4 (∗) = 1.
qτ,1 (j, i, δ | x) =
j ∈ {0, . . . , |x| − 1},
i ∈ {1, 2},
δ ∈ {−2, −1, 0, 1, 2},
v ∈ {−5, −4, . . . , 5}, j ∈ {0, . . . , |x| − 1},
Natural-number lists and arrays. When τ ∈ {List Nat, Array Nat}, domain of the two types are both ! [ ∗ n Dτ = N ≜ N . n∈N
The mutation schemas are analogous to those for integer lists and arrays, except that every newly generated element is clipped to the natural-number domain. Let clip(z) = max(0, z). We define Oτ ≜ {sτ,1 , sτ,2 , sτ,3 , sτ,4 } , where ( replace(x, j, clip(sInt,i (xj ; δ))) , |x| > 0, sτ,1 (x; j, i, δ) = x, |x| = 0, sτ,2 (x; v) = x ++ [clip(v)], ( del(x, j), |x| > 0, sτ,3 (x; j) = x, |x| = 0, sτ,4 (x; ∗) = rev(x). The parameter spaces are Θτ,1 (x) = {0, . . . , |x| − 1} × {1, 2} × {−2, −1, 0, 1, 2}, Θτ,2 = {−5, −4, . . . , 5}, Θτ,3 (x) = {0, . . . , |x| − 1}, Θτ,4 = ∅. For empty lists or arrays, we again interpret index-dependent mutations as identity transformations. When ingredient pool reuse is disabled, 1 pτ (i) = , 4
i ∈ {1, 2, 3, 4}. 12
The parameters are sampled uniformly: 1 1 1 · · , |x| 2 5 1 qτ,2 (v) = , 11 1 , qτ,3 (j | x) = |x| qτ,4 (∗) = 1.
qτ,1 (j, i, δ | x) =
j ∈ {0, . . . , |x| − 1},
i ∈ {1, 2},
δ ∈ {−2, −1, 0, 1, 2},
v ∈ {−5, −4, . . . , 5}, j ∈ {0, . . . , |x| − 1},
As before, when |x| = 0, we use a singleton dummy parameter space for the index-dependent schemas. Character lists.
When τ = List Char, the domain is ! Dτ =
Σ∗char ≜
[
Σnchar
,
n∈N
where Σchar denotes the finite set of allowable characters. We define Oτ ≜ {sτ,1 , sτ,2 , sτ,3 , sτ,4 } , corresponding to character modification, appending, deletion, and reversal: ( replace(x, j, c), |x| > 0, sτ,1 (x; j, c) = x, |x| = 0, sτ,2 (x; c) = x ++ [c], ( del(x, j), |x| > 0, sτ,3 (x; j) = x, |x| = 0, sτ,4 (x; ∗) = rev(x). The parameter spaces are Θτ,1 (x) = {0, . . . , |x| − 1} × Σchar , Θτ,2 = Σchar , Θτ,3 (x) = {0, . . . , |x| − 1}, Θτ,4 = ∅. When ingredient pool reuse is disabled, the schema is sampled uniformly: 1 pτ (i) = , 4
i ∈ {1, 2, 3, 4}.
The parameter distributions are uniform: 1 1 · , |x| |Σchar | 1 qτ,2 (c) = , |Σchar | 1 qτ,3 (j | x) = , |x| qτ,4 (∗) = 1.
qτ,1 (j, c | x) =
j ∈ {0, . . . , |x| − 1},
c ∈ Σchar ,
c ∈ Σchar , j ∈ {0, . . . , |x| − 1},
For |x| = 0, the index-dependent schemas use a singleton dummy parameter space and reduce to the identity transformation. 13
Strings. When τ = String, we model the domain in the same way as List Char, namely as the set of all finite character sequences: Dτ = Σ∗char . Unlike List Char, however, we define the mutation-schema set as Oτ ≜ {sτ,1 , sτ,2 , sτ,3 } , where sτ,1 (x) = ϵ,
Θτ,1 = ∅,
sτ,2 (x) = rev(x),
Θτ,2 = ∅,
sτ,3 (x; c) = x ++ c,
Θτ,3 = Σsp .
Here, ϵ denotes the empty string, rev reverses a string, and Σsp is the set of special characters. When ingredient pool reuse is disabled, the schema is sampled uniformly: 1 pτ (i) = , 3
i ∈ {1, 2, 3}.
The parameter distributions are qτ,1 (∗) = 1, qτ,2 (∗) = 1, qτ,3 (c) =
B
1 , |Σsp |
c ∈ Σsp .
Hyperparameter Settings
Table 3 provides the detailed hyperparameter configurations used across the test-suite expansion and reduction stages of the VeriScale pipeline. Table 3: Detailed hyperparameter settings for the VeriScale pipeline. Parameter
Value
Description
Test-Suite Expansion Seed Generation –rounds –candidates_per_round –example_limit
1 40 5
Number of LLM generation rounds for each task Number of candidates generated per round for each task Maximum number of accept/reject examples in prompt
Type-aware Mutation –max_mutations_per_input –mutation_multi_step_size –mutation_ingredient_prob
15 5 0.3
Upper limit of mutation samples per seed input Maximum number of consecutive steps per mutation Probability of ingredient reuse during mutation
Adversarial Implementation Synthesis –max_adver_impl
5
Maximum number of adversarial implementations per specification
Boundary-Preserving Reduction –MAX_REJECT_INPUTS_PER_TASK –KEEP_PER_CRITICAL_BUCKET
50 1
Maximum number of unexpected inputs retained per task Number of unexpected inputs retained from each boundary bucket
Adversary-Killing Reduction –MAX_ACCEPT_TEST_CASES_PER_TASK
50
Maximum number of expected input-output pairs retained per task
Test-Suite Reduction
14
C
Prompt Templates
This appendix provides the detailed prompt templates utilized across the expansion stage of the VeriScale pipeline. We present the exact instructions formulated for tasks including seed generation, problem decomposition, specification generation, and adversarial implementation synthesis. Prompt Template for Seed Generation You are an expert at generating diverse candidate inputs for Lean4 code verification tasks. Return ONLY a JSON array. Each element must strictly follow: {"input": {"param1": value1, "param2": value2, ...}} Rules: 1. Do not output markdown, prose, comments, or code fences. 2. Keys in each `input` object must exactly match the function parameter names: no missing keys, no extra keys. 3. Values must be JSON−serializable and type−compatible with the declared Lean parameter types. 4. Treat the ground−truth precondition as the valid−input boundary: generate both valid and invalid inputs, especially boundary cases. 5. Include both likely−valid and likely−invalid inputs. Treat likely−invalid as semantically violating the precondition, not malformed JSON. 6. 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 that satisfy it and inputs that violate it. − Focus on hard boundary/edge cases around this condition. − "likely−invalid" means: still valid JSON and type−compatible, but likely violates the precondition. Validity mix target: − total candidates: {candidate_count} − likely−invalid target: {invalid_target} − likely−valid target: {valid_target} − If constraints make exact ratio hard, prioritize exact total count and boundary coverage. Function parameters (JSON): {parameters} Example likely−valid inputs: {test_examples} Example likely−invalid inputs (maybe no examples available, but generate if possible): {reject_examples} Output format MUST be exactly a JSON array of objects: [{{"input": {{"param": value, ...}}}}, ...]
15
Prompt Template for Problem Decomposition ### Role You are a mathematical modeling expert. Your task is to analyze a programming problem description and produce a structured mathematical model that captures its formal meaning. ### Input − **Problem Description**: A natural language description of a programming problem. ### Instructions 1. 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, properties that may be included in the constraints) 2. 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.) 3. 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. 4. 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? 5. Unless explicitly stated, do NOT mark non−empty, integer−only, positivity, uniqueness, sortedness and etc. with `E`. 6. 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_description}
16
Prompt Template for Specification Generation ### Role You are an expert in Lean4 programming. Your task is to analyze a programming problem description and produce the Lean4 code of its precondition and postcondition. ### Input − **Problem Description**: A natural language description of a programming problem. − **Input**: Input of the problem, and constraints on the input. − **Output**: Output of the problem, and constraints on the output. − **Precondition Function Signature**: Function signature of the precondition. − **Postcondition Function Signature**: Function signature of the postcondition. ### Instructions 1. 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. 2. You should carefully analyze the problem description to help you identify gaps and omissions, thereby capturing any missing details within the Input and Output. 3. Define the Lean4 precondition and postcondition by using the provided function signature. 4. Only translate the constraints of the precondition marked with 'E'. Neglect the constraints marked with 'H'. 5. 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. postcondition implementation} ``` ### Now perform the task below: − **Problem Description**: {problem_description} − **Input**: {input} − **Output**: {output} − **Precondition Function Signature**: {precond_signature} − **Postcondition Function Signature**: {postcond_signature}
17
Prompt Template for Adversarial Implementation Synthesis ### Role You are an expert Red Teamer in formal verification and a "lazy" code hacker. Your objective is to perform " Specification Gaming": identify underspecification loopholes within a given `post−condition` in Lean4, and write degenerate code to exploit these vulnerabilities. ### Input − **Problem Description**: A natural language description of a programming problem. − **Pre−condition**: Defines valid inputs. Assume inputs always pass this. − **Post−condition**: The flawed contract your output MUST satisfy. − **Implementation Signatures**: The function signature of the adversarial functions. ### Instructions 1. 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 being provable). 2. 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 empty−list case is vacuously true? 3. 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`, `List.range n`, `Array.mkArray n 0`, or entirely fabricated data that satisfies the shape/type/length constraints. − *Malicious Deletion/Modification*: If the post−condition only checks for the absence of something (e.g., "no duplicates", "no negative elements"), delete everything and return `[]` / `#[]`. − *Edge Case Exploitation*: Force empty or trivial states (e.g., empty list, `0`, `none`) that make universally quantified checks (`∀ x ∈ []`, ...) vacuously true. 4. 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 of a function − register new `instance`s that shadow or override existing typeclass resolution for standard types (`Eq`, `LE`, `LT`, `Decidable`, `Ord`, `BEq`, `Hashable`, etc.) − rely on `IO`, `ST`, `IO.Ref`, or any monadic side effects that persist outside the function call − use noncomputable definitions or use `choose`, `choose_spec` to define the adversarial functions If any strategy requires modifying the ambient environment, DO NOT use it. 5. 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`, `HAdd`, `HSub`, ` Membership`, `GetElem` for standard types − return proxy/wrapper/sentinel values (e.g., via `Subtype` with a bogus proof, or a wrapper with a custom equality) that are not semantically valid outputs − exploit `Decidable` instances whose `decide` always returns `isTrue` Outputs must be plain values of the exact types expected by the specification (`Nat`, `Int`, `String`, `List α`, `Array α`, `Option α`, tuples of these, etc.). 6. 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. 7. 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. 8. 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 {adversatial function 3} −− Adversarial Implementation 4 {adversatial function 4} −− Adversarial Implementation 5 {adversatial function 5} ``` ### Now perform the task below: − **Problem Description**: {problem_description} − **Pre−condition**: ```lean {pre_condition} ``` − **Post−condition**: ```lean {post_condition} ``` − **Implementation Signatures**: ```lean {impl_signature} ```
19