{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/124424"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/124424","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Neural abstract interpretation: Leveraging neural networks for automated, efficient and differentiable abstract interpretation","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2024-09-16 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2024-09-16 without embargo terms","abstract_has_math":false,"creators":["Gomber, Shaurya"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Singh, Gagandeep"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2024,"date_issued":"2024-05","date_published":"2024-05","updated_at":"2026-07-22T22:25:00Z","subjects":["Abstract Interpretation","Program Analysis","Differentiable Program Analysis"],"languages":["en","eng"],"rights":["Copyright 2024 Shaurya Gomber"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/124424","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Singh, Gagandeep"]},{"key":"dc:creator","label":"Author","values":["Gomber, Shaurya"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2024-05","2024-04-30"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Abstract Interpretation","Program Analysis","Differentiable Program Analysis"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2024 Shaurya Gomber"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/124424"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2024-09-16 without embargo terms","The student, Shaurya Gomber, accepted the attached license on 2024-04-27 at 14:59.","The student, Shaurya Gomber, submitted this Thesis for approval on 2024-04-27 at 15:32.","This Thesis was approved for publication on 2024-04-30 at 13:03.","DSpace SAF Submission Ingestion Package generated from Vireo submission #20676 on 2024-09-16 at 00:37:18","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."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Neural abstract interpretation: Leveraging neural networks for automated, efficient and differentiable abstract interpretation"]}]}],"canonical_facts":{"dc:contributor":["Singh, Gagandeep"],"dc:creator":["Gomber, Shaurya"],"dc:date":["2024-05","2024-04-30"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2024-09-16 without embargo terms","The student, Shaurya Gomber, accepted the attached license on 2024-04-27 at 14:59.","The student, Shaurya Gomber, submitted this Thesis for approval on 2024-04-27 at 15:32.","This Thesis was approved for publication on 2024-04-30 at 13:03.","DSpace SAF Submission Ingestion Package generated from Vireo submission #20676 on 2024-09-16 at 00:37:18","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."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/124424"],"dc:language":["en","eng"],"dc:rights":["Copyright 2024 Shaurya Gomber"],"dc:subject":["Abstract Interpretation","Program Analysis","Differentiable Program Analysis"],"dc:title":["Neural abstract interpretation: Leveraging neural networks for automated, efficient and differentiable abstract interpretation"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:00Z"}