一句话：提出 SAIL 框架，利用 LLM 自动合成全局可靠的抽象变换器，将任务形式化为约束优化并用不可靠度代价函数指导搜索。
构建全局可靠的抽象解释器以安全近似程序行为是抽象解释领域的瓶颈。本文探索利用最先进的大语言模型（LLM）自动化这一繁琐过程，聚焦神经网络验证，在不同抽象域上从零搜索合成非平凡的可靠抽象变换器。作者将合成任务形式化为约束优化问题，设计了一种新颖的、有数学基础的代价函数来度量生成候选变换器的不可靠程度，同时施加严格的语法和语义有效性约束。基于此，提出 SAIL 统一框架，结合模型生成、语法与语义验证以及基于代价函数的精化，合成全局可靠的抽象变换器。实验表明，SAIL 不仅匹配手工设计变换器的性能，还能为复杂非线性算子合成文献中不存在的可靠且高精度的变换器。
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.
@article{paperbot3754,
title = {SAIL: Sound Abstract Interpreters with LLMs},
author = {Qiuhan Gu and Avaljot Singh and Gagandeep Singh},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808308}
}