Cost-Driven Synthesis of Sound Abstract Interpreters

TL;DR

This paper explores using large language models to automatically synthesize sound abstract interpreters for neural network verification, employing a novel cost function and validation framework to ensure correctness.

Contribution

It introduces a unified, cost-guided synthesis framework leveraging LLMs to generate sound abstract interpreters, addressing a key challenge in abstract interpretation.

Findings

Matches handcrafted interpreters in quality

Discovers sound interpreters for complex nonlinear operators

Outperforms existing literature in synthesis quality

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.