Current numerical abstract interpretation relies on fixed, hand-crafted, instruction-specific transformers tailored to each domain, causing three key limitations: transformers cannot be reused across domains; precise compositional reasoning over instruction sequences is difficult; and all downstream tasks must use the same fixed transformer regardless of precision or efficiency needs.To address this, we propose the Evolving Abstract Transformer, which replaces the fixed single-output design with an adaptable search over a parametric space of sound outputs via two algorithms. 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, covering both individual instructions and structured sequences. Second, the Adaptive Gradient Guidance (AGG) algorithm leverages the differentiable structure of UPOSE's output space to efficiently search it according to downstream objectives and available runtime, continually evolving the output as more time is provided. We implement these ideas in the AbsEvolve framework and evaluate across three numerical abstract domains: Zones, Octagons, and Polyhedra. Results show the evolving transformer works across domains and instructions, enables efficient precision-efficiency tradeoffs by adjusting number of gradient steps in the search, and reaches the most precise invariants up to 3.2x faster than existing baselines.

翻译：当前数值抽象解释依赖领域定制的固定人工设计指令变换器，存在三个关键局限性：变换器无法跨领域复用；难以对指令序列进行精确组合推理；所有下游任务必须使用相同的固定变换器，无法根据精度或效率需求进行调整。为解决这些问题，我们提出可演化抽象变换器，通过两种算法将固定单输出设计替换为对合理输出参数空间的自适应搜索。首先，通用参数化输出空间编码器(UPOSE)可为任意多面体数值域和二次有界保护算子(QGO)类中的任意算子构建紧凑的合理输出参数空间，覆盖单条指令和结构化指令序列。其次，自适应梯度引导(AGG)算法利用UPOSE输出空间的可微结构，根据下游目标和可用运行时间高效搜索该空间，随着时间增加持续演化输出。我们在AbsEvolve框架中实现这些思想，并在三个数值抽象域（区域、八边形、多面体）上进行评估。结果表明，可演化变换器可跨领域和指令工作，通过调整搜索中的梯度步数实现高效的精度-效率权衡，并在生成最精确不变量方面比现有基线快达3.2倍。