Cost-Driven Synthesis of Sound Abstract Interpreters

TL;DR

This work tackles the long-standing challenge of constructing globally sound abstract interpreters by leveraging large language models (LLMs) to synthesize abstract transformers across domains, framed as constrained optimization guided by a novel soundness cost $\mathcal{L}$. The authors formalize global soundness via $F(\gamma(z)) \subseteq_C \gamma(F^{\#}(z))$ and introduce a comprehensive deviation metric $\Delta_S$, including shape-aware and single-assignment decompositions, together with a sampling-based relaxation that uses gradient-informed weights $\phi$ to drive refinement. The framework integrates LLM generation with static validation, a repair agent, and an SMT-based verifier (ProveSound) to obtain sound transformers, and proves convergence of the iterative refinement procedure under a fixed improvement threshold $\lambda$. Empirically, the approach yields transformers on par with handcrafted ones for standard nonlinear operators and can generate sound transformers for novel nonlinear operators (e.g., GeLU, ELU, Sigmoid) within DeepPoly and related domains, demonstrating strong precision in neural-network verification and indicating broad applicability beyond neural certification.

Abstract

Constructing abstract interpreters that provide global soundness guarantees remains a major obstacle in abstract interpretation. We investigate whether modern LLMs can reduce this burden by leveraging them to synthesize sound, non-trivial abstract interpreters across multiple abstract domains in the setting of neural network verification. We formulate synthesis as a constrained optimization problem and introduce a novel mathematically grounded cost function for measuring unsoundness under strict syntactic and semantic constraints. Based on this formulation, we develop a unified framework that unifies LLM-based generation with syntactic and semantic validation and a quantitative cost-guided feedback mechanism. Empirical results demonstrate that our framework not only matches the quality of handcrafted transformers, but more importantly, discovers sound, high-precision transformers for complex nonlinear operators that are absent from existing literature.

Figures (20)

• Figure 1: The overview of our framework. Given a prompt $p$, which specifies an operator, the domain specific language and abstract domain, and previous generation history, which includes the unsound transformer $F^\sharp_{t-1}$ and the counterexample $c$, the LLM $L_1$ proposes a set of candidates $\{F^\sharp_i, i\in[1,m]\}$, which will be validated by syntax and semantics checkers. Failing candidates trigger an automatic repair process based on another model agent $L_2$ until they pass the checkers. Valid candidates are scored by a soundness-driven cost $\mathcal{L}(F^\sharp)$. If their score is less than that of $F_t^\sharp$, then they will replace $F_t^\sharp$ as the current "best" unsound transformer in the prompt. This feedback loop transforms synthesis into an optimization process, refining candidates until $\mathcal{L}(F^\sharp)=0$.
• Figure 2: Definition and visualization of the HardSigmoid activation. HardSigmoid linearly approximates the standard sigmoid between $-3$ and $3$, and saturates at $0$ and $1$ outside this range.
• Figure 3: Correct polyhedra bounds for HardSigmoid transformer on interval $[\ell_i,u_i]$ when $\ell_i<-3<3<u_i$. The shaded areas highlight the safely approximated region.
• Figure 4: Incorrect polyhedra bounds for HardSigmoid transformer on interval $[\ell_i,u_i]$ when $\ell_i<-3<3<u_i$. The shaded areas highlight the regions that are not safely approximated and violate the soundness condition.
• Figure 5: Search trajectory of abstract transformers within the search space $\mathcal{H}$. Starting from $F^{\sharp}_0$, the process iteratively selects the candidate transformer with the lowest cost function value each round. Each refinement step must satisfy the progress condition $\mathcal{L}(\mathcal{R}(F^{\sharp})) < \mathcal{L}(F^{\sharp}) - \lambda$; for example, the transition from $F^{\sharp}_1$ to $F^{\prime\sharp}_2$ is invalid since it violates this constraint.

Theorems & Definitions (1)

• theorem 1