一句话：提出可演化抽象变换器，用参数化可靠输出空间上的梯度搜索替代固定变换器，实现跨数值域、可适应精度—效率权衡的抽象解释。
现有数值抽象解释依赖固定、手工定制且指令级的变换器，导致三个问题：变换器无法跨域复用，新域或新算子需重新设计；难以对指令序列进行精确的组合推理；下游任务被迫使用同一固定变换器，无法按精度、效率或任务需求调整。为此，论文提出可演化抽象变换器（Evolving Abstract Transformer），将传统单一固定输出设计替换为在可靠输出参数空间上的自适应搜索。其核心包括两个算法：UPOSE 为任意多面体数值域和二次有界守卫算子（QGO）类中的任意算子（涵盖单条指令与结构化序列）构造紧凑的可靠输出参数空间；AGG 利用该空间的可微结构，根据下游分析目标和可用运行时间，用梯度更新高效搜索，并随更多时间持续演化输出。作者在 AbsEvolve 框架中实现该思想，并在 Zones、Octagons、Polyhedra 三个数值抽象域上评估。结果表明，该变换器可跨域工作，处理多种指令与序列，通过调整梯度步数在精度—效率之间灵活权衡，且生成最精确不变式的速度最高比现有基线快 3.2 倍。
Current numerical abstract interpretation relies on fixed, hand-crafted, instruction-specific transformers tailored to each domain, giving rise to three significant limitations. First, extensibility is limited because transformers cannot be reused across domains and new transformers need to be designed for each new domain or operator. Second, precise compositional reasoning over instruction sequences is difficult as transformers are defined only at the instruction level. Third, all downstream tasks are forced to use the same fixed transformer, irrespective of their precision, efficiency, or task-specific requirements. To address these limitations, we propose the Evolving Abstract Transformer, a general transformer that replaces the fixed single-output design of traditional transformers with an adaptable search over a parametric space of sound outputs. This is achieved through two underlying algorithms we develop. First, the Universal Parametric Output Space Encoder (UPOSE) constructs a compact parametric space of sound outputs for any polyhedral numerical domain and any operator in the Quadratic-Bounded Guarded Operators (QGO) class which includes both individual instructions and structured sequences. Next, the Adaptive Gradient Guidance (AGG) algorithm leverages the differentiable structure of the space generated by UPOSE and uses gradient-based updates to efficiently search it according to downstream analysis objectives and available runtime, continually evolving the output as more time is provided. We implement these ideas in the AbsEvolve framework and evaluate their effectiveness across three numerical abstract domains: Zones, Octagons, and Polyhedra. Our results demonstrate that the evolving transformer works across domains and handles diverse instructions and sequences, allowing efficient adaptability in the precision–efficiency tradeoff by adjusting the number of gradient steps in the search, while also reaching the most precise invariants up to 3.2× faster than existing baselines.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{GomberBS26,
title = {Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation},
author = {Shaurya Gomber and Debangshu Banerjee and Gagandeep Singh},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808346}
}