Neural abstract interpretation: Leveraging neural networks for automated, efficient and differentiable abstract interpretation

Abstract Interpretation is a popular technique for formally analyzing the properties of programs, neural networks, and complex real-world systems. However, designing efficient abstract transformers for expressive relational domains such as Octagon and Polyhedra is hard as one needs to carefully balance the fundamental tradeoff between the cost, soundness, and precision of the transformer for downstream tasks. Further, scalable implementations involve intricate performance optimizations like Octagon and Polyhedra decomposition. This motivates the need for the automatic generation of efficient, sound, and precise abstract transformers. Given the inherent complexity of abstract transformers and the proven capability of neural networks to effectively approximate complex functions, this thesis envisions and proposes the concept of Neural Abstract Transformers: neural networks that serve as abstract transformers. The Neural Abstract Interpretation (NeurAbs) framework introduced in this thesis provides supervised and unsupervised methods to learn efficient neural transformers automatically, which reduces development costs. These neural transformers can then act as a fast and sometimes even more precise replacement for slow and imprecise hand-crafted transformers. Additionally, these neural transformers are differentiable as opposed to the hand-crafted ones. This enables differentiable abstract interpretation and allows for the use of gradient-guided learning methods to solve problems that can be posed as learning tasks. We instantiate the NeurAbs framework for two widely used numerical domains: Interval and Octagon. Evaluations on these domains demonstrate the effectiveness of the NeurAbs framework to learn sound and precise neural transformers. We further demonstrate the advantages of differentiability of neural transformers by formulating the task of invariant generation as a learning problem and then using the learned neural transformers in the Octagon domain to generate valid octagonal invariants.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2024

Author dc:creator

• Gomber, Shaurya

Contributors dc:contributor

• Singh, Gagandeep

• Abstract Interpretation
• Program Analysis
• Differentiable Program Analysis

Statement dc:rights

• Copyright 2024 Shaurya Gomber

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/124424

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F124424