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.

翻译：如何构造全局可靠的抽象解释器以安全近似程序行为，仍是抽象解释领域的瓶颈。本文展示了利用最先进大语言模型自动化这一繁琐过程的潜力。聚焦神经网络验证领域，我们通过LLMs从零开始在无限空间中搜索，跨多种抽象域合成了非平凡的可靠抽象转换器。我们将合成任务形式化为带约束优化问题，为此设计了基于数学原理的新型代价函数——该函数在施加严格句法/语义有效性约束的同时，可量化每个候选生成转换器的不可靠程度。基于此公式，我们提出SAIL这一统一框架，通过融合模型生成、句法语义验证及基于代价函数的精炼，实现全局可靠抽象转换器的合成。评估结果表明，SAIL不仅能匹敌人工设计的转换器性能，还能为现有文献中未涉及的复杂非线性算子合成可靠且高精度的新型转换器。