The overview of SAIL.
How to construct globally sound abstract interpreters to safely approximate program behaviors remains a bottleneck in abstract interpretation. We show the potential of using state-of-the-art LLMs to automate this tedious process. Focusing on the neural network verification area, we synthesize non-trivial sound abstract transformers across diverse abstract domains using LLMs to search within infinite space from scratch. We formalize the synthesis task as a constrained optimization problem, for which we design a novel mathematically grounded cost function that measures the degree of unsoundness of each generated candidate transformer, while enforcing hard syntactic and semantic validity constraints.
To use this artifact, you will need a machine capable of running Docker with at least 16 GB of RAM and 35 GB of free disk space. The Docker image is approximately 20 GB in size. GPU is not required. Currently this artifact only supports Linux systems.
Special requirements: Running the generation experiments requires access to paid external LLM APIs (OpenAI API and/or AWS Bedrock).
git clone git@github.com:uiuc-focal-lab/SAIL.git
cd SAIL# You may need to use `sudo` depending on your system configuration
docker build -t sail-artifact .Note: This artifact mainly consists of two parts: (1) Model synthesis, which requires API keys; (2) Precision Evaluation, which does not require any external credentials. You may skip this step if you do not intend to run the model synthesis experiments. The Docker container and the evaluation experiments will still run successfully; however, the model synthesis functionality will be unavailable.
Fill in your API keys by editting SAIL/.env:
OPENAI_KEY=sk-...
AWS_ACCESS_KEY_ID=...
AWS_SECRET_ACCESS_KEY=...
Note: DO NOT share this file with anyone. All models are accessed through paid services. Monitor your usage carefully.
Run the following commands from the SAIL/ directory.
# You may need to use `sudo` depending on your system configuration
docker run --rm -it --network=host --env-file .env -v $(pwd):/app sail-artifactYou will be dropped into a bash shell inside the container at /app. All results generated inside the container will be saved directly to your local filesystem and can be visualized. The container will be automatically deleted after exit.
Inside the container, verify the installation by importing the core package:
python -c "import constraintflow; print('constraintflow OK')"You should see constraintflow OK.
Note: This experiment requires access to paid external LLM APIs (OpenAI API and/or AWS Bedrock). Make sure you have provided your own credentials in
.envwhen creating the container. If you do not have access to these APIs, you may skip this claim.
In the paper, we use 4 models to generate 14 operators in total across three abstract domains. To reproduce the full experiment, run:
./src/generation/gen.sh -m gpt-5 gpt-4o llama4 claude -c deeppoly deepz ibpNote: We recommend running this experiment sequentially as below for better performance. Since Running multiple model servers in parallel causes them to compete for CPU, RAM, and memory bandwidth, which significantly degrades inference throughput for each individual model. Each command below takes approximately 10-40 hours to complete (depending on model response speed).
./src/generation/gen.sh -m gpt-5 -c deeppoly deepz ibp
./src/generation/gen.sh -m gpt-4o -c deeppoly deepz ibp
./src/generation/gen.sh -m llama4 -c deeppoly deepz ibp
./src/generation/gen.sh -m claude -c deeppoly deepz ibpExpected Output: When starting the script successfully, you should see
[✓] Starting ... model on port ...
at the very beginning. And then a progress bar will appear indicating progress. Other warnings or error messages printed to the terminal during execution can be safely ignored. After finishing the synthesis, results are saved under src/generation/logs/<timestamp>/results/<domain>/<model>/:
logs/<timestamp>/results/<domain>/<model>/
├── generation.log # Full generation trace
├── success/
│ └── ... # Successfully synthesized operators (.txt)
├── failure/
│ └── ... # Failed operators (.txt)
└── statistics/
├── <model>.pdf # Overall performance chart, reporting the generation rounds, repair rounds, cost function refinement rounds.
├── <operator>_cost_curve.pdf # Visualization of the decrease of the cost through the synthesis process.
├── statistic.json # Per-operator summary (attempts, retries, runtime). Can be ignored.
└── op_monitor.json # Per-attempt cost tracking. Can be ignored.
The files generation.log, success/, and failure/ are generated incrementally during the synthesis process. The statistics/ directory is created after the program finishes, summarizing the overall results and visualizations. You may check the generation.log any time during the process to check the synthesis status.
Because LLM generation is stochastic, the synthesis results may vary across different runs. In particular, for more complex operators such as HardSigmoid, HardTanh, Affine, etc., the framework may sometimes fail to produce a sound transformer within the allowed number of attempts. In the paper, we reported the best result obtained across multiple runs for each operator, as shown in Figures 15–20 in the appendix of the paper. Figure 6 presents a representative example that is excerpted from the complete results. The results obtained from a single run of the artifact may therefore not always be as good as those shown in these figures.
Despite this randomness, the overall synthesis behavior remains consistent. For operators that are successfully synthesized, inspecting the detailed logs in generation.log and the corresponding cost function curves (*_cost_curve.pdf) shows that the optimization process gradually improves the candidate transformers. For example, the generation log will have the similar paragraph as below:
2026-03-16 22:41:39,182 - INFO - [RETRY 0 STEP 1] Sample 3: Validation failed. Get counter example:
Counterexample unsound for ...:
...
Start to evaluate the deviation.
2026-03-16 22:41:39,640 - INFO -
[Unsound Transformer Evaluation] Evaluation succeeds. Set the evaluation for the code:
...
to 0.375.
2026-03-16 22:41:39,641 - INFO - best_score : score = inf : 0.375
meaning that the synthesis process is guided by the cost of previously synthesized incorrect candidate. This behavior can be more clearly observed in the *_cost_curve.pdf files, where the cost function is visualized over iterations. In successful cases, the cost gradually converges to 0, indicating that the synthesized transformer has become globally sound. This trend is often more obvious when the synthesis task becomes more challenging. For example, the convergence behavior tends to be clearer for more complex operators (e.g., HardSigmoid compared to Add) and when using less capable models (e.g., LLaMA compared to GPT).
We conduct an ablation study to investigate the importance of different components in the SAIL framework. In particular, we evaluate how the synthesis performance changes when removing or modifying key modules in the pipeline, including the validation-repair module and the cost-function-guided refinement.
Note: This experiment requires access to paid external LLM APIs (OpenAI API and/or AWS Bedrock). Make sure you have provided your own credentials in
.envwhen creating the container. If you do not have access to these APIs, you may skip this claim.
To run the ablation experiments, use the following commands:
# w/o Counterexample (no cost function + counterexample)
./src/experiments/run_ablation/gen.sh -m llama4 -c deeppoly --mode wo_cex
# w/o Any feedback (no cost function + counterexample, no repair)
./src/experiments/run_ablation/gen.sh -m llama4 -c deeppoly --mode wo_anyExpected Output:
Results are saved under src/experiments/run_ablation/logs/<timestamp>/results/<domain>/<model>/ in the same format as the main generation pipeline. The ablation results correspond to Figures 13-14 in the paper.
Similarly, because LLM generation is stochastic, the exact results obtained from a single run may not be identical to those reported in the paper. However, the overall trends observed in the ablation study remain consistent. In most runs, removing key components of the framework leads to noticeably worse synthesis performance. For example, without cost and counterexample feedback (--mode wo_cex), the synthesis process typically converges more slowly and fewer operators are successfully synthesized. Without any feedback mechanism (--mode wo_any), the generation process often fails to converge to sound transformers within the allowed number of attempts. These behaviors match the qualitative trends reported in Figures 13–14 of the paper.
You can observe such trends in the statistics/<model>.pdf files or in the generation.log for more details. In the log, you will typically see repeated validation failures and retries, such as:
INFO - [Semantic Phase] ❌ Semantic error:
...
INFO - [RETRY 0 STEP 1] Sample 3: Validation failed.
...
This trend is often more obvious when the synthesis task becomes more challenging. For example, such failure-and-retry patterns appear more frequently for more complex operators (e.g., HardSigmoid compared to Add) and when using less capable models (e.g., LLaMA compared to GPT).
Note: First download the networks here directly, put them in
experiments/run_precision/nets/for the following experiments.
We evaluate the precision of the synthesized abstract transformers produced by SAIL and compare them against existing handcrafted transformers used in neural network verification frameworks. Table 1 in the paper presents a representative subset of the results for readability. The complete precision comparison results are reported in Table 2 and Table 3 in the appendix, which include the full set of evaluated operators and benchmarks.
We provides the script to reproduce the full evaluation pipeline. Run:
bash src/experiments/run_precision/run_all.shExpected Output:
Terminal outputs during the process can be ignored. In the end the terminal will print 2 tables with the title:
=============================DeepPoly===========================================
Dataset Network Training Activation Layers eps OurWork Handcrafted
----------------------------------------------------------------------------------
......
=============================DeepZ===========================================
Dataset Network Training Activation Layers eps OurWork Handcrafted
----------------------------------------------------------------------------------
......
respectively, which are expected to exactly match Tables 2 and Table 3 of the paper.
To remove the Docker image after the reproduction:
exit # exit the docker container
# You may need to use `sudo` depending on your system configuration
docker rmi sail-artifact # remove the docker image1. Credential errors (OPENAI_KEY not set, etc.)
Make sure the .env file is complete before running docker run.
2. Model server not reachable from gen.py
Make sure you used --network=host. Without it, socket.getfqdn() returns the container's internal hostname, which gen.py cannot reach.
3. Port already in use (Port xxxx is in use by another program)
A previous model server process may still be running. Kill it with:
pkill -f models.pyOr find the process using the port and kill it:
ss -lptn 'sport = :<port>'
# Then: kill -9 <PID>4. Out of disk space during build The full image is approximately 20–30 GB. Make sure Docker has sufficient disk space allocated.
5. run_all.sh: line N: <PID> Killed during precision evaluation
This means the system OOM (Out-of-Memory) killer terminated the process due to insufficient RAM.
To work around this, run each experiment script individually instead of through run_all.sh:
cd src/experiments/run_precision
python experiment_precision_mnist.py
python experiment_precision_mnist_constraintflow.py
python experiment_precision_mnist_gelu.py
python experiment_precision_mnist_hardtanh.py
python experiment_precision_mnist_relu6.py
python experiment_precision_cifar.py
python experiment_precision_cifar_constraintflow.py
python experiment_precision_cifar_gelu.py
python experiment_precision_cifar_hardtanh.py
python experiment_precision_cifar_relu6.py- README.md: instructions to run the artifact
- LICENSE: Apache 2.0 License file for the artifact
- Dockerfile: installation and configuration steps for the Docker image
- requirements-docker.txt: Python dependencies installed in the Docker image
- src/: source code for SAIL
- src/kick.sh: kick-the-tires script to quickly verify the full pipeline end-to-end
- src/constraintflow/: the ConstraintFlow abstract interpretation framework
- src/generation/: LLM-based synthesis pipeline
- src/generation/gen.py: main synthesis script (full pipeline with feedback loop)
- src/generation/models.py: model server for hosting LLMs
- src/generation/request.py: LLM query interface
- src/generation/validator/: syntax, semantics, and soundness checks used as feedback during synthesis
- src/generation/evaluator/: cost function evaluator for synthesized transformers
- src/generation/dnn_certifiers/: pre-synthesized abstract transformers produced by SAIL (used in precision experiments)
- src/experiments/: scripts and data to reproduce all evaluation experiments in the paper
- src/experiments/run_precision/: precision evaluation pipeline
- src/experiments/run_ablation/: ablation study scripts