Static analysis of differentiable programs

Differentiable Programming which includes Automatic Differentiation (AD), serves as the backbone for machine learning and simultaneously pervades many other domains including graphics and scientific computing. Despite AD’s ubiquity, automated formal reasoning about the derivatives AD computes has lagged. The difficulty in developing automated analyses for differentiable programs stems from the fact that these programs use complicated semantics, contain highly nonlinear operations (e.g., the chain rule) and involve thousands of program variables. Thus, developing program analyses for AD that are simultaneously general, precise, and scalable remains a challenging task. To tackle these challenges, this dissertation develops a novel, unified framework for statically analyzing differentiable programs by coupling abstract interpretation with automatic differentiation. To obtain program analyses with the desired generality, Chapter 2 of this dissertation proposes DeepJ, the first abstract interpretation framework built upon Clarke Generalized Jacobians. By leveraging a generalized notion of derivatives, DeepJ can soundly reason about gradient properties for both differentiable and non-differentiable (but Lipschitz continuous) functions that result from programs with control flow. The need for generality also extends to higher derivatives and richer program abstractions. To enable these extensions, Chapter 3 proposes the first general construction for abstract interpretation of higher-order AD. This construction allows one to automatically build sound abstract interpreters for arbitrary orders of derivatives with general numerical abstract domains for precise analysis of program properties defined over higher derivatives. To obtain the desired precision, Chapter 4 proposes Pasado which is the first automated technique to synthesize precise static analyzers tailored to the structure of AD. By formulating abstract interpretation as a tractable optimization problem, Pasado optimally solves for precise abstractions of groups of multiple nonlinear operations which correspond to the chain rule, product rule, and quotient rule. Since these rules underlie forward and reverse mode AD, Pasado’s generality enables abstract interpretation of both modes. Compared to the prior state of the art, this precision allows Pasado to compute derivative bounds and local Lipschitz constant bounds that are orders of magnitude more precise. In addition, this dissertation shows extensive experimental results in Chapters 2, 3, and 4 highlighting how these static analyses obtain high scalability. These experiments demonstrate how the proposed analyses successfully reason about derivatives of large convolutional neural architectures involving hundreds of thousands of nonlinear operations.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2024

Author dc:creator

• Laurel, Jacob Scott

Contributors dc:contributor

• Misailovic, Sasa
• Singh, Gagandeep
• Marinov, Darko
• Hückelheim, Jan

• Static Analysis
• Differentiable Programming
• Automatic Differentiation
• Abstract Interpretation
• Programming Languages

Statement dc:rights

• Copyright 2024 Jacob Scott Laurel

Language dc:language

en, eng

Handle dc:identifier

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

OAI record oai:identifier

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