Cost-Driven Synthesis of Sound Abstract Interpreters
This addresses the problem of reducing manual effort in abstract interpretation for researchers and practitioners in neural network verification, representing an incremental advance by automating synthesis with LLMs.
The paper tackles the challenge of constructing sound abstract interpreters for neural network verification by using LLMs to synthesize them, achieving results that match handcrafted transformers and discover new ones for complex nonlinear operators.
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.