Validating Formal Specifications with LLM-generated Test Cases: Research artifact

This artifact accompanies the FM26 paper entitled "Validating Formal Specifications with LLM-generated Test Cases", which reports an empirical evaluation of using pre-trained large language models (LLMs) to automate the generation of test cases from natural language requirements. The artifact provides the scripts, datasets and required tools for reproducing the experiment and the analysis of the results. More specifically, the artifact is split into 3 components: Data preparation: Scripts to process the existing Alloy4Fun dataset of formal specifications to create the benchmarks for the evaluation. It also contains the pre-computed benchmarks. Experiment execution: Scripts to execute the experiment for the prepared benchmarks, which involves the use of LLM APIs. Depending on the LLM, this may require an API key. It also contains the pre-computed results from executing the experiment. Result analysis: Scripts to analyze the results from the experiment, by using a solver to check validity and diversity. It also contains the pre-computed analysis results. Data requirements.json: all natural language requirements for which instances were generated, along with pointers to the Alloy4Fun database to retrieve oracles. Each entry consists of the following: example: its description model: the declaration of its structure in Alloy id: the identifier of the model in the Alloy4Fun database containing the oracles requirements: the list of requirements for this model, containing a description in natural language and the pred encoding its oracle prompt_zero.txt, prompt_one.txt, and prompt_few.txt: prompts for the generation of valid/invalid instances from requirements models_20250916.json.gz: a snapshot of the Alloy4Fun database filtered for the exercises used in the evaluation alloytools.jar: snapshot of AlloyTools, used to parse and execute Alloy models and commands prepare: directory containing scripts to retrieve oracles and incorrect submissions from the Alloy4Fun database. It contains: semantic_grouping.py: a script to perform grouping of the entries merge_reqs_groups.py: a script to merge groups with requirements.json for subsequent analysis results: a folder with the pre-calculated results for the scripts execute: directory containing scripts to call LLM APIs for the generation of instances given a dataset of requirements and header prompts. It contains: claude.py: script for Claude Opus 4.1 gemini.py: script for Gemini 2.5 Pro gpt.py: script for GPT-5 and GPT-5 Mini llama.py: script for Llama 3.1 results: a folder with the pre-calculated results for the scripts analysis: directory containing analysis scripts to process the LLM-generated instances. It contains: analysis.py: script for testing syntactic and semantic correctness of generated instances, as well as diversity results: a folder with the pre-calculated results for the scripts invalid: a folder containing invalid generated instances with annotations Results RQ1: Influence of prompt design Prompt Tests Syntax Scopes Previous Valid % Cost Few-shot 258 255 255 252 247 96% $3.56 One-shot 258 226 208 206 205 79% $3.69 Zero-shot 258 137 120 119 118 46% $4.20 RQ2: Effect of non-determinism Run Tests Syntax Scopes Previous Valid % Cost 1st 258 255 255 252 247 96% $3.56 2nd 258 256 256 256 251 97% $3.50 3rd 258 252 252 250 246 95% $3.61 RQ3: LLM comparison Model Tests Syntax Scopes Previous Valid % Cost GPT-5 258 255 255 252 247 96% $3.56 Gemini 2.5 Pro 258 248 220 212 210 81% $2.78 Claude Opus 4.1 258 258 258 202 197 76% $5.55 GPT-5 Mini 258 188 183 179 174 67% $0.53 RQ4: Characterization of invalid test cases See annotated Alloy files in analysis/invalid for the GPT-5, 3 positive / 3 negative instances, few-show prompt, or the raw failure files in analysis/results. RQ5: Effectiveness at detecting incorrect specifications Size Complete Wrong Missed Mean % 1 pos, 1 neg 41 5587 2204 38.10% 2 pos, 2 neg 34 4623 814 17.02% 3 pos, 3 neg 36 4395 525 9.90% 4 pos, 4 neg 35 5129 446 7.45% 5 pos, 5 neg 35 4816 348 6.43% Reproducibility Setup The scripts are written in Python and use (through a JPype interface) the Alloy Analyzer (a standalone Java archive). Reproducing the analysis requires: - A JVM (Java 17 or later), with the JAVA_HOME correctly set in the environment - A Python installation (3.11 or later) (with the same architecture as the JVM) Then install the Python requirements: pip install -r requirements.txt Alternatively, use the provided Dockerfile to create a Docker image with all the dependencies and run the scripts from within it: docker build -t alloy-llm-tests . docker run -it alloy-llm-tests Data preparation Script semantic_grouping.py groups together all entries of an Alloy4Fun database that have been submitted to given challenges. Entries are grouped when semantically equivalent according to the Alloy solver (i.e., equivalence within a certain scope). Since the solver is called to compare entries, this may take some time. Two entries are equivalent for a challenge if the predicate to be filled by the student are equivalent (identified as an empty predicate called from a check command in the root model). This has a few consequences: This ignores any pre-condition in the check. This means that there may be multiple correct groups (which were equivalent under the pre-conditions). If the student used any auxiliary predicate, the test will fail, since these are not copied into the test (there are few cases, identified in the log). The script only considers execution entries that are syntactically correct in the database (no sharing entries, nor errored). Script merge_reqs_groups.py can then be used to insert erroneous specifications into the provided requirements.json. The mapping is done via the predicate name: for each example in requirements.json (identified by id in the Alloy4Fun database), each requirement must have the student predicate defined. The script will search for the corresponding groups among the files generated by semantic_grouping.py. The script ignores groups with only 1 entry (i.e., submissions that have only been attempted once). Usage Run the grouping script as: usage: semantic_grouping.py [-h] [-o OUTPUT] [-s SCOPE] jar entries ... Script for grouping semantically and syntactically equivalent Alloy predicates positional arguments: jar AlloyTools jar path entries JSON entry database path originals Ids for the models to process optional arguments: -h, --help show this help message and exit -o OUTPUT, --output OUTPUT Output folder path (default=results) -s SCOPE, --scope SCOPE Scope for equivalence tests (default=3) This generates a JSON file for each of the selected entries with the grouping information. Finally, run the merging script into the requirements JSON file:usage: merge_reqs_groups.py [-h] [-o OUTPUT] [-t THRESHOLD] groups reqs Script for merging entry groups with challenge requirements positional arguments: groups folder with JSONs with entry groups reqs JSON with challenge requirements optional arguments: -h, --help show this help message and exit -o OUTPUT, --output OUTPUT Output JSON path (default=dataset.json) -t THRESHOLD, --threshold THRESHOLD Member group filtering threshold (default=2) This generates an extended version of the requirements JSON file with grouping information. Results The script was run for models Social Network (x3JXgWhJ3uti5Dzxz), Courses (iP5JL36afv5KbDKP6), Production line (dyj49tEp7j6aWAQQX) and Train Station (cXPP9QBPTYgTX6WJ6), with scope 3, for the Alloy4Fun database models_20250916.json.gz. Statistics are in prepare/results/grouping_stats.txt and groups in folder prepare/results. Note: this takes a few hours to run. python3 prepare/semantic_grouping.py alloytools.jar models_20250916.json.gz cXPP9QBPTYgTX6WJ6 x3JXgWhJ3uti5Dzxz iP5JL36afv5KbDKP6 dyj49tEp7j6aWAQQX These groups have been merged into the provided requirements.json in file prepare/results/dataset.json. Statistics are in prepare/results/merging_stats.txt. python3 prepare/merge_reqs_groups.py prepare/results requirements.json Experiment execution Scripts in folder execute call the APIs of the selected LLMs and ask for the generation of instances of the requirements prepared in the previous phase, using one of the provided prompts. Usage For each of the supported LLMs (gpt, gemini, claude, llama) , the generation script is run as: usage: [LLM].py [-h] prompt dataset instances Script for generating instances using [LLM] positional arguments: prompt the header prompt to be passed to the LLM dataset the dataset of natural language requirements instances the number of positive and negative instances to be generated options: -h, --help show this help message and exit Note that running gpt, gemini or claude requires a valid API key to be configured in the environment. For llama, a local model version llama3.1:8b is expected to be running. A Dockerfile is also provided to launch the proper llama instance: docker build -t llama3.1 -f ollama.Dockerfile .docker run -p 11434:11434 llama3.1 Note also that running the script for each LLM may take a few hours. The output of this script is a JSON file extending the provided dataset with a field instances containing instances generated by the LLM. Results The script was run for a few combinations of LLMs (GPT-5, GPT5 Mini, Gemini 2.5 Pro, Claude Opus 4.1), the provided prompts (prompt_zero.txt, prompt_one.txt and prompt_few.txt), and number of instances (from 1 to 5), for the requirements in prepare/results/dataset.json. For instance, for GPT-5, few-shot prompt and 3 instances, the following command should be run: python3 execute/gpt.py prompt_few.txt prepare/results/dataset.json 3 The pre-computed results of the generation process as extended JSON files are collected in execute/results. Results analysis Scripts in folder analysis process the instances generated by the LLMs and use AlloyTools to check its syntactic and semantic validity, as well as how many erroneous entries in the Alloy4Fun dataset would be detected. Usage For each of the JSON files containing LLM-generated instances, the generation script is run as: usage: analyze.py process [-h] jar results icost ocost positional arguments: jar AlloyTools jar path results JSON LLM instance generation results icost input cost ocost output cost options: -h, --help show this help message and exit The LLM token cost can be passed to print total cost statistics. This script reports overall results in terms of valid and failing instances, both in textual .txt and markdown .md format. Additionally, it provides a JSON file reporting all failing instances for inspection. Alternatively, the analysis can be run for a set of LLM executions specified in a JSON file. usage: analyze.py all [-h] jar execs positional arguments: jar AlloyTools jar path execs JSON file reporting a set of LLM executions and costs options: -h, --help show this help message and exit Results To run the analysis for an LLM execution the following command should be run, in this case for GPT-5, few-shot prompt and 3 instances: python analysis/analyze.py process alloytools.jar execute/results/gpt-5-2025-08-07_230925_few3.json 1.25 10 Running the analysis for all executions of the benchmark can be done with the following command. Note that this takes about 30 minutes to execute. python analysis/analyze.py all alloytools.jar execute/results/results.json The script was run for all LLM executions, whose JSON files are stored in execute/results. These pre-computed results of the analysis process are in analysis/results, containing the overall results in textual .txt and markdown .md format. The JSON files reporting failing instances are contained in analysis/invalid.