Static analysis of differentiable programs

Laurel, Jacob Scott

Permalink

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

Description

Title

Static analysis of differentiable programs

Author(s)

Laurel, Jacob Scott

Issue Date

2024-12-03

Director of Research (if dissertation) or Advisor (if thesis)

Misailovic, Sasa

Doctoral Committee Chair(s)

Misailovic, Sasa

Committee Member(s)

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

Department of Study

Siebel School Comp & Data Sci

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

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

Abstract

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.

Graduation Semester

2024-12

Type of Resource

Thesis

Handle URL

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

Copyright and License Information

Copyright 2024 Jacob Scott Laurel

Owning Collections