# SAIL: Sound Abstract Interpreters with LLMs

arXiv: https://arxiv.org/abs/2511.13663 · HTML: https://mlsanity.com/paper/2511.13663/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 87 references that are in the map.
- First posted on arXiv 17 Nov 2025.

## Builds on (most cited first, 23 of 23)

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesis](https://mlsanity.com/paper/2203.13474/) (2022)
- [Automatic differentiation in machine learning: a survey](https://mlsanity.com/paper/1502.05767/) (2015)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Hallucination is Inevitable: An Innate Limitation of Large Language Models](https://mlsanity.com/paper/2401.11817/) (2024)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Towards Stable and Efficient Training of Verifiably Robust Neural Networks](https://mlsanity.com/paper/1906.06316/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Jigsaw: Large Language Models meet Program Synthesis](https://mlsanity.com/paper/2112.02969/) (2021)
- [Symbolic Regression with a Learned Concept Library](https://mlsanity.com/paper/2409.09359/) (2024)
- [When Deep Learning Met Code Search](https://mlsanity.com/paper/1905.03813/) (2019)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions](https://mlsanity.com/paper/2201.13351/) (2022)
- [Safe Neurosymbolic Learning with Differentiable Symbolic Execution](https://mlsanity.com/paper/2203.07671/) (2022)
- [Demanded Abstract Interpretation (Extended Version)](https://mlsanity.com/paper/2104.01270/) (2021)
- [Verification in the Loop: Correct-by-Construction Control Learning with Reach-avoid Guarantees](https://mlsanity.com/paper/2106.03245/) (2021)
- [Automated Verification of Soundness of DNN Certifiers](https://mlsanity.com/paper/2504.04542/) (2025)
- [Synthesizing Abstract Transformers](https://mlsanity.com/paper/2105.00493/) (2021)
- [A Tensor-Based Compiler and a Runtime for Neuron-Level DNN Certifier Specifications](https://mlsanity.com/paper/2507.20055/) (2025)

## Built on by (most cited first, 2 of 2)

- [Lattice Deduction Transformers](https://mlsanity.com/paper/2605.08605/) (2026)
- [Ceci n'est pas une pipe: AI systems as semantic abstractions](https://mlsanity.com/paper/2607.09489/) (2026)

## Abstract (arXiv)

How to construct globally sound abstract interpreters to safely approximate program behaviors remains a bottleneck in abstract interpretation. In this paper, 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. Building on this formulation, we introduce SAIL, a novel unified framework that combines model generation, syntactic and semantic validation, and cost-function-based refinement to synthesize globally sound abstract transformers. Evaluation results show that SAIL not only matches the performance of manually designed transformers, but also is able to synthesize sound and high-precision transformers that do not exist in the literature for complex non-linear operators.