{"ID":2840749,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2511.13663","arxiv_id":"2511.13663","title":"Cost-Driven Synthesis of Sound Abstract Interpreters","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.","short_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 n...","url_abs":"https://arxiv.org/abs/2511.13663","url_pdf":"https://arxiv.org/pdf/2511.13663v1","authors":"[\"Qiuhan Gu\",\"Avaljot Singh\",\"Gagandeep Singh\"]","published":"2025-11-17T18:16:36Z","proceeding":"cs.PL","tasks":"[\"cs.PL\",\"cs.LG\"]","methods":"[\"Transformer\",\"Large Language Model\"]","has_code":false}